Commit Graph

361 Commits

Author SHA1 Message Date
Alan Mishchenko 52a8ebb451 Adding bit-blasting of sqrt using non-restoring algorithm (Parhami, 2nd ed, p. 452) 2019-10-05 17:30:56 -07:00
Alan Mishchenko 395614a4dd Fixing performance bug (too many partial products) in blasting signed Booth multiplier. 2019-09-19 07:53:21 -07:00
Alan Mishchenko 9754572283 Adding switch to suppress printing simple objects in %retime. 2019-08-14 19:55:16 +07:00
Alan Mishchenko ee1bd8f0be Fixing some update gcc. 2019-07-24 11:44:28 +07:00
Alan Mishchenko d1b6413d1c Fix index of delay tables created by %blast. 2019-04-16 21:37:45 -07:00
Alan Mishchenko 812821554c Adding miter construction with one bit-level output for each pair of word-level outputs. 2019-04-14 20:45:24 -07:00
Alan Mishchenko 362b2d9d08 Supporting LUT in NDR and WLC. 2019-04-05 21:08:46 -10:00
Alan Mishchenko c24fd01f19 Recognizing async reset in blasting (the case of constant 0 driver). 2019-04-02 17:43:57 -10:00
Alan Mishchenko acdfc3cc9f Recognizing async reset in blasting. 2019-03-26 13:20:39 -07:00
Alan Mishchenko 911c11afeb Adding support for LUT primitive in NDR. 2019-03-20 11:40:44 +02:00
Alan Mishchenko b78ec9db14 Adding support for LUT primitive in NDR. 2019-03-20 11:38:51 +02:00
Alan Mishchenko 9842e82326 Bug in handling reverse ranges in blasting. 2019-03-04 13:39:38 -08:00
Alan Mishchenko 4d838e7513 Bug fix in generating box library. 2019-02-04 14:03:09 -08:00
Alan Mishchenko 7b419f9041 Compiler warning. 2019-02-01 19:24:55 -08:00
Alan Mishchenko 0699c43ac5 Experiments with memory abstraction. 2019-01-27 21:57:18 -08:00
Alan Mishchenko 82eead0817 Experiments with memory abstraction. 2019-01-22 22:49:36 -08:00
Alan Mishchenko f86cfc937e Experiments with memory abstraction. 2019-01-22 22:44:07 -08:00
Alan Mishchenko 72e3b4ca78 Fixing flop names with reversed ranges. 2019-01-21 15:15:11 -08:00
Alan Mishchenko b3d81b5f76 Exploring other ways of CEX writing. 2019-01-21 14:57:05 -08:00
Alan Mishchenko d4ce4cc982 Undoing some recent changes for improved CEX writing. 2019-01-21 11:49:35 -08:00
Alan Mishchenko f421d2a113 Fixing the problem with outputting word-level CEXes after retiming. 2019-01-18 19:54:41 -08:00
Alan Mishchenko 4d8c72d0e9 Fixing the problem with outputting word-level CEXes after retiming. 2019-01-17 11:07:31 -08:00
Alan Mishchenko d05f89d997 Fixing the problem with outputting word-level CEXes. 2019-01-16 17:57:40 -08:00
Alan Mishchenko 7f778ff805 Procedure to transform counter-examples (bug fix). 2019-01-15 19:08:24 -08:00
Alan Mishchenko f3946eea93 Procedure to transform counter-examples (bug fix). 2019-01-15 18:59:34 -08:00
Alan Mishchenko 36e5badf05 Procedure to trasnsform counter-examples. 2019-01-15 17:30:39 -08:00
Alan Mishchenko d071e02616 Updated for memory abstraction. 2018-12-11 16:52:46 -08:00
Alan Mishchenko 36585eff57 Experiments with retiming (adding new APIs). 2018-12-09 15:18:12 -08:00
Alan Mishchenko a3253767b9 Experiments with retiming. 2018-12-06 23:13:16 -08:00
Alan Mishchenko 65b10c0327 Experiments with retiming. 2018-12-04 23:04:13 -08:00
Alan Mishchenko 5aa3025ce7 Adding switch &w -n to modify the comment section of the AIGER file written. 2018-11-21 13:12:01 -08:00
Alan Mishchenko 12908d3c25 Various usability changes. 2018-11-18 21:01:30 -08:00
Alan Mishchenko 4d56acfd5a Several recent bug fixes. 2018-11-04 20:24:33 +08:00
Alan Mishchenko 9e787c7191 Experiments with word-level retiming. 2018-09-30 20:51:37 -07:00
Alan Mishchenko 563f4a8a56 New way of blasting complex flops. 2018-09-25 20:53:18 -07:00
Alan Mishchenko a93699f696 New way of blasting complex flops. 2018-09-24 21:38:12 -07:00
Alan Mishchenko fea47821f5 New way of blasting complex flops. 2018-09-24 21:34:33 -07:00
Alan Mishchenko a2258f5ee6 Support for flops with complex controls. 2018-09-22 17:40:41 -07:00
Alan Mishchenko a9815b75ab Adding dump of name mapping after blasting. 2018-09-21 18:07:21 -07:00
Alan Mishchenko c5f74867b2 Fixing a memory leak. 2018-09-19 19:01:07 -07:00
Alan Mishchenko c9e520e2dc Expriments with functions. 2018-09-16 13:52:59 -07:00
Alan Mishchenko caaca11032 Supporting unitialized flops in NDR. 2018-09-11 22:20:09 +03:00
Alan Mishchenko 2c73723b74 Skip non-driven nodes during DFS. 2018-08-26 19:01:20 +07:00
Alan Mishchenko 28a1307a61 Command %blastmem for bit-blasting small memories. 2018-06-16 18:47:23 -07:00
Alan Mishchenko f4a267d581 Bug fix in 'lutpack' (level count overflow). 2018-06-16 14:52:20 -07:00
Alan Mishchenko 15939511df Extending NDR to support adder/subtractor. 2018-06-14 21:13:54 -07:00
Alan Mishchenko dca2218275 Compiler warnings. 2018-06-08 12:30:13 -07:00
Alan Mishchenko d06d78363c Improvements in bit-blasting of adders and multipliers. 2018-06-08 12:11:40 -07:00
Alan Mishchenko 867600b766 Supporting the decoder primitive in NDR and bit-blasting. 2018-06-05 16:23:04 -07:00
Alan Mishchenko 5b588e0951 Exposing a switch to generate carry-lookahead adder during bit-blasting. 2018-06-05 13:49:23 -07:00
Alan Mishchenko 6df1396273 Supporting SEL in bit-blasting. 2018-05-25 12:47:36 +09:00
Alan Mishchenko 21c7dad7e4 Supporting NMUX and SEL in NDR. 2018-05-24 19:36:28 +09:00
Alan Mishchenko d9e68f60c8 Bug fix in supporting signed multiplication in NDR. 2018-05-18 09:54:06 +09:00
Alan Mishchenko eb027885ee Supporting wide MUX in NDR. 2018-05-16 15:52:08 +09:00
Alan Mishchenko 03b17916f8 Bug fix in the naming of outputs in %blast -d. 2018-05-10 18:55:46 -07:00
Alan Mishchenko aa313189c4 Updates to NDR format (bug fixes). 2018-05-03 22:28:21 -07:00
Alan Mishchenko f23ea8e33f Updates to NDR format (flops, memories, signed mult, etc). 2018-04-29 15:14:01 -07:00
Alan Mishchenko 0e15e4dd15 Memory abstraction. 2018-04-20 16:06:13 -07:00
Alan Mishchenko 1c6655578c Memory abstraction. 2018-04-19 17:05:04 -07:00
Alan Mishchenko 098103012d Memory abstraction. 2018-04-15 21:23:22 -07:00
Alan Mishchenko 69416b7ca1 Temporary bug fix for signal names in WLC (correction). 2018-03-21 20:52:36 -07:00
Alan Mishchenko d410faf85c Temporary bug fix for signal names in WLC. 2018-03-21 20:18:17 -07:00
Alan Mishchenko 3d16d44cff Bug fix in blasting with boxes. 2018-03-06 23:21:49 -08:00
Alan Mishchenko 48e128aa72 Extending primitives supported by WLC. 2018-03-03 17:57:30 -08:00
Alan Mishchenko f6b9cc013d Adding parameters and improvements to %blast. 2018-02-28 19:38:55 -08:00
Alan Mishchenko 7e9f3f027b Adding parameters and improvements to %blast. 2018-02-28 18:45:44 -08:00
Alan Mishchenko 33971604cf Adding support for adders with carry-in in WLC and NDR. 2018-02-24 09:50:24 -08:00
Alan Mishchenko fe56e29d44 Bug fix in NDR handling. 2018-02-20 16:56:52 -08:00
Alan Mishchenko 76b00a2d3e Compilation problem with pow(). 2018-02-19 09:07:44 -08:00
Alan Mishchenko c6bce9c20e Fixing input swapping issue in MUXes derived from NDR. 2018-02-07 09:02:28 -08:00
Alan Mishchenko 3202c2581e Improvements to NDR to represent hierarchical designs. 2018-02-05 00:37:39 -08:00
Alan Mishchenko 30a06d002a Adding support of reading and writing designs using a new internal format (bug fix). 2018-01-29 17:01:01 -08:00
Alan Mishchenko 99ddb64095 Adding support of reading and writing designs using a new internal format. 2018-01-28 18:53:20 -08:00
Alan Mishchenko f06056d85d Changes to 'pdr' to run with updated Satoko. 2017-09-06 08:34:04 -07:00
Alan Mishchenko 4886a4ef4c Adding new type of MUX blasting. 2017-07-07 23:40:59 -07:00
Yen-Sheng Ho 584e28e8f4 merge 2017-06-06 23:16:55 -07:00
Yen-Sheng Ho 10f5e944c9 %pdra: fixed a bug 2017-06-06 23:15:38 -07:00
Alan Mishchenko e140ef7e5a Bug fix in SMT handling: 'distinct' with more than two inputs. 2017-06-05 12:36:26 +02:00
Alan Mishchenko 41314cea01 Adding switch %blast -d to dump dual-output miter after blasting. 2017-04-29 18:34:56 -07:00
Yen-Sheng Ho 38e5c8c9e6 %pdra: added an option for disabling incremental solving 2017-04-16 22:03:47 -07:00
Yen-Sheng Ho 0f1a758c2f %pdra: bug fix 2017-04-09 17:59:34 -07:00
Yen-Sheng Ho 3c43851c36 %pdra: bug fix 2017-04-09 17:22:14 -07:00
Yen-Sheng Ho 3401ed364b %pdra: added top level callbacks 2017-04-09 14:38:37 -07:00
Yen-Sheng Ho 2761e5e35b small changes 2017-04-06 14:18:28 -07:00
Yen-Sheng Ho 131a51a4b5 %pdra: handled real CEXs; refactor 2017-04-06 14:15:26 -07:00
Yen-Sheng Ho 1531dd8ec5 %pdra: added an option -t for disabling trace reuse 2017-03-31 15:34:21 -07:00
Yen-Sheng Ho 04bd8631e0 merge 2017-03-31 07:42:06 -07:00
Yen-Sheng Ho 16ef095f9c %pdra: fixed bugs 2017-03-30 15:22:39 -07:00
Alan Mishchenko 96056c377c Experiments with multipliers. 2017-03-30 14:53:35 -07:00
Yen-Sheng Ho 1cb140bb11 %pdra: fixed bugs 2017-03-30 13:53:18 -07:00
Yen-Sheng Ho 4d47904831 %pdra: fixed bugs 2017-03-29 14:20:40 -07:00
Alan Mishchenko 7285f1051e Experiments with multipliers. 2017-03-28 23:28:04 -07:00
Yen-Sheng Ho bf4be3fc25 %pdra: improved performance 2017-03-28 15:20:53 -07:00
Yen-Sheng Ho 2fea987ec6 %pdra: added an option -s 2017-03-28 14:08:04 -07:00
Yen-Sheng Ho 7a423e4fbe %pdra: added a procedure to shrink abstraction 2017-03-27 17:09:23 -07:00
Yen-Sheng Ho 758270d663 %pdra: refactor 2017-03-27 15:18:35 -07:00
Yen-Sheng Ho e6098d20be %pdra: added a procedure to rebuild traces 2017-03-27 15:10:33 -07:00
Alan Mishchenko d0ea4853ec Experiments with multipliers. 2017-03-26 14:38:04 -07:00
Yen-Sheng Ho 875411985c %pdra: working on bmc3 2017-03-19 14:21:19 -07:00
Yen-Sheng Ho 51fbf37cb4 %pdra: working on bmc3 2017-03-19 12:41:06 -07:00