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

3874 Commits

Author SHA1 Message Date
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
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 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
Alan Mishchenko f7a1fe88fb Merged in boschmitt/abc (pull request #51) 
Modifications to satoko.
 2017-02-11 01:41:19 +00:00
Alan Mishchenko 1bdbea6612 Compiler warnings. 2017-02-10 17:40:34 -08:00
Alan Mishchenko 8bff9aa1cd Adding PDR with abstraction. 2017-02-10 17:36:20 -08:00
Bruno Schmitt d69735309d Merged alanmi/abc into default 2017-02-10 17:28:17 -08:00
Bruno Schmitt 342d2d9f5c New fixed point data type. 
Expose all options to command line.
Expose search statistics to users.
 2017-02-10 17:26:45 -08:00
Alan Mishchenko fce2b16a60 Re-introducing floating-point activity in the SAT solver. 2017-02-10 13:31:29 -08:00
Alan Mishchenko f2d096c9f0 Improving CEX minimization. 2017-02-10 13:20:20 -08:00
Alan Mishchenko d335ee096e Standardizing the use of new CNF generator. Adding CNF variable connectivity information. 2017-02-10 11:05:00 -08:00
Alan Mishchenko 4e6978f242 Profiling CEX minimization. 2017-02-09 18:05:55 -08:00
Alan Mishchenko 7a2984bbe9 Word-level abstraction. 2017-02-09 16:38:08 -08:00
Alan Mishchenko 2fe17c1f4b Word-level abstraction. 2017-02-09 14:30:10 -08:00
Alan Mishchenko 32712ec9ab Making sure 'inv_out' can match flops by name. 2017-02-09 14:17:19 -08:00
Alan Mishchenko e20ef654d9 Word-level abstraction. 2017-02-09 13:31:07 -08:00
Bruno Schmitt 871899dcea - Adding a compile time option to use floats for var activity (now it can be either ‘double’, ‘float’ or ‘unsigned’ (default)) 
- Adding vector of ‘float’
- Adding an option to configure the ratio of learnt clauses to be kept in clause database at each reduction (0 means no reduction).
- Other small changes.
 2017-02-09 05:17:50 -08:00
Alan Mishchenko 040b88a7c6 Editing output messages. 2017-02-08 19:12:57 -08:00
Alan Mishchenko 2a9902eec7 Accidental change. 2017-02-08 19:10:15 -08:00
Alan Mishchenko 778ea6bb8a Editing output messages. 2017-02-08 19:07:21 -08:00
Alan Mishchenko 1e62fb4a92 Compiler warning. 2017-02-08 18:59:07 -08:00
Alan Mishchenko 77e2b1ff53 Autotuner for 'satoko'. 2017-02-08 18:57:16 -08:00
Alan Mishchenko cf24a0eb0c Compiler warning. 2017-02-08 14:12:49 -08:00
Alan Mishchenko de4bf41c53 New command &satoko. 2017-02-08 14:10:08 -08:00
Alan Mishchenko 80f5070dbe Re-introducing floating-point activity in the SAT solver. 2017-02-07 02:05:03 -08:00