Commit Graph

350 Commits

Author SHA1 Message Date
Alan Mishchenko 87d39b40aa Missing type cast after one of the previous changes. 2011-03-04 17:11:33 -08:00
Alan Mishchenko ef89333774 Improved the speed of refinement algorithm in &abs_refine. 2011-03-04 16:59:28 -08:00
Alan Mishchenko 148a786b69 Made abc.h independent of CUDD and Extra. 2011-03-03 12:28:52 -08:00
Alan Mishchenko 88bdf467d8 Bug fix in dprove, adding command option -p. 2011-03-03 10:02:32 -08:00
Alan Mishchenko d13bbe5b5f Bug fix in &fraig. 2011-03-03 10:01:28 -08:00
Alan Mishchenko f2945e12f3 Upgrading epd and mtr packages to be compatible with the latest release of CUDD 2.4.2 2011-03-02 19:02:04 -08:00
Alan Mishchenko e3f2dde1c4 Upgrading epd and mtr packages to be compatible with the latest release of CUDD 2.4.2 2011-03-02 18:50:03 -08:00
Alan Mishchenko e881eaf693 Removing useless printout in &resim. 2011-03-02 18:48:51 -08:00
Alan Mishchenko de984d7f90 Fixing corner-case bugs in &srm -s. 2011-02-28 21:55:40 -08:00
Alan Mishchenko 6119f7068a Cumulative update to BDD-based reachability, speeding up &reachm and other changes. 2011-02-28 14:52:51 -08:00
Alan Mishchenko 39839c3feb Updated read_status/write_status to correctly handle the case of seq cex without regs. 2011-02-27 20:57:27 -08:00
Alan Mishchenko 4704dbc798 Replaced remove() by unlink() to compile on Windows. 2011-02-27 20:43:02 -08:00
Baruch Sterin 34d59b0b91 fixes to pyabc kill mechanism 2011-02-27 18:33:56 -08:00
Alan Mishchenko 02081dba67 Added generation of counter-examples in &reachm. 2011-02-27 17:05:44 -08:00
Alan Mishchenko 2f874d27fc Fixed the problem with filtered equivalences (&srm -sf and &equiv_mark -f). 2011-02-22 12:47:55 -08:00
Alan Mishchenko a84b1cfc55 Fixed a critical bug in the previous update. 2011-02-21 21:32:28 -08:00
Alan Mishchenko 75ee395f91 Implemented additional filtering of equivalences (&srm -sf). 2011-02-21 15:09:51 -08:00
Alan Mishchenko ab75993d28 Moved two new APIs for reading/writing CEX from/into ABC from abc.c to mainFrame.c. 2011-02-19 16:53:11 -08:00
Alan Mishchenko e3f88c81c6 Changes to support sequential verification with reduction without speculation. 2011-02-19 16:47:05 -08:00
Alan Mishchenko 2619edf8c0 Added two new APIs for reading/writing CEX from/into ABC. 2011-02-19 16:43:00 -08:00
Alan Mishchenko 443cc01782 Another corner-case bug in zeropo. 2011-02-19 13:24:21 -08:00
Alan Mishchenko 0656af22fd Adding one more control switch to CEC commands (i)prove. 2011-02-19 11:51:20 -08:00
Alan Mishchenko c7ebd93211 Improvements to CEC command iprove. 2011-02-18 22:19:45 -08:00
Alan Mishchenko 06ae1644b2 Fixing the problem with writing/reading bug-free depth in status files. 2011-02-17 09:18:07 -08:00
Alan Mishchenko 5b4ef503bd Fixed Cudd_DumpDot() to not print leading zeros because of OS-dependent fprintf switch %p. 2011-02-16 12:21:58 -08:00
Baruch Sterin 9d02679ef7 fixes for dumb erros in utilSignal.c/h 2011-02-15 16:50:12 -08:00
Alan Mishchenko a7e214bb01 Improved timeout in the BDD reachability engines. 2011-02-13 20:50:29 -08:00
Alan Mishchenko 573694f9bf Fixing g++ compilation issue for tmpFile(). 2011-02-13 19:48:30 -08:00
Alan Mishchenko 8cc7b43865 Unified the use of counter-examples in three packages (additional files). 2011-02-13 18:02:52 -08:00
Alan Mishchenko 71cbf17e7f Unified the use of counter-examples in three packages. 2011-02-13 17:46:48 -08:00
Alan Mishchenko 686d38d667 Changes to enable C++ compilation after recent modifications. 2011-02-13 15:16:10 -08:00
Alan Mishchenko 8acd4edd5a Removing 1.txt, which was added by mistake. 2011-02-13 13:43:14 -08:00
Alan Mishchenko e7b544f111 Upgrade to the latest CUDD 2.4.2. 2011-02-13 13:42:25 -08:00
Alan Mishchenko d99de60e6c Portability changes to the st package. 2011-02-13 13:40:21 -08:00
Alan Mishchenko 350bedf53f Minor change to the project file. 2011-02-13 13:39:56 -08:00
Alan Mishchenko bef084bd9b Bug fix in setting the number of finished frames when reading a status file. 2011-02-11 13:57:57 -08:00
Alan Mishchenko 78aed3f6d5 LUT-size-based balancing (disabled by default). 2011-02-11 09:11:30 -08:00
Alan Mishchenko 2a214a9283 Bug fix in zeropo. 2011-02-11 09:10:34 -08:00
Alan Mishchenko f74fb87dae Improved timeout in &reachp. 2011-02-08 12:45:28 -08:00
Alan Mishchenko ed253df750 Additional change to enable runtime limit in CUDD in variable reordering. 2011-02-08 12:43:32 -08:00
Alan Mishchenko 46075098da Improved timeout in &reachm. 2011-02-08 11:36:02 -08:00
Alan Mishchenko 7977b2dd5d Modificationd to CUDD to enable runtime-limit in variable reordering. 2011-02-08 11:09:12 -08:00
Alan Mishchenko 53217cdc8b Yet another update to the runtime control in BDD operations. 2011-02-07 20:37:53 -08:00
Alan Mishchenko 21bb515b3c Added handling runtime limit inside And and AndExist. 2011-02-07 15:58:29 -08:00
Alan Mishchenko 3e92b87362 Added timeout to &reachn. 2011-02-04 20:22:10 -08:00
Alan Mishchenko 82e9de9000 Eneabled writing/reading pAbc->nFrames into/from status files. 2011-02-04 00:07:21 -08:00
Alan Mishchenko e5fb4fe550 Added writing signal names in AIGER writer for GIA package. 2011-02-03 22:11:47 -08:00
Alan Mishchenko e6f8744777 Make PDR return the number of completed frames. 2011-02-03 21:34:46 -08:00
Alan Mishchenko 59d7455cf1 Minor changes while improving BDD-based reachability. 2011-02-03 13:05:01 -08:00
Alan Mishchenko 1d54983bc4 Minor changes to hash table and utilSignal.c. 2011-02-01 16:35:50 -08:00