Alan Mishchenko
|
095345fc4a
|
Added new name manager and modified hierarchy manager to use it.
|
2012-01-13 15:43:09 -08:00 |
Alan Mishchenko
|
cb2d12bb04
|
New hierarchy manager.
|
2012-01-13 00:34:13 -08:00 |
Alan Mishchenko
|
2e1dcdd239
|
Added model ID inside the design.
|
2012-01-12 23:29:47 -08:00 |
Alan Mishchenko
|
fadde52dc6
|
Changes to the lazy man's synthesis code.
|
2012-01-11 22:08:35 -08:00 |
Alan Mishchenko
|
564a3553f0
|
Gate level abstraction.
|
2012-01-08 13:15:03 +07:00 |
Alan Mishchenko
|
376bf3a703
|
Bug fix: changing output number to 0 in the CEX after ORing POs.
|
2012-01-07 11:19:03 +07:00 |
Alan Mishchenko
|
26b87c8c55
|
Added warning when the network from file has no primary inputs.
|
2012-01-06 01:36:08 +07:00 |
Alan Mishchenko
|
aec5d33889
|
Backward reachability using circuit cofactoring.
|
2012-01-01 15:58:17 +07:00 |
Alan Mishchenko
|
1e20e2ccbc
|
Delay optimization using precomputed library.
|
2011-12-30 13:11:52 +07:00 |
Alan Mishchenko
|
655d452cbb
|
Delay optimization using precomputed library.
|
2011-12-30 11:36:25 +07:00 |
Alan Mishchenko
|
6ed8340226
|
Delay optimization using precomputed library.
|
2011-12-30 11:27:12 +07:00 |
Alan Mishchenko
|
64b8aa51e9
|
Delay optimization using precomputed library.
|
2011-12-30 09:54:30 +07:00 |
Alan Mishchenko
|
6c19c1dfed
|
Delay optimization using precomputed library.
|
2011-12-29 21:14:01 +07:00 |
Alan Mishchenko
|
ed13bd16fd
|
New variable-time frame abstraction.
|
2011-12-29 10:13:25 +07:00 |
Alan Mishchenko
|
21df8bf021
|
Experiments with flattening hierarchy.
|
2011-12-28 22:16:04 +07:00 |
Alan Mishchenko
|
1c51d9577d
|
Added switch -n to 'miter' to ignore PI/PO names.
|
2011-12-22 14:55:10 -08:00 |
Alan Mishchenko
|
d0da3a8258
|
Computing interpolants as truth tables.
|
2011-12-22 14:26:47 -08:00 |
Alan Mishchenko
|
82a2495ce9
|
Improvements to hierarchical BLIF parser.
|
2011-12-22 14:26:03 -08:00 |
Alan Mishchenko
|
b3c9609e82
|
Improvements to hierarchical BLIF parser.
|
2011-12-21 12:56:28 -08:00 |
Alan Mishchenko
|
3418a8820a
|
Fixed a bug in matching code.
|
2011-12-17 17:51:13 -08:00 |
Alan Mishchenko
|
f67cb76dff
|
Added optional printout of the hierarchy structure before collapsing.
|
2011-12-15 19:32:05 -08:00 |
Alan Mishchenko
|
2bb95a97d0
|
Adding switch '-W' to fx to control the quality of extracted divisors.
|
2011-12-15 15:44:56 -08:00 |
Alan Mishchenko
|
b63b332bac
|
Trying to make sorting of nodes platform-indendent.
|
2011-12-15 12:42:42 -08:00 |
Alan Mishchenko
|
40ddda3edd
|
Trying to make sorting of nodes platform-indendent.
|
2011-12-15 12:27:35 -08:00 |
Alan Mishchenko
|
bc2f199bd3
|
Started SAT-based reparameterization.
|
2011-12-13 23:38:41 -08:00 |
Alan Mishchenko
|
8fdc5d220f
|
g++ portability changes.
|
2011-12-13 12:17:03 -08:00 |
Alan Mishchenko
|
23af7f9036
|
Added command &read_blif to read hierarchical BLIF directly into the &-space.
|
2011-12-12 19:10:33 -08:00 |
Alan Mishchenko
|
be874a7abe
|
Added command &read_blif to read hierarchical BLIF directly into the &-space.
|
2011-12-12 18:43:49 -08:00 |
Alan Mishchenko
|
ed4f4adeee
|
Added the hierarchy printout.
|
2011-12-11 17:29:25 -08:00 |
Alan Mishchenko
|
eb35f0ef65
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 01:05:18 -08:00 |
Alan Mishchenko
|
beb29257bf
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 00:38:16 -08:00 |
Alan Mishchenko
|
200c5cc659
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 00:37:05 -08:00 |
Alan Mishchenko
|
07405ca1c5
|
Integrated new proof-logging into proof-based gate-level abstraction.
|
2011-12-08 22:42:50 -08:00 |
Alan Mishchenko
|
e84dcb7862
|
g++ portability changes.
|
2011-12-06 16:06:59 -08:00 |
Alan Mishchenko
|
ef37d14bc6
|
Added recording of AIG subgraphs.
|
2011-12-06 15:37:09 -08:00 |
Alan Mishchenko
|
f95e73c40b
|
Added recording of AIG subgraphs.
|
2011-12-06 14:29:32 -08:00 |
Alan Mishchenko
|
0f8b68aef8
|
Performance bug fix in SOP balancing.
|
2011-12-06 13:15:53 -08:00 |
Alan Mishchenko
|
360c705fc4
|
Added recording of AIG subgraphs.
|
2011-12-06 12:42:00 -08:00 |
Alan Mishchenko
|
d2db956a61
|
Started experiments with a new solver.
|
2011-11-25 18:08:48 -08:00 |
Alan Mishchenko
|
0a5d856cec
|
Making GLA PBA and GLA CBA communicate information.
|
2011-11-22 19:07:00 -08:00 |
Alan Mishchenko
|
30ea50a3b4
|
Temporary debugging change.
|
2011-11-12 23:21:41 -08:00 |
Alan Mishchenko
|
df3e23ae3a
|
Enabled skipping random decisions in PBA, which are performed by default.
|
2011-11-12 17:50:41 -08:00 |
Alan Mishchenko
|
fa96b8d798
|
Do not allow interpolation with constraints.
|
2011-11-12 17:18:49 -08:00 |
Alan Mishchenko
|
c1ac6b9b3e
|
Dump inductive invariant or last interpolant after interpolation.
|
2011-11-12 16:56:41 -08:00 |
Alan Mishchenko
|
3beb36778e
|
Enabled counter-example minimization in 'write_counter'.
|
2011-11-11 20:56:05 -08:00 |
Alan Mishchenko
|
0b73c76380
|
Preventing scripts from aborting if reading has failed.
|
2011-11-08 17:58:51 -08:00 |
Alan Mishchenko
|
55e9c4d0fa
|
Corner case bug in deriving truth table from SOP.
|
2011-11-08 11:36:35 -08:00 |
Alan Mishchenko
|
9a89e3f9f5
|
Changing defaults in gate-level abstraction.
|
2011-11-06 23:35:15 -08:00 |
Alan Mishchenko
|
d2ced9f82e
|
Changes to read multi-output testcases described using AIGER 1.9.
|
2011-11-06 23:15:27 -08:00 |
Alan Mishchenko
|
5b75410a5e
|
Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.
|
2011-10-31 15:04:47 -05:00 |
Alan Mishchenko
|
f08be2742e
|
C++ portability changes.
|
2011-10-27 23:34:11 -07:00 |
Alan Mishchenko
|
bc81cf2dae
|
Improvements to the new abstraction code.
|
2011-10-27 14:20:47 -07:00 |
Alan Mishchenko
|
0f77840520
|
New proof-based abstraction code.
|
2011-10-25 18:32:06 +08:00 |
Alan Mishchenko
|
f7fd329787
|
Improvements to the QBF solver.
|
2011-10-25 17:22:33 +08:00 |
Alan Mishchenko
|
a8e1ba40b9
|
The result of merging with recent PyABC changes.
|
2011-10-25 14:05:50 +08:00 |
Alan Mishchenko
|
f96f3fa583
|
Improvements to the QBF solver.
|
2011-10-24 18:05:45 +08:00 |
Alan Mishchenko
|
9ec9d9f315
|
New abstraction code.
|
2011-10-19 23:45:11 +07:00 |
Alan Mishchenko
|
19ce8396f0
|
New abstraction code.
|
2011-10-19 16:03:15 +07:00 |
Alan Mishchenko
|
397bebf8a5
|
New abstraction code.
|
2011-10-19 15:42:55 +07:00 |
Alan Mishchenko
|
12b70d4946
|
Changes to CNF generation code.
|
2011-10-17 10:39:05 +03:00 |
Alan Mishchenko
|
6f0b87dd5c
|
New abstraction code.
|
2011-10-15 22:04:05 +03:00 |
Alan Mishchenko
|
ad5ee9ff46
|
Changes to the matching procedure.
|
2011-10-12 15:04:41 +03:00 |
Alan Mishchenko
|
924ec940fe
|
Changes to the matching procedure.
|
2011-10-06 15:48:27 +07:00 |
Alan Mishchenko
|
d66b586330
|
Modified write_blif to output LUT structures.
|
2011-10-04 18:43:23 +07:00 |
Alan Mishchenko
|
e6e6a3cf9e
|
Changes to the matching procedure.
|
2011-10-01 17:00:59 +07:00 |
Baruch Sterin
|
ef0fbf0372
|
completely silence the "source" command when the -s option is given
|
2011-10-24 15:21:08 -07:00 |
Alan Mishchenko
|
519b03e8e8
|
Changes to the matching procedure and new abstraction code.
|
2011-09-27 15:10:53 +07:00 |
Alan Mishchenko
|
976f5f5a12
|
Changes to Boolean matching.
|
2011-09-24 20:15:54 -07:00 |
Alan Mishchenko
|
d080336bb5
|
Added new feature to bmc3.
|
2011-09-23 22:35:03 -07:00 |
Alan Mishchenko
|
8f74276edb
|
Initial changes to enable gate-level abstraction.
|
2011-09-22 09:37:44 -07:00 |
Alan Mishchenko
|
c1edeccc60
|
64-bit portability changes.
|
2011-09-17 16:24:40 -07:00 |
Alan Mishchenko
|
8248691d84
|
Added limit on the number of flops to add in one iteration of &abs_refine.
|
2011-09-12 16:46:37 -05:00 |
Alan Mishchenko
|
583bc4d71a
|
Added limit on the number of flops to add in one iteration of &abs_cba.
|
2011-09-11 20:31:25 -05:00 |
Alan Mishchenko
|
a7acb2f104
|
Fixed the problem with blackboxes not preserving their names after duplication.
|
2011-09-08 21:10:36 +07:00 |
Alan Mishchenko
|
11ed724766
|
Added timeout to &abc_pba.
|
2011-09-02 17:09:07 +07:00 |
Alan Mishchenko
|
f8fb154229
|
Change 'testcex' to modify the PO number.
|
2011-08-27 22:44:21 +07:00 |
Alan Mishchenko
|
2adf8dc2fd
|
Sequential cleanup with symbolic/ternary simulation.
|
2011-08-25 17:21:17 +07:00 |
Alan Mishchenko
|
df6d509023
|
Sequential cleanup with symbolic/ternary simulation.
|
2011-08-25 14:14:50 +07:00 |
Alan Mishchenko
|
3469b605e1
|
Sequential cleanup with symbolic/ternary simulation.
|
2011-08-24 17:39:57 +07:00 |
Alan Mishchenko
|
c913fd8849
|
Other changes to enable new features in the mapper (bug fix).
|
2011-08-24 09:33:40 +07:00 |
Alan Mishchenko
|
d79cd4db44
|
Experiments with SPFD-based decomposition.
|
2011-08-21 15:05:44 +07:00 |
Alan Mishchenko
|
21dfaedebd
|
Experiments with SPFD-based decomposition + new K-map print-out.
|
2011-08-20 20:18:31 +07:00 |
Alan Mishchenko
|
b71b5bbc23
|
Bug fix in CBA and PBA.
|
2011-08-18 14:38:02 +07:00 |
Alan Mishchenko
|
48ae2c448f
|
Bug fix in CBA and PBA.
|
2011-08-17 20:49:41 +07:00 |
Alan Mishchenko
|
3344a46b26
|
Added switch '-t' to 'miter' to create regular miter from dual-output miter.
|
2011-08-14 19:22:30 +07:00 |
Alan Mishchenko
|
94726c981b
|
Other changes to enable new features in the mapper (bug fix).
|
2011-08-06 13:28:22 +08:00 |
Alan Mishchenko
|
b9dea5d674
|
Other changes to enable new features in the mapper (bug fix).
|
2011-08-06 01:31:07 +08:00 |
Alan Mishchenko
|
49df91f071
|
Several bug fixes.
|
2011-08-02 12:58:37 +07:00 |
Alan Mishchenko
|
64f31f98bf
|
Added API to access the CEX vector.
|
2011-08-02 12:01:49 +07:00 |
Alan Mishchenko
|
6c6c0b0686
|
Enabled saving vector of counter-examples in the ABC framework.
|
2011-08-02 00:31:03 +07:00 |
Alan Mishchenko
|
4e9f972489
|
Changes to enable CEX minimization.
|
2011-08-01 20:44:13 +07:00 |
Alan Mishchenko
|
961f7532d7
|
Changing the ordering of arguments in two iterators.
|
2011-08-01 13:47:51 +07:00 |
Alan Mishchenko
|
820a147ef1
|
Removed useless typecasts related to changes in Vec_VecEntry().
|
2011-08-01 12:35:34 +07:00 |
Alan Mishchenko
|
81620f2e92
|
Changes to enable CEX minimization.
|
2011-08-01 12:13:49 +07:00 |
Alan Mishchenko
|
34811655f2
|
Minor bug fix in 'testcex'.
|
2011-07-31 20:37:38 +07:00 |
Alan Mishchenko
|
0d65c49048
|
Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed).
|
2011-07-31 20:22:57 +07:00 |
Alan Mishchenko
|
340e4380e9
|
Changes to enable smarter simulation (bug fix).
|
2011-07-30 20:26:17 +07:00 |
Alan Mishchenko
|
43d8b8bece
|
Changes to enable smarter simulation.
|
2011-07-30 20:19:28 +07:00 |
Alan Mishchenko
|
02711b6392
|
Added generation of counter-examples to induction in 'ind'.
|
2011-07-30 19:18:26 +07:00 |
Alan Mishchenko
|
c60852f4a9
|
Changes to enable smarter simulation.
|
2011-07-30 13:37:02 +07:00 |
Alan Mishchenko
|
2ea0ded0bc
|
Changes to enable smarter simulation.
|
2011-07-30 13:30:04 +07:00 |
Alan Mishchenko
|
e4f15dd003
|
Changes to enable smarter simulation.
|
2011-07-30 02:04:54 +07:00 |
Alan Mishchenko
|
badf8e4742
|
Improving and updating the abstraction code.
|
2011-07-29 18:57:54 +07:00 |
Alan Mishchenko
|
dac71e9b33
|
Added deriving abstraction in GIA from the precomputed flop map.
|
2011-07-29 16:21:25 +07:00 |
Alan Mishchenko
|
ce38474c74
|
Improving and updating the abstraction code.
|
2011-07-29 15:38:44 +07:00 |
Alan Mishchenko
|
9e6d0664cb
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-28 15:27:07 +07:00 |
Alan Mishchenko
|
fddff7a55b
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-28 13:50:34 +07:00 |
Alan Mishchenko
|
8ed6d8e05f
|
Adding procedures to find the care bits of a counter-example (update).
|
2011-07-27 20:18:14 +07:00 |
Alan Mishchenko
|
7184003b42
|
Adding procedures to find the care bits of a counter-example (update).
|
2011-07-25 20:52:15 +07:00 |
Alan Mishchenko
|
e7a5a74b4c
|
Adding procedures to find the care bits of a counter-example.
|
2011-07-25 20:35:06 +07:00 |
Alan Mishchenko
|
76447062cc
|
Adding &equiv3, a new way of refining equivalence classes.
|
2011-07-22 20:20:19 +07:00 |
Alan Mishchenko
|
9a2a0f2912
|
Changes to enable smarter simulation.
|
2011-07-21 17:55:44 +07:00 |
Alan Mishchenko
|
fdf79ed471
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-21 12:02:07 +07:00 |
Alan Mishchenko
|
ee261ef3f2
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-20 18:23:10 +07:00 |
Alan Mishchenko
|
bb86d9142e
|
New demitering features.
|
2011-07-20 13:52:54 +07:00 |
Alan Mishchenko
|
4ca6612821
|
Fixed assertion failure when mitering with choices.
|
2011-07-20 11:01:12 +07:00 |
Alan Mishchenko
|
bc63966e4a
|
Corner case bug fix in 'speedup'.
|
2011-07-20 10:55:58 +07:00 |
Alan Mishchenko
|
fbd6a08e73
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-16 17:49:35 +07:00 |
Alan Mishchenko
|
302f7d7a97
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-15 18:50:58 +07:00 |
Alan Mishchenko
|
96e44e313e
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-15 12:27:40 +07:00 |
Alan Mishchenko
|
6a020d6f69
|
Added switch to PDR to disable expensive generalization step.
|
2011-07-13 15:13:08 +07:00 |
Alan Mishchenko
|
669f390c6d
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-13 12:48:51 +07:00 |
Alan Mishchenko
|
73702835c6
|
Added equivalence class computation for flop outputs only in &equiv2.
|
2011-07-13 10:13:24 +07:00 |
Alan Mishchenko
|
204fac4dca
|
Other changes to enable new features in the mapper.
|
2011-07-10 13:56:05 +07:00 |
Alan Mishchenko
|
ebfd70cdf4
|
Initial changes to enable new features in the mapper
|
2011-07-08 19:40:07 -07:00 |
Alan Mishchenko
|
a37de7cc4d
|
Printing out the path/name of the resource file that is being sourced.
|
2011-07-02 17:17:55 -07:00 |
Alan Mishchenko
|
10953634c9
|
Fixing a typo, which led to not printing delay in 'ps' after SC mapping.
|
2011-07-02 17:05:14 -07:00 |
Alan Mishchenko
|
f866920eb5
|
Added a new demitering feature for dual-output miters.
|
2011-07-02 13:58:12 -07:00 |
Alan Mishchenko
|
6c2ac7661d
|
Added another specialized check to the mapper.
|
2011-06-27 20:17:52 -07:00 |
Alan Mishchenko
|
0985eaca6c
|
Updated 'iprove' to generate seq CEX when CEC fails (small fix).
|
2011-06-25 09:48:23 -07:00 |
Alan Mishchenko
|
49869d08ec
|
Merged two last changes.
|
2011-06-25 09:45:04 -07:00 |
Alan Mishchenko
|
15cc374fe3
|
Updated 'iprove' to generate seq CEX when CEC fails.
|
2011-06-25 09:23:44 -07:00 |
Alan Mishchenko
|
5b639818e9
|
Added dumping CEXes in AIGER format.
|
2011-06-21 19:54:31 -07:00 |
Alan Mishchenko
|
4669839b24
|
Added new mapping feature.
|
2011-06-20 22:23:32 -07:00 |
Alan Mishchenko
|
6fd29922d3
|
Added permute/unpermute.
|
2011-06-20 13:16:23 -07:00 |
Alan Mishchenko
|
3b77f2d16d
|
Added permute/unpermute.
|
2011-06-20 13:14:51 -07:00 |
Alan Mishchenko
|
51134ab81c
|
Disabled duplication of the network while removing POs in 'zeropo'.
|
2011-06-15 23:18:51 -07:00 |
Alan Mishchenko
|
68c79ee879
|
Added command &filter to filter equiv classes.
|
2011-06-15 00:31:11 -07:00 |
Alan Mishchenko
|
dcd95cac6f
|
Disabled duplication of the network while removing POs in 'removepo'.
|
2011-06-14 23:02:34 -07:00 |
Alan Mishchenko
|
b2dfa01370
|
Adding command 'srm2' (additional feature).
|
2011-06-08 11:34:51 -07:00 |
Alan Mishchenko
|
11f684c04d
|
Adding command 'srm2'.
|
2011-06-08 09:25:32 -07:00 |
Alan Mishchenko
|
bfbbfadfc4
|
Adding command 'srm2'.
|
2011-06-08 09:23:31 -07:00 |
Alan Mishchenko
|
ddb34e871c
|
Adding command 'removepo'.
|
2011-06-03 18:16:08 -07:00 |
Alan Mishchenko
|
3bdce84c5b
|
Bug fix in 'swappos'.
|
2011-06-03 17:54:12 -07:00 |
Alan Mishchenko
|
31360734b7
|
Added new command 'outdec'.
|
2011-05-19 11:43:11 +07:00 |
Alan Mishchenko
|
27311713c7
|
Special BLIF writing (bug fixes).
|
2011-05-18 15:03:19 +07:00 |
Alan Mishchenko
|
26fb1fcd14
|
Special BLIF writing.
|
2011-05-18 13:35:35 +07:00 |
Alan Mishchenko
|
3c7842be32
|
Improvements to timeout.
|
2011-05-11 22:14:12 +08:00 |
Alan Mishchenko
|
57daeee997
|
Updated technology mapping.
|
2011-05-08 00:22:32 -07:00 |
Alan Mishchenko
|
27bb2a684d
|
Updated technology mapping.
|
2011-05-07 20:19:45 -07:00 |