luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
3,946 Commits 27 Branches 57 Tags 58 MiB
Commit Graph

3946 Commits

Author SHA1 Message Date
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
Alan Mishchenko 429f52ce15 Experiments with SAT sweeping. 2017-02-18 14:20:10 -08:00
Yen-Sheng Ho b93a805129 copied some functions from pdr 2017-02-18 12:43:03 -08:00
Yen-Sheng Ho 91a0a0fc3b copied pdr_mansolve 2017-02-18 10:28:16 -08:00
Yen-Sheng Ho 196b359183 started pdrIncr.c 2017-02-18 09:51:54 -08:00
Yen-Sheng Ho 16fda0bd24 added a simple example; edited hgignore 2017-02-18 09:10:45 -08:00
Yen-Sheng Ho 1d3ff5338a added ipdr 2017-02-17 18:55:00 -08:00
Alan Mishchenko bc010af4be Promising modification of the generalization procedure in 'pdr'. 2017-02-17 14:10:32 -08:00
Alan Mishchenko 378af9d94f Experiment with graph constuction using ZDDs. 2017-02-17 14:09:58 -08:00
Alan Mishchenko 6d6bf8740d Fixing missing sat_solver APIs in 'iprove'. 2017-02-16 13:57:36 -08:00
Alan Mishchenko 632ca7ed11 Promising alternative of CEX minimization in 'pdr'. 2017-02-16 13:37:46 -08:00
Alan Mishchenko 61b665ac8d Experiment with graph constuction using ZDDs. 2017-02-16 11:38:06 -08:00
Alan Mishchenko 408ce46815 Fixing memory leak in 'pdr'. 2017-02-16 10:28:39 -08:00
Alan Mishchenko c7b68c5e3f Promising modification of the generalization procedure in 'pdr'. 2017-02-16 10:03:34 -08:00
Alan Mishchenko bcc6d2686f Fixing missing sat_solver APIs in 'iprove'. 2017-02-15 19:12:47 -08:00
Bruno Schmitt 7811f1bb07 Merged alanmi/abc into default 2017-02-15 17:19:52 -08:00
Alan Mishchenko ab387953ab Word-level abstraction engine. 2017-02-15 17:16:19 -08:00
Bruno Schmitt 088aabc102 - Small changes to the watch lists behavior. 
- Implementation of bookmark, unbookmark and rollback procedures.
- Minor changes.
 2017-02-15 17:02:32 -08:00
Alan Mishchenko cb1ab7030f Experiments with simulation. 2017-02-14 20:26:43 -08:00
Bruno Schmitt 30037e0653 - Small bug fix in var activity (improve performance) 
- New implementation of watcher lists.
 2017-02-14 14:43:44 -08:00
Alan Mishchenko f4853496d7 Adding PDR with abstraction. 2017-02-13 01:02:03 -08:00
Alan Mishchenko 3fb058a355 Adding PDR with abstraction. 2017-02-11 22:48:20 -08:00
Alan Mishchenko 4abb1ce8a4 Commenting out uncommented message. 2017-02-11 21:11:45 -08:00
Alan Mishchenko ae521b6601 Adding PDR with abstraction. 2017-02-11 21:00:37 -08:00
Alan Mishchenko 2a5fa67d36 Adding APIs to mark cones. Creating test-bench for incremental solving &satoko -i. 2017-02-11 17:28:37 -08:00
Alan Mishchenko 7b7ebf91e4 Compiler warning. 2017-02-11 15:40:53 -08:00
Alan Mishchenko f6193c0d45 Updates to variable activity in the SAT solver. 2017-02-11 15:38:50 -08:00
Alan Mishchenko 45f4d6c7e8 Movinng custom floating-point implementations, etc. 2017-02-11 13:55:41 -08:00
Bruno Schmitt ab2d3acac9 New implementation of a software floating point implementation (sdbl) for consistency across different platforms and compilers. 
Removing useless files and compile time options related to variable activity data type (it can only be sdbl).
 2017-02-11 13:28:22 -08:00
Alan Mishchenko 8333cb807f Platform-independent double. 2017-02-11 10:55:34 -08:00
Alan Mishchenko dd96bb7477 Adding PDR with abstraction. 2017-02-10 18:53:39 -08:00
Alan Mishchenko 5d717256d3 Updates to the autotuner. 2017-02-10 18:14:06 -08:00
Alan Mishchenko d4b491d849 Changes to compile on Windows. 2017-02-10 17:51:42 -08:00