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

437 Commits

Author SHA1 Message Date
Alan Mishchenko 63ce84d824 Implementation of CE extraction for multiple MUXes driving D-inputs of FFs. 2015-01-08 16:30:32 -08:00
Alan Mishchenko 4af39856b2 Returning multiple counter-examples. 2015-01-03 22:59:34 -08:00
Alan Mishchenko 3b9e363ef2 Returning multiple counter-examples. 2015-01-03 22:53:58 -08:00
Alan Mishchenko b94b7852d7 Bug fix in &fftest when used for ECO. 2014-12-10 18:55:12 -08:00
Alan Mishchenko ad7c8d6382 Experimental implementation of BMC-related procedures. 2014-11-05 09:29:00 -08:00
Alan Mishchenko 8c2e51824e Experimental implementation of BMC-related procedures. 2014-11-04 20:35:36 -08:00
Alan Mishchenko d75b8ce874 Compiler warnings. 2014-11-03 18:10:36 -08:00
Alan Mishchenko 93754146a4 Bug fix in CEX printing. 2014-11-03 16:45:09 -08:00
Alan Mishchenko 505747d443 Improvements to &fftest (adding computation of fixed parameters). 2014-11-02 21:43:49 -08:00
Alan Mishchenko 135bf3ecdf Compiler warnings. 2014-10-28 23:53:17 -07:00
Alan Mishchenko e2b8d95b6f Bug fix in bmc3 -a -x. 2014-10-28 19:49:32 -07:00
Alan Mishchenko 4edc023479 Bug fix in bmc3 -a -x. 2014-10-28 18:28:21 -07:00
Alan Mishchenko f93ede121d Adding switch &fftest -N <num> to detect fixed vars after each <num> iterations. 2014-10-25 17:07:38 -07:00
Alan Mishchenko 5c93850553 Compiler problems. 2014-10-21 20:24:13 -07:00
Alan Mishchenko c49f35835b Compiler problems. 2014-10-21 20:20:22 -07:00
Alan Mishchenko 5bd9edb52d Compiler problems. 2014-10-21 20:18:14 -07:00
Alan Mishchenko 5ae8a37d9d Compiler problems. 2014-10-21 20:13:25 -07:00
Alan Mishchenko 228dbcc51e Adding code of MiniSAT 2.2. 2014-10-21 19:45:52 -07:00
Alan Mishchenko ccb5bb34d7 Suggested patch for type-punned warnings 2014-10-10 08:58:18 -07:00
Alan Mishchenko 65f9b73505 Changing default CNF generation in &bmc. 2014-08-18 20:19:32 -07:00
Alan Mishchenko 68ce0bc1c1 Adding delay optimization to synthesis script &syn2. 2014-08-08 12:45:28 -07:00
Alan Mishchenko 9790867817 Fix to the problem of not dumping test-vectors in &fftest when the use-specified test set is complete or when a timeout occurred. 2014-06-30 10:57:33 -07:00
Alan Mishchenko 44d9c7e543 Improvements to CNF generation. 2014-06-23 13:11:59 -07:00
Alan Mishchenko cf993a9d90 Adding more features to the synthesis script &syn2. 2014-06-14 19:03:05 -07:00
Alan Mishchenko b844433a0d Adding CEC command &splitprove. 2014-06-04 15:00:38 -07:00
Alan Mishchenko ed1a925c61 Adding symbolic fault representation in &fftest. 2014-05-23 00:13:03 +09:00
Alan Mishchenko 824ee5b4f3 Adding symbolic fault representation in &fftest. 2014-05-22 15:59:01 +09:00
Alan Mishchenko 8160721240 Experiment with support minimization. 2014-05-21 22:11:44 +09:00
Alan Mishchenko ab85108c62 Simple version of ECO. 2014-05-21 12:41:34 +09:00
Alan Mishchenko 368de31ae2 Simple version of ECO. 2014-05-21 12:40:20 +09:00
Alan Mishchenko fb10d54bf5 Adding symbolic fault representation in &fftest. 2014-05-20 23:35:58 +09:00
Alan Mishchenko f30160f4be Adding symbolic fault representation in &fftest. 2014-05-19 21:10:19 +09:00
Alan Mishchenko 911b801f20 Adding symbolic fault representation in &fftest. 2014-05-14 20:28:55 +09:00
Alan Mishchenko 22ada3b2b7 Adding command to dump UNSAT core of BMC instance. 2014-04-07 14:20:25 -07:00
Alan Mishchenko 7753e097f9 Adding command to dump UNSAT core of BMC instance. 2014-04-07 14:13:06 -07:00
Alan Mishchenko 42927d5ebb Adding command to dump UNSAT core of BMC instance. 2014-04-07 14:10:51 -07:00
Alan Mishchenko f6ae0e41f3 Better CEX minimization and renaming of write_counter into write_cex. 2014-04-04 13:14:16 -07:00
Alan Mishchenko 329cdc3565 Compiler warnings. 2014-04-01 11:58:36 -07:00
Alan Mishchenko 7b8863466e Adding switch to handle only single faults. 2014-04-01 11:53:08 -07:00
Alan Mishchenko 41e94c474a Updating logic file print-out. 2014-03-31 23:26:21 -07: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 90867a64b4 Adding functionally observable fault testing. 2014-03-31 21:33:45 -07:00
Alan Mishchenko fa1fafe4de Adding functionally observable fault testing. 2014-03-31 21:33:02 -07:00
Alan Mishchenko 37fd73cf9e Adding new code to verify invariant derived by 'pdr'. 2014-03-30 14:10:12 -07:00
Alan Mishchenko 7d500c8920 Updating &if for new cut function representation. 2014-03-29 22:14:15 -07:00
Alan Mishchenko 14f69d77fd Adding per-output logging to bmc3. 2014-03-29 10:28:20 -07:00
Alan Mishchenko c0f688349d Adding a feature to dump untestable multiple faults. 2014-03-28 13:47:00 -07:00
Alan Mishchenko c6663b04c7 Experiments with stuck-at fault testing. 2014-03-24 22:48:37 -07:00
Alan Mishchenko b13e65882d Experiments with stuck-at fault testing. 2014-03-23 10:47:08 -07:00