6180 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Yen-Sheng Ho	46b6ac1539	improved %pdra -L	2017-02-27 20:44:19 -08:00
Yen-Sheng Ho	9195192f65	%pdra -L: now applies to all types	2017-02-27 14:31:59 -08:00
Yen-Sheng Ho	bb3eacf480	small tweaks	2017-02-27 13:45:22 -08:00
Alan Mishchenko	ed31679759	Enabling LUT pairing.	2017-02-27 12:18:24 -08:00
Yen-Sheng Ho	ff745ca1a5	fixed a bug	2017-02-26 15:45:35 -08:00
Yen-Sheng Ho	86b3cb3da9	added an option -L to %pdra for limiting the number of muxes	2017-02-26 15:39:48 -08:00
Yen-Sheng Ho	27bdffd5a2	small tweaks	2017-02-26 14:38:38 -08:00
Yen-Sheng Ho	cba376cfff	improved %pdra -b	2017-02-25 22:26:51 -08:00
Yen-Sheng Ho	a8f6e5c60a	added an option -b to %pdra	2017-02-25 18:32:43 -08:00
Alan Mishchenko	4ec5ee410d	Adding dump of trivial abstraction map at the beginning in &gla -m.	2017-02-25 16:22:31 -08:00
Yen-Sheng Ho	a7bc919b69	imported proof-based codes from ufar	2017-02-25 15:22:30 -08:00
Yen-Sheng Ho	7508a37a51	imported proof-based codes from ufar	2017-02-25 14:58:01 -08:00
Alan Mishchenko	7d5b1c572b	Restoring constraint manager to read old constraint file by default (use 'read_constr -n' to read new format).	2017-02-25 13:34:54 -08:00
Alan Mishchenko	80773b9522	Adding dump of trivial abstraction map at the beginning in &gla -m.	2017-02-25 09:49:31 -08:00
Yen-Sheng Ho	14cf117968	imported proof-based codes from ufar	2017-02-25 09:37:59 -08:00
Yen-Sheng Ho	06797fb611	mege	2017-02-24 14:21:45 -08:00
Alan Mishchenko	db36c65bce	Small changes in the usage message for &gla.	2017-02-23 14:12:56 -08:00
Yen-Sheng Ho	ca0bdde9b3	changed how pdr -t cleans up abs flops	2017-02-23 10:54:53 -08:00
Yen-Sheng Ho	d5bbf9188c	added %pdra -a: run with pdr -nct	2017-02-23 08:48:53 -08:00
Mathias Soeken	28e8e7f3e7	Merged alanmi/abc into default	2017-02-22 19:00:28 -08:00
Yen-Sheng Ho	f01c63f712	working on %pdra -m	2017-02-22 17:57:19 -08:00
Yen-Sheng Ho	2f90e5e15d	added an option -m for %pdra	2017-02-22 15:37:49 -08:00
Alan Mishchenko	dd8cc7e9a2	Removing unused procedure.	2017-02-22 13:03:53 -08:00
Alan Mishchenko	53b1d46b8d	Remapping flops in '%pdra.	2017-02-21 22:20:03 -08:00
Alan Mishchenko	96ccd24e6e	Changes to Visual Studio project file to support 'pdra'.	2017-02-21 20:39:52 -08:00
Alan Mishchenko	0e9f8093c3	Merged in ysho/abc (pull request #59) ... added a new abstraction	2017-02-22 04:31:10 +00:00
Yen-Sheng Ho	fb2fbd70bd	clean up	2017-02-21 20:10:11 -08:00
Yen-Sheng Ho	01e6beea8e	clean up	2017-02-21 20:06:13 -08:00
Bruno Schmitt	9d46d84b27	Small tweak to rollback behavior.	2017-02-21 18:37:06 -03:00
Yen-Sheng Ho	c5e9506f5d	small tweaks in %pdra -p	2017-02-20 12:58:20 -08:00
Yen-Sheng Ho	9f43c84501	added options of checking and pushing to %pdra	2017-02-20 12:51:04 -08:00
Alan Mishchenko	ac1eb60db9	Experiments with SAT sweeping.	2017-02-20 12:32:32 -08:00
Yen-Sheng Ho	19510bd38e	added datastructure for %pdra options	2017-02-20 11:07:12 -08:00
Yen-Sheng Ho	222b3741a4	fixed time profiling in pdr	2017-02-20 10:13:18 -08:00
Yen-Sheng Ho	25ecc3d429	fixed a tricky bug: property should not be assumed true in the last frame	2017-02-19 19:57:44 -08:00
Yen-Sheng Ho	1a66a5823a	working on pdr with wla	2017-02-19 16:09:59 -08:00
Yen-Sheng Ho	2d1792040a	working on pdr with wla	2017-02-19 15:57:13 -08:00
Bruno Schmitt	68dd780635	Adding new command to reset Satoko. ... Small fixes in watching list data structure.	2017-02-19 15:34:21 -08:00
Alan Mishchenko	99fe7dfe29	Experiments with SAT sweeping.	2017-02-19 12:51:38 -08:00
Yen-Sheng Ho	2732cbc1ee	working on pdr with wla	2017-02-19 12:31:28 -08:00
Yen-Sheng Ho	840f5d1ca8	working on pdr with wla	2017-02-19 10:22:15 -08:00
Yen-Sheng Ho	6cf289dadd	working on pdr with wla	2017-02-19 09:55:58 -08:00
Yen-Sheng Ho	24fdcecb2d	started %pdra	2017-02-19 09:20:44 -08:00
Yen-Sheng Ho	fc0f3b8d0d	working on incremental pdr	2017-02-18 21:22:26 -08:00
Alan Mishchenko	27caed8dc8	Experiments with SAT sweeping.	2017-02-18 20:20:50 -08:00
Bruno Schmitt	3f0cb6318b	New function to retrieve polarity value of a variable.	2017-02-18 17:08:54 -08:00
Bruno Schmitt	ac409b3152	Bug fix in analyze_final method.	2017-02-18 15:24:56 -08:00
Yen-Sheng Ho	fdc0b471e5	working on incremental pdr	2017-02-18 14:38:08 -08:00
Alan Mishchenko	131c1613a4	Compiler warnings.	2017-02-18 14:29:04 -08:00
Alan Mishchenko	316238d484	Compiler warnings.	2017-02-18 14:26:31 -08:00