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

32 Commits

Author SHA1 Message Date
Jannis Harder 5444cf281c Improved anytime pdr 
(cherry picked from commit c832967200)
 2024-08-07 15:46:44 +02:00
Alan Mishchenko 29cb71f98b Integrating Satoko into pdr. 2017-08-16 12:08:55 +07:00
Alan Mishchenko d877074d8f Improvements to ternary simulation. 2017-03-09 22:53:47 -08:00
Alan Mishchenko 632ca7ed11 Promising alternative of CEX minimization in 'pdr'. 2017-02-16 13:37:46 -08:00
Alan Mishchenko ab387953ab Word-level abstraction engine. 2017-02-15 17:16:19 -08:00
Alan Mishchenko dd96bb7477 Adding PDR with abstraction. 2017-02-10 18:53:39 -08:00
Alan Mishchenko 8bff9aa1cd Adding PDR with abstraction. 2017-02-10 17:36:20 -08:00
Alan Mishchenko fce2b16a60 Re-introducing floating-point activity in the SAT solver. 2017-02-10 13:31:29 -08:00
Alan Mishchenko 89e8e50069 Improving new X-valued simulation in 'pdr'. 2017-02-06 00:21:28 -08:00
Alan Mishchenko 8b6de217f6 Compiler warnings. 2017-02-05 11:08:44 -08:00
Alan Mishchenko 2c4c464ab0 Adding structural flop priority heuristics in 'pdr' (bug fix). 2017-02-03 21:31:40 -08:00
Alan Mishchenko 45bf0369a8 Adding structural flop priority heuristics in 'pdr'. 2017-02-03 19:51:53 -08:00
Alan Mishchenko a2cebd3e20 Removing dead code in 'pdr'. 2017-02-03 17:32:44 -08:00
Alan Mishchenko 6d088bc440 Enabling new X-valued simulation in 'pdr'. 2017-02-03 17:02:36 -08:00
Alan Mishchenko c4446189a9 Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network. 2016-01-14 20:42:22 -08:00
Alan Mishchenko 1c56a92a6c Undoing previous change, which was made by mistake. 2014-03-31 22:16:47 -07:00
Alan Mishchenko 679e38b012 Making per-output timeout in bmc3 -a and pdr -a work in CLOCKS_PER_SECs instead of miliseconds. 2014-03-31 22:03:22 -07:00
Alan Mishchenko 37fd73cf9e Adding new code to verify invariant derived by 'pdr'. 2014-03-30 14:10:12 -07:00
Alan Mishchenko e87f0dd679 Bug fix in PDR. 2013-09-16 08:49:37 -07:00
Alan Mishchenko ab5c1692db Handling the case when all outputs are undecided in 'pdr -a' with per-output timeout. 2013-09-14 12:23:46 -07:00
Alan Mishchenko 35273eaeba Small data-structure improvements in 'pdr'. 2013-07-19 14:08:21 -07:00
Alan Mishchenko 19c25fd6aa Adding a wrapper around clock() for more accurate time counting in ABC. 2013-05-27 15:09:23 -07:00
Alan Mishchenko 760c1f60d2 Adding new command &mprove for proving groups of properties. 2013-05-17 11:50:16 -07:00
Alan Mishchenko 7c7d527755 Changing per-output runtime limit to be in miliseconds. 2013-05-09 11:35:04 -07:00
Alan Mishchenko 50095be5ac Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>). 2013-05-03 19:58:25 -07:00
Alan Mishchenko 58d4012a55 Enabling multi-output solving in 'pdr'. 2012-12-09 14:46:16 -08:00
Alan Mishchenko b65ae7349a Enabling multi-output solving in 'pdr'. 2012-12-09 09:47:48 -08:00
Alan Mishchenko 117bc0dbcd Prepared &gla to try abstracting and proving concurrently. 2012-09-14 21:20:37 -07:00
Alan Mishchenko e80bd69ed6 Adding flushing stdout after printing verbose stats. 2012-07-07 20:41:16 -07:00
Alan Mishchenko e484231598 Fixing time printouts in 'pdr'. 2012-07-07 09:16:41 -07:00
Alan Mishchenko c47dc99a94 Redirecting printf messages. 2012-03-02 01:15:40 -08:00
Alan Mishchenko 8014f25f6d Major restructuring of the code. 2012-01-21 04:30:10 -08:00