Alan Mishchenko
|
f59de3decc
|
Fixes to Verilog parser.
|
2012-09-20 11:29:37 -07:00 |
Alan Mishchenko
|
723f85ef1b
|
Extending Liberty parser to handle multi-output cells.
|
2012-09-19 20:21:27 -07:00 |
Alan Mishchenko
|
5dc50744f0
|
Extending Liberty parser to handle multi-output cells.
|
2012-09-19 18:42:00 -07:00 |
Alan Mishchenko
|
480ca14c75
|
Extending Liberty parser to handle multi-output cells.
|
2012-09-19 17:35:04 -07:00 |
Alan Mishchenko
|
3af0f719af
|
Extending BLIF parser/write to hangle multi-output cells.
|
2012-09-19 16:28:06 -07:00 |
Alan Mishchenko
|
60c6614885
|
Extending Genlib to hangle multi-output cells.
|
2012-09-19 11:53:40 -07:00 |
Alan Mishchenko
|
48996f7a36
|
Changes to command 'upsize'.
|
2012-09-18 19:12:54 -07:00 |
Alan Mishchenko
|
e0eb270324
|
Changes to command 'upsize'.
|
2012-09-18 13:23:58 -07:00 |
Alan Mishchenko
|
508b6f1b13
|
Fixing mismatch between declaration of the output value of Extra_CpuTime.
|
2012-09-18 09:58:06 -07:00 |
Alan Mishchenko
|
6dc3a0a246
|
Bug fix in bmc3.
|
2012-09-17 17:39:42 -07:00 |
Alan Mishchenko
|
1f9abfd7a8
|
Bug fix: no need to normalize const0 node.
|
2012-09-17 10:02:37 -07:00 |
Alan Mishchenko
|
819b41bb59
|
Fixed timeout problem in bmc3 -s.
|
2012-09-17 09:54:45 -07:00 |
Alan Mishchenko
|
790ea6545f
|
Moving binary IO streams to the vector package.
|
2012-09-17 01:01:47 -07:00 |
Alan Mishchenko
|
7e843d64a9
|
Added delay multipliers to 'map'.
|
2012-09-16 23:34:56 -07:00 |
Alan Mishchenko
|
6d05fde2dc
|
Added delay multipliers to 'map'.
|
2012-09-16 22:05:15 -07:00 |
Alan Mishchenko
|
bbf4b8bc1e
|
Improving printouts in 'stime'.
|
2012-09-16 21:40:20 -07:00 |
Alan Mishchenko
|
8b2b4fb6b8
|
Improving printouts in &gla.
|
2012-09-16 18:57:53 -07:00 |
Alan Mishchenko
|
c15137bd3f
|
Improving printouts in &gla.
|
2012-09-16 16:48:50 -07:00 |
Alan Mishchenko
|
ee436f9377
|
Changed a few things in the refinement package of &gla.
|
2012-09-16 13:56:10 -07:00 |
Alan Mishchenko
|
5953beb2da
|
Restructured the code to post-process object used during refinement in &gla.
|
2012-09-16 09:54:19 -07:00 |
Alan Mishchenko
|
5a4f1fe44c
|
Made abstraction and PDR communicate in-memory rather than through a file.
|
2012-09-16 00:26:18 -07:00 |
Alan Mishchenko
|
fdf5ad3433
|
Cleaned 'abc.c' by removing useless procedures.
|
2012-09-15 23:52:36 -07:00 |
Alan Mishchenko
|
69bbfa9856
|
Created new abstraction package from the code that was all over the place.
|
2012-09-15 23:27:46 -07:00 |
Alan Mishchenko
|
ec95f569dd
|
Corrected &gla -a to work as expected.
|
2012-09-15 21:18:32 -07:00 |
Alan Mishchenko
|
152aaedcb2
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 22:45:51 -07:00 |
Alan Mishchenko
|
080c325500
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:22:31 -07:00 |
Alan Mishchenko
|
117bc0dbcd
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:20:37 -07:00 |
Alan Mishchenko
|
f64bb36fd5
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:33:23 -07:00 |
Alan Mishchenko
|
3b14c7b490
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:31:29 -07:00 |
Alan Mishchenko
|
19c28cae94
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 10:27:48 -07:00 |
Alan Mishchenko
|
9b15f71f2f
|
Added new command 'upsize'.
|
2012-09-12 14:39:50 -07:00 |
Alan Mishchenko
|
e3d75484ce
|
Reversed to a buggy version of reduceDB in complete proof-logging, because it works with rollback and it is not used in &gla -pn -L 0.
|
2012-09-12 12:46:56 -07:00 |
Alan Mishchenko
|
606341dca6
|
Added code to collect experimental results.
|
2012-09-11 22:36:38 -07:00 |
Alan Mishchenko
|
e95844c0af
|
Added code to collect experimental results.
|
2012-09-11 22:35:27 -07:00 |
Alan Mishchenko
|
087ec9eb1f
|
Added code to collect experimental results.
|
2012-09-11 22:34:49 -07:00 |
Alan Mishchenko
|
825bcd823c
|
Added code to collect experimental results.
|
2012-09-11 22:33:47 -07:00 |
Alan Mishchenko
|
4c06c8afc0
|
Improved topo print-out.
|
2012-09-11 19:40:12 -07:00 |
Alan Mishchenko
|
a246882a5b
|
Scalable gate-level abstraction.
|
2012-09-11 19:11:51 -07:00 |
Niklas Een
|
1c865bf229
|
Added -C to command line for running commands, then staying in interactive mode
|
2012-09-11 18:48:43 -07:00 |
Alan Mishchenko
|
784a3579e5
|
Fixing Verilog writer's way of writing module names.
|
2012-09-11 18:44:07 -07:00 |
Alan Mishchenko
|
759b7c0855
|
Added code to collect experimental results.
|
2012-09-11 16:26:01 -07:00 |
Alan Mishchenko
|
d257fce824
|
Added code to collect experimental results.
|
2012-09-11 16:25:00 -07:00 |
Alan Mishchenko
|
20bd241e20
|
Commenting out some assertions in the 'map' mapper.
|
2012-09-10 00:23:41 -07:00 |
Alan Mishchenko
|
d40af538e2
|
Unified print-out of property failures produced by all engines.
|
2012-09-09 20:46:34 -07:00 |
Alan Mishchenko
|
71d7c9e66d
|
Disable printing refinement statistics by default.
|
2012-09-09 20:25:55 -07:00 |
Alan Mishchenko
|
56117d56e8
|
Added switch '-p' to '&gla -n' to use full proof for UNSAT core computation (for experiments).
|
2012-09-09 15:28:31 -07:00 |
Alan Mishchenko
|
4333fd24d2
|
Started CEX minimization procedure.
|
2012-09-08 18:28:13 -07:00 |
Alan Mishchenko
|
9efe9579f9
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 15:04:44 -07:00 |
Alan Mishchenko
|
519b9fdf7c
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 15:04:00 -07:00 |
Alan Mishchenko
|
002117c0e9
|
Started CEX minimization procedure.
|
2012-09-08 14:56:25 -07:00 |
Alan Mishchenko
|
cc6da1f905
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 00:19:46 -07:00 |
Alan Mishchenko
|
e1b76633dc
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 00:14:49 -07:00 |
Alan Mishchenko
|
5ca4f3cf9f
|
Updating &gla_refine to perform suffic refinement.
|
2012-09-07 23:26:23 -07:00 |
Alan Mishchenko
|
548e04192b
|
Updating &gla_refine to perform suffic refinement.
|
2012-09-07 20:44:12 -07:00 |
Alan Mishchenko
|
0b8e07bdde
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-07 13:36:39 -07:00 |
Alan Mishchenko
|
6c1d4ee8dd
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-07 13:33:52 -07:00 |
Alan Mishchenko
|
509194a898
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-07 13:02:46 -07:00 |
Alan Mishchenko
|
75a5c46b99
|
Added switch 'dch -r' to skip choices with structural support redundancy.
|
2012-09-07 00:18:54 -07:00 |
Alan Mishchenko
|
ce0e96bcaa
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 23:15:08 -07:00 |
Alan Mishchenko
|
5b3e31bd4d
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 23:11:34 -07:00 |
Alan Mishchenko
|
894fc81041
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:44:56 -07:00 |
Alan Mishchenko
|
4efd8bf7b3
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:33:43 -07:00 |
Alan Mishchenko
|
bf69a345c9
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:10:03 -07:00 |
Alan Mishchenko
|
794bd2fd33
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:01:48 -07:00 |
Alan Mishchenko
|
aff7f38495
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 20:58:14 -07:00 |
Alan Mishchenko
|
1cefca7dea
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 20:54:00 -07:00 |
Alan Mishchenko
|
58d50bf94a
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 20:51:16 -07:00 |
Alan Mishchenko
|
460f1905e2
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 16:30:00 -07:00 |
Alan Mishchenko
|
5a5577f907
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:55:54 -07:00 |
Alan Mishchenko
|
39fe23f079
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:52:54 -07:00 |
Alan Mishchenko
|
7a6cf9f48c
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:40:47 -07:00 |
Alan Mishchenko
|
9c8be56ccd
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:32:07 -07:00 |
Alan Mishchenko
|
4393a5fade
|
Added platform-independent random-number generator to 'fraig'.
|
2012-09-05 19:50:32 -07:00 |
Alan Mishchenko
|
cd2bd70865
|
Added switch 'dch -r' to skip choices with structural support redundancy.
|
2012-09-05 19:39:25 -07:00 |
Alan Mishchenko
|
c1f4545e07
|
Added error message when the user is trying 'dsat' for multi-output comb miters.
|
2012-09-05 18:53:21 -07:00 |
Alan Mishchenko
|
9cb16d654a
|
Added new command &gla_shrink.
|
2012-09-05 00:55:33 -07:00 |
Alan Mishchenko
|
f6b67d7846
|
Added new command &gla_shrink.
|
2012-09-04 23:57:58 -07:00 |
Alan Mishchenko
|
2071d9a732
|
Enabling additinal printouts.
|
2012-09-04 21:14:47 -07:00 |
Alan Mishchenko
|
8e12b60b66
|
Better batch mode printout.
|
2012-09-04 14:39:14 -07:00 |
Alan Mishchenko
|
acc3abe9cc
|
Correcting the report of completed timeframes in &gla.
|
2012-09-04 14:22:06 -07:00 |
Alan Mishchenko
|
4507a5d3ed
|
Correcting the report of completed timeframes in &gla.
|
2012-09-04 14:19:19 -07:00 |
Alan Mishchenko
|
b08aca5c1e
|
Make switches -d (-m) by default dump abstracted model (miter with abstraction map) into files whose names are derived from the names of the input file by adding _abs (_gla).
|
2012-09-04 14:09:39 -07:00 |
Alan Mishchenko
|
05f51cbb2a
|
Enabled recording the name of the file GIA is coming from.
|
2012-09-04 13:52:42 -07:00 |
Alan Mishchenko
|
b9ed304236
|
Correcting the report of completed timeframes in &gla.
|
2012-09-04 13:38:52 -07:00 |
Alan Mishchenko
|
6b2744ff77
|
Improving print-outs in 'stime' and 'gsize'.
|
2012-09-04 12:22:59 -07:00 |
Alan Mishchenko
|
b26d698ff8
|
Uniqifying status file name in &gla.
|
2012-09-03 19:06:01 -07:00 |
Alan Mishchenko
|
201cb24596
|
Several minor changes.
|
2012-09-03 17:15:44 -07:00 |
Alan Mishchenko
|
9621ae946e
|
Added switch &srm -A <file> for dumping SRM into a user-specified file.
|
2012-09-02 20:12:03 -07:00 |
Alan Mishchenko
|
ba597f6787
|
New package to read/write a subset of Liberty for STA.
|
2012-09-01 13:47:41 -07:00 |
Alan Mishchenko
|
fe1a16e9b4
|
Changes to allow &gla to run with fSimple = 1 (useful for debugging).
|
2012-08-31 18:45:10 -07:00 |
Alan Mishchenko
|
1e53a78a99
|
Bug fix in the old Liberty parser.
|
2012-08-31 15:14:30 -07:00 |
Alan Mishchenko
|
4bef56feb9
|
Added several assertions.
|
2012-08-31 15:08:05 -07:00 |
Alan Mishchenko
|
8c0e0d7143
|
Added command 'print_gs' to print gate sizes in the mapping.
|
2012-08-31 09:26:26 -07:00 |
Alan Mishchenko
|
e63c603e92
|
Fixing assert which failes when SAT solver returns after a timeout.
|
2012-08-31 00:52:08 -07:00 |
Alan Mishchenko
|
a49ba2d280
|
Fixing the way constants are written into mapped Verilog files.
|
2012-08-31 00:05:10 -07:00 |
Alan Mishchenko
|
5a009b6774
|
Improvements to gate-sizing.
|
2012-08-30 21:46:31 -07:00 |
Alan Mishchenko
|
484ab7a17b
|
Improvements to gate-sizing.
|
2012-08-30 19:54:17 -07:00 |
Alan Mishchenko
|
b8b478c8d8
|
Improvements to gate-sizing.
|
2012-08-30 16:46:54 -07:00 |
Alan Mishchenko
|
caa66f0ca9
|
Improving print-out in gate-sizing.
|
2012-08-30 14:32:36 -07:00 |
Alan Mishchenko
|
a38861babf
|
Improving print-out in gate-sizing.
|
2012-08-30 14:27:25 -07:00 |
Alan Mishchenko
|
3400670839
|
Handling constant nodes in gate sizing.
|
2012-08-30 13:58:26 -07:00 |
Alan Mishchenko
|
b9a1c6ec87
|
Commenting out debug dump of the library.
|
2012-08-30 13:44:28 -07:00 |
Alan Mishchenko
|
69c36f426c
|
Improvements to gate-sizing.
|
2012-08-30 12:34:53 -07:00 |
Alan Mishchenko
|
6dd270d41f
|
Improvements to gate-sizing.
|
2012-08-30 11:10:02 -07:00 |
Alan Mishchenko
|
c84f26c9b1
|
Compiler warnings.
|
2012-08-29 17:31:14 -07:00 |
Alan Mishchenko
|
b2b93858ee
|
Compiler warnings.
|
2012-08-29 17:14:02 -07:00 |
Alan Mishchenko
|
4c5bfbe73f
|
Forgot to update makefile.
|
2012-08-29 17:02:31 -07:00 |
Alan Mishchenko
|
83bfe0b1fe
|
New package to read/write a subset of Liberty for STA.
|
2012-08-29 16:20:39 -07:00 |
Alan Mishchenko
|
6814c48bb4
|
Added an API to convert a multi-output PLA into a shared AIG.
|
2012-08-29 12:43:55 -07:00 |
Alan Mishchenko
|
bebd7ee6cb
|
New package to read/write a subset of Liberty for STA.
|
2012-08-29 00:48:36 -07:00 |
Alan Mishchenko
|
5ff49be993
|
Ensured that SC mapped network is always in a topo order.
|
2012-08-28 19:42:53 -07:00 |
Alan Mishchenko
|
9b02fe59bd
|
Added buffering based on combinational merging.
|
2012-08-28 19:24:13 -07:00 |
Alan Mishchenko
|
329831bdac
|
Bug fix: abstraction commands not properly updating status when dumping intermediate abstraction.
|
2012-08-28 12:12:24 -07:00 |
Alan Mishchenko
|
8a1d439cb1
|
Added precomputation of TFO ordering for incremental network updates.
|
2012-08-27 22:11:29 -07:00 |
Alan Mishchenko
|
7772a4af05
|
Added printout of library cells.
|
2012-08-27 19:58:15 -07:00 |
Alan Mishchenko
|
a6bfd49591
|
Improved printout of command history.
|
2012-08-27 19:57:44 -07:00 |
Alan Mishchenko
|
da6838463f
|
Added features 'map -M <float>' to control the use of large gates.
|
2012-08-27 14:29:32 -07:00 |
Alan Mishchenko
|
9abe8b66c9
|
New package to read/write a subset of Liberty for STA.
|
2012-08-27 13:50:33 -07:00 |
Alan Mishchenko
|
c25f5dee05
|
Bug fix in &gla.
|
2012-08-27 13:49:53 -07:00 |
Alan Mishchenko
|
1ba1e6574c
|
New package to read/write a subset of Liberty for STA.
|
2012-08-26 17:32:22 -07:00 |
Alan Mishchenko
|
95e14cd72c
|
Select for mapping smallest-area gates for each functionality.
|
2012-08-26 17:31:23 -07:00 |
Alan Mishchenko
|
889ed19c1c
|
Compiler warnings.
|
2012-08-26 09:31:43 -07:00 |
Alan Mishchenko
|
137f0347f0
|
Added switch '&gla -m' to dump original miter with the abstraction map.
|
2012-08-26 09:21:45 -07:00 |
Alan Mishchenko
|
dfd6ab0823
|
New package to read/write a subset of Liberty for STA.
|
2012-08-25 19:00:26 -07:00 |
Alan Mishchenko
|
fba0552f87
|
Added recording history of used commands into file 'abc.history' (Windows only).
|
2012-08-25 14:57:06 -07:00 |
Alan Mishchenko
|
bffbd05a2f
|
Added recording history of used commands into file 'abc.history' (Windows only).
|
2012-08-25 13:43:44 -07:00 |
Alan Mishchenko
|
19d50b98a1
|
New package to read/write a subset of Liberty for STA.
|
2012-08-25 12:34:54 -07:00 |
Alan Mishchenko
|
2a7a06b653
|
Added recording history of used commands into file 'abc.history' (Windows only).
|
2012-08-25 12:32:44 -07:00 |
Alan Mishchenko
|
49c5799934
|
Several improvements to command 'testnpn'.
|
2012-08-25 10:30:53 -07:00 |
Alan Mishchenko
|
f85db9dd1f
|
Compiler warnings.
|
2012-08-24 21:36:09 -07:00 |
Alan Mishchenko
|
13bd7b334c
|
New package to read/write a subset of Liberty for STA.
|
2012-08-24 21:31:46 -07:00 |
Alan Mishchenko
|
22d21a5c44
|
Added recording history of used commands into file 'abc.history' (Windows only).
|
2012-08-24 15:44:33 -07:00 |
Alan Mishchenko
|
7e2b007762
|
Added recording history of used commands into file 'abc.history' (Windows only).
|
2012-08-24 12:25:53 -07:00 |
Alan Mishchenko
|
4a9152d0e1
|
Changed command 'sim' to work with a miter by default (replace 'sim -m' by 'sim' in verification applications).
|
2012-08-24 11:14:40 -07:00 |
Alan Mishchenko
|
942600414d
|
Added simulation of comb circuits with user-specified patterns in command 'sim'.
|
2012-08-24 11:12:51 -07:00 |
Alan Mishchenko
|
12c776ed6e
|
Added new algorithm for NPN semi-canonical form computation.
|
2012-08-23 22:20:27 -07:00 |
Alan Mishchenko
|
5da7102f55
|
Fixing undesirable effect of recent refinement code on older code in &gla -n.
|
2012-08-11 11:47:22 -07:00 |
Alan Mishchenko
|
528c8e0bba
|
Enabling -S <num> for &gla to not check the first <num> frames.
|
2012-08-10 23:56:46 -07:00 |
Alan Mishchenko
|
d22b3d055b
|
Fixing problem with max limit on the number of abstracted objects in &gla.
|
2012-08-10 11:16:23 -07:00 |
Alan Mishchenko
|
65b652fadb
|
Added purification of UNSAT core in &gla.
|
2012-08-10 09:31:03 -07:00 |
Alan Mishchenko
|
409ce39b61
|
Improved abstraction refinement.
|
2012-08-09 19:44:40 -07:00 |
Alan Mishchenko
|
a019dd216e
|
Improved abstraction refinement.
|
2012-08-09 19:16:25 -07:00 |
Alan Mishchenko
|
cfc82efbb9
|
Compiler warnings.
|
2012-08-09 18:56:48 -07:00 |
Alan Mishchenko
|
518410af35
|
Compiler warnings.
|
2012-08-09 18:55:30 -07:00 |
Alan Mishchenko
|
20518f59d1
|
Compiler warnings.
|
2012-08-09 18:45:53 -07:00 |
Alan Mishchenko
|
1451614c5c
|
Compiler warnings.
|
2012-08-09 18:10:14 -07:00 |
Alan Mishchenko
|
8ad4a10fae
|
Compiler warnings.
|
2012-08-09 18:07:00 -07:00 |
Alan Mishchenko
|
5b80d704a1
|
Improved abstraction refinement.
|
2012-08-09 17:53:38 -07:00 |
Alan Mishchenko
|
d01c0807bd
|
New semi-canonical form computation package.
|
2012-08-08 20:37:58 -07:00 |
Alan Mishchenko
|
bf35ed1b86
|
New cut-based refinement.
|
2012-08-08 12:33:48 -07:00 |