Alan Mishchenko
|
e70adbcd2d
|
Improvements to the standard cell flow.
|
2013-11-08 15:16:13 -08:00 |
Aaron Tomb
|
56378651c7
|
Fix parenthesization of Abc_Clock #ifdef.
The previous location of parentheses led to an attempt to compile
against Linux-only clock APIs when building on 32-bit OS X.
|
2013-11-06 16:35:02 -08:00 |
Alan Mishchenko
|
e3560904ec
|
Merged in atomb/abc (pull request #1)
Several patches to fix compilation under MINGW32
|
2013-11-05 13:41:39 -08:00 |
Alan Mishchenko
|
a1d2ba0fcc
|
Tuning for multi-ouptut solver.
|
2013-11-04 22:30:27 -08:00 |
Aaron Tomb
|
aa2eae5cab
|
Don't assume MSVC when __MINGW32__ set.
|
2013-11-04 14:28:32 -08:00 |
Aaron Tomb
|
6a4d430e60
|
Choose Windows file operations with MINGW32.
|
2013-11-04 14:27:09 -08:00 |
Aaron Tomb
|
cf1746e348
|
Make definition of Abc_Clock work with MINGW32.
|
2013-11-04 14:25:55 -08:00 |
Alan Mishchenko
|
9439786d95
|
Changes to Liberty parser.
|
2013-10-30 18:07:41 -04:00 |
Alan Mishchenko
|
80f46fa2ae
|
Compiler warnings.
|
2013-10-30 10:29:44 -04:00 |
Alan Mishchenko
|
7d2b77afc8
|
Multi-output property solver.
|
2013-10-23 16:26:20 -07:00 |
Alan Mishchenko
|
2c7f39026a
|
Extending truth table support in &jf for more than 6 inputs.
|
2013-10-10 14:45:19 -07:00 |
Alan Mishchenko
|
33695bed11
|
Improvements to the canonical form computation.
|
2013-10-10 12:35:27 -07:00 |
Alan Mishchenko
|
7a1c4ee867
|
Moved the code to a different file.
|
2013-10-06 16:16:21 -07:00 |
Alan Mishchenko
|
8a03e530c2
|
Resubstitution code.
|
2013-10-06 15:57:17 -07:00 |
Alan Mishchenko
|
e1986d0433
|
Towards better Boolean matching.
|
2013-10-05 22:52:15 -07:00 |
Alan Mishchenko
|
a4a1053d98
|
Towards better Boolean matching.
|
2013-10-05 22:44:02 -07:00 |
Niklas Een
|
c9635d029e
|
Added 'abort' message in bridge mode for pdr -a timeout
|
2013-10-04 15:20:42 -07:00 |
Alan Mishchenko
|
7b99370e0a
|
Changing default values.
|
2013-10-02 14:36:33 -07:00 |
Alan Mishchenko
|
e34251060e
|
Changing default values.
|
2013-09-30 11:43:17 -07:00 |
Alan Mishchenko
|
1f16b97c89
|
Changing default values.
|
2013-09-29 11:57:25 -07:00 |
Alan Mishchenko
|
f6653175b4
|
Code to test AIG generation for DSD structures.
|
2013-09-27 10:08:54 -07:00 |
Niklas Een
|
4cc3203110
|
Fixed a bug in Bridge mode
|
2013-09-27 00:17:59 -07:00 |
Alan Mishchenko
|
f704aa43fb
|
New logic sharing extraction.
|
2013-09-26 19:04:18 -07:00 |
Alan Mishchenko
|
f787e75b83
|
Improving DAG-aware unmapping.
|
2013-09-25 16:41:19 -07:00 |
Alan Mishchenko
|
531657105b
|
Improving DAG-aware unmapping.
|
2013-09-25 15:29:01 -07:00 |
Alan Mishchenko
|
ee11ee1833
|
Changes to enable decomposition of non-DSD functions.
|
2013-09-25 13:18:21 -07:00 |
Alan Mishchenko
|
e446cfca15
|
Added bridge integration for multi-output 'pdr -a'.
|
2013-09-16 14:54:11 -07:00 |
Alan Mishchenko
|
653dc8cff5
|
Added bridge integration for multi-output 'pdr -a'.
|
2013-09-16 14:46:07 -07:00 |
Alan Mishchenko
|
3b1cf0976c
|
Added bridge integration for multi-output 'pdr -a'.
|
2013-09-16 14:39:37 -07:00 |
Alan Mishchenko
|
ff5d3591d1
|
Infrastructure to support full Liberty format and unitification of library representations.
|
2013-09-15 18:23:49 -07:00 |
Alan Mishchenko
|
5b6b7c5bbe
|
Removing duplicated typedef line.
|
2013-09-13 09:39:50 -07:00 |
Alan Mishchenko
|
75fee10708
|
Improvements to the new technology mapper.
|
2013-09-12 22:37:26 -07:00 |
Alan Mishchenko
|
14606c473e
|
Improvements to the new technology mapper.
|
2013-09-12 17:53:41 -07:00 |
Alan Mishchenko
|
61abba9571
|
Improvements to the new technology mapper.
|
2013-09-11 23:49:05 -07:00 |
Alan Mishchenko
|
211ac730c6
|
Improvements to the new technology mapper.
|
2013-09-11 18:19:36 -07:00 |
Alan Mishchenko
|
0e256dc2c2
|
Updates for the new BMC engine.
|
2013-09-10 22:12:42 -07:00 |
Alan Mishchenko
|
2fa9645b08
|
Improvements to the new technology mapper.
|
2013-09-09 14:00:47 -07:00 |
Alan Mishchenko
|
48db1c3a04
|
Improvements to the new technology mapper.
|
2013-09-09 00:15:01 -07:00 |
Alan Mishchenko
|
23879f9200
|
Unifying parameters for the &ps command.
|
2013-09-05 20:40:50 -07:00 |
Alan Mishchenko
|
a495163f74
|
Buf fixes and minor changes to the &if mapper.
|
2013-08-29 14:41:01 -07:00 |
Alan Mishchenko
|
eec022ea64
|
Adding procedures to specify permutations with unused flops.
|
2013-08-28 20:21:01 -07:00 |
Alan Mishchenko
|
7013e0b672
|
Small changes to compile on Mac.
|
2013-08-15 00:58:23 -07:00 |
Alan Mishchenko
|
fcfafb0601
|
Enabling additional matching feature in the LUT mapper.
|
2013-08-12 23:27:20 -07:00 |
Alan Mishchenko
|
881b2ec46f
|
Integrated buffering and sizing.
|
2013-08-08 18:23:00 -07:00 |
Alan Mishchenko
|
c0ac159888
|
New technology mapper.
|
2013-07-14 15:04:25 -07:00 |
Alan Mishchenko
|
b3e0f5b2e9
|
New technology mapper.
|
2013-07-13 23:40:51 -07:00 |
Alan Mishchenko
|
2ee26b00f9
|
Precomputing DSD functions.
|
2013-07-11 22:08:35 -07:00 |
Alan Mishchenko
|
76875cd18d
|
Compiler warning.
|
2013-07-01 23:08:54 -07:00 |
Alan Mishchenko
|
64e2ee223b
|
Adding #include <stdlib.h> to 'abc_global.h' to prevent compilation problem on some platforms.
|
2013-07-01 14:07:42 -07:00 |
Alan Mishchenko
|
4e247281d2
|
Updating new mapper.
|
2013-06-29 23:45:04 -07:00 |
Niklas Een
|
45ce151195
|
Forgot that LIN64 was used in place of LIN for 64-bit architectures. Fixed.
|
2013-06-29 02:23:23 -07:00 |
Niklas Een
|
43df8967b5
|
Fixed a problem in BridgeMode; it will now correctly detect if the pipe has been closed and exit ABC.
|
2013-06-28 21:11:26 -07:00 |
Alan Mishchenko
|
fe40fd5c80
|
Updating new mapper.
|
2013-06-28 16:46:18 -07:00 |
Alan Mishchenko
|
13dd754a8c
|
Suggested changes to counting time in Abc_Clock()
|
2013-06-18 11:26:37 -07:00 |
Alan Mishchenko
|
3c97892514
|
New MFS package.
|
2013-05-30 14:09:50 -07:00 |
Alan Mishchenko
|
67127b838d
|
New DSD detection code.
|
2013-05-30 09:46:13 -07:00 |
Alan Mishchenko
|
22bdf62465
|
Adding a wrapper around clock() for more accurate time counting in ABC.
|
2013-05-27 15:14:42 -07:00 |
Alan Mishchenko
|
19c25fd6aa
|
Adding a wrapper around clock() for more accurate time counting in ABC.
|
2013-05-27 15:09:23 -07:00 |
Alan Mishchenko
|
0cad45fa90
|
New MFS package.
|
2013-05-27 09:49:13 -07:00 |
Alan Mishchenko
|
ac037cbb96
|
New MFS package.
|
2013-05-23 23:22:12 -07:00 |
Alan Mishchenko
|
3880623c9b
|
Extending cube representation to handle SOPs with many cubes.
|
2013-05-12 23:23:18 -07:00 |
Alan Mishchenko
|
9d219eee4b
|
New MFS package.
|
2013-05-12 19:09:28 -07:00 |
Alan Mishchenko
|
eacfad7622
|
Changing the queue to work in the same the array of costs is realloced.
|
2013-05-05 09:04:14 -07:00 |
Alan Mishchenko
|
a762c695d7
|
New fast extract.
|
2013-05-05 01:54:11 -07:00 |
Alan Mishchenko
|
744d35d029
|
C++ compiler errors.
|
2013-05-04 20:32:38 -07:00 |
Alan Mishchenko
|
3945d382fe
|
Adding new API to the queue.
|
2013-05-04 20:24:35 -07:00 |
Alan Mishchenko
|
95571be503
|
Changes to the ABC data-structures to allow for larger designs.
|
2013-05-04 10:48:46 -07:00 |
Alan Mishchenko
|
fcd377405a
|
Compiler warnings.
|
2013-05-03 15:48:05 -07:00 |
Alan Mishchenko
|
6a49d1f4c6
|
Reading/writing MiniAIG and several minor changes.
|
2013-05-03 15:45:50 -07:00 |
Alan Mishchenko
|
bc50421928
|
Minor changes and improvement in PO partitioning (command &popart).
|
2013-05-01 12:45:34 -07:00 |
Alan Mishchenko
|
b94766bce5
|
Faster isomorphism detection (command &iso).
|
2013-05-01 00:10:53 -07:00 |
Alan Mishchenko
|
b09926e8e2
|
SAT sweeping under constraints.
|
2013-04-28 01:25:29 -07:00 |
Alan Mishchenko
|
324d73c29a
|
New fast extract.
|
2013-04-27 15:23:12 -07:00 |
Alan Mishchenko
|
2650f94598
|
Shrink for 6-LUTs.
|
2013-03-31 23:09:51 -07:00 |
Alan Mishchenko
|
e64cad10e2
|
Adding command &miter2 to derive a specified sequential miter.
|
2013-03-27 12:43:00 -07:00 |
Alan Mishchenko
|
eee8ceb0fa
|
PO partitioning algorithm.
|
2013-03-09 12:19:11 -08:00 |
Alan Mishchenko
|
ae091e695e
|
Integrating box library.
|
2013-03-08 18:58:54 -08:00 |
Alan Mishchenko
|
dcc8907161
|
Improvements to the hierarchy/timing manager.
|
2013-03-05 16:53:18 -08:00 |
Alan Mishchenko
|
4ff5203f4c
|
Improvements to the hierarchy/timing manager.
|
2013-03-05 13:13:15 -08:00 |
Alan Mishchenko
|
a27a7bc827
|
User-controlable SAT sweeper and other small changes.
|
2013-02-27 12:12:23 -05:00 |
Alan Mishchenko
|
c98119594e
|
User-controlable SAT sweeper.
|
2013-02-26 16:59:21 -05:00 |
Alan Mishchenko
|
7e293ebe08
|
User-controlable SAT sweeper.
|
2013-02-25 22:07:32 -05:00 |
Alan Mishchenko
|
fe3b2e250b
|
User-controlable SAT sweeper.
|
2013-02-25 17:49:59 -05:00 |
Alan Mishchenko
|
fdba646b64
|
Integrating sweeping information.
|
2013-02-23 17:13:42 -08:00 |
Alan Mishchenko
|
7802db98af
|
Integrating sweeping information.
|
2013-02-23 16:08:10 -08:00 |
Alan Mishchenko
|
2e14b73af6
|
Allowing for Verilog names of the type slash-<name>-space-[N].
|
2013-02-22 13:49:07 -08:00 |
Alan Mishchenko
|
24823dce0c
|
Integrating sweeping information.
|
2013-02-20 23:34:27 -08:00 |
Alan Mishchenko
|
b096809458
|
Integrating sweeping information.
|
2013-02-20 23:22:01 -08:00 |
Alan Mishchenko
|
aa7daf1e51
|
Integrating sweeping information.
|
2013-02-20 17:13:29 -08:00 |
Alan Mishchenko
|
466c4e9992
|
Integrating hierarchy information (reporting incorrect topological order).
|
2013-02-20 14:23:00 -08:00 |
Alan Mishchenko
|
59fe3268a7
|
Adding STG generation (&era -d) and STG encoding (&read_stg <file>).
|
2013-02-19 23:07:29 -08:00 |
Alan Mishchenko
|
99a9718355
|
Integrating sweeping information.
|
2013-02-19 12:56:36 -08:00 |
Alan Mishchenko
|
cda61cb2fa
|
Integrating sweeping information.
|
2013-02-18 23:18:42 -08:00 |
Alan Mishchenko
|
930369f36f
|
Integration of timing manager.
|
2013-02-03 18:02:22 +08:00 |
Alan Mishchenko
|
6a0dca4535
|
Integration of timing manager.
|
2013-02-01 23:55:12 +08:00 |
Alan Mishchenko
|
686f8fdaa6
|
Integration of timing manager.
|
2013-01-30 19:04:45 +07:00 |
Alan Mishchenko
|
7e598cd231
|
Fixing compilation problems on Linux-32 related to constants of type unsigned long long.
|
2013-01-30 16:15:53 +07:00 |
Alan Mishchenko
|
4aa434ad11
|
Updated CEX code to handle trivial CEX of the type (Abc_Cex_t*)1.
|
2013-01-25 14:16:31 +07:00 |
Alan Mishchenko
|
4bd54729d7
|
Integration of timing manager.
|
2013-01-25 05:57:52 +07:00 |
Alan Mishchenko
|
6863688789
|
Enabled detecting CEXes in multiple POs without stopping (sim3 -a).
|
2013-01-23 12:37:44 +07:00 |
Alan Mishchenko
|
70655d5d31
|
Integration of timing manager.
|
2013-01-23 01:34:34 +07:00 |
Alan Mishchenko
|
a625caa17d
|
Fixing C++ compilation issues.
|
2013-01-08 13:56:20 +08:00 |
Alan Mishchenko
|
64e907d153
|
Technology mapper.
|
2013-01-08 05:51:36 +08:00 |
Alan Mishchenko
|
bfad654205
|
Assembling timing/hierarchy manager from input data.
|
2012-12-15 17:39:34 -08:00 |
Alan Mishchenko
|
82050bbe11
|
Assembling timing/hierarchy manager from input data.
|
2012-12-13 15:18:53 -08:00 |
Alan Mishchenko
|
ad67f4ef25
|
Assembling timing/hierarchy manager from input data.
|
2012-12-10 16:04:01 -08:00 |
Alan Mishchenko
|
2575a5d683
|
Unifification of custom extensions.
|
2012-12-10 13:56:40 -08:00 |
Alan Mishchenko
|
58d4012a55
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 14:46:16 -08:00 |
Alan Mishchenko
|
0058cefee3
|
Deriving CEX after phase/tempor/reparam.
|
2012-12-09 00:19:18 -08:00 |
Alan Mishchenko
|
8e5d771feb
|
Deriving CEX after phase/tempor/reparam.
|
2012-12-08 12:38:31 -08:00 |
Alan Mishchenko
|
f1a5288904
|
Counter-example analysis and optimization.
|
2012-11-30 11:38:05 -08:00 |
Alan Mishchenko
|
c48e3c7ab4
|
Counter-example analysis and optimization.
|
2012-11-29 13:34:07 -08:00 |
Alan Mishchenko
|
661265984c
|
Counter-example analysis and optimization.
|
2012-11-28 16:18:39 -08:00 |
Alan Mishchenko
|
b2fd119933
|
DSD manager.
|
2012-11-20 21:34:40 -08:00 |
Alan Mishchenko
|
ffbe3bc576
|
DSD manager.
|
2012-11-19 23:42:05 -08:00 |
Alan Mishchenko
|
a0052e22b4
|
Added switch 'cexcut -m' to generate bad states for all frames after G.
|
2012-11-15 16:00:29 -08:00 |
Alan Mishchenko
|
be29f37baa
|
Added command 'cexcut' and 'cexmerge'.
|
2012-11-14 18:20:35 -08:00 |
Alan Mishchenko
|
9d5d804610
|
Added command 'cexcut' and 'cexmerge'.
|
2012-11-14 16:09:49 -08:00 |
Alan Mishchenko
|
30b8c3d422
|
Made print-out of frontier cut an option ('-c') in '&ps'.
|
2012-11-12 14:08:10 -08:00 |
Alan Mishchenko
|
21e6a59ed8
|
Improved DSD.
|
2012-11-11 13:26:36 -08:00 |
Alan Mishchenko
|
2fbb4b1826
|
Improved DSD.
|
2012-11-06 20:27:31 -08:00 |
Alan Mishchenko
|
3f7f497351
|
Improved DSD.
|
2012-11-06 16:32:58 -08:00 |
Alan Mishchenko
|
7ba37f4901
|
Improved DSD.
|
2012-11-03 00:38:17 -07:00 |
Alan Mishchenko
|
b9c22ba99a
|
Improved DSD.
|
2012-11-02 14:24:22 -07:00 |
Alan Mishchenko
|
35c8d6a2fd
|
Improvements to the truth table computations.
|
2012-11-01 14:58:31 -07:00 |
Alan Mishchenko
|
d56570f235
|
Improvements to the truth table computations.
|
2012-11-01 14:23:05 -07:00 |
Alan Mishchenko
|
ce3f8cb1d1
|
Improvements to the truth table computations.
|
2012-11-01 02:53:09 -07:00 |
Alan Mishchenko
|
ee939fa0dd
|
Improvements to the truth table computations.
|
2012-10-31 01:33:13 -07:00 |
Alan Mishchenko
|
d8e84ce666
|
Improvements to the truth table computations.
|
2012-10-31 01:22:16 -07:00 |
Alan Mishchenko
|
6f3425150b
|
Improvements to the truth table computations.
|
2012-10-31 00:11:30 -07:00 |
Alan Mishchenko
|
66c044c688
|
Improvements to the truth table computations.
|
2012-10-30 23:42:04 -07:00 |
Alan Mishchenko
|
32b09a1e7b
|
Improvements to the truth table computations.
|
2012-10-30 22:33:30 -07:00 |
Alan Mishchenko
|
0fafe786ae
|
Improvements to the truth table computations.
|
2012-10-30 22:25:45 -07:00 |
Niklas Een
|
77fde55b1b
|
Added switch for netlist type to 'send_aig'. Changed defautl to &-space. Fixed printf -> Abc_Print in some places.
|
2012-10-30 19:09:40 -07:00 |
Alan Mishchenko
|
c3298ec225
|
Improvements to the truth table computation in 'if' package.
|
2012-10-29 23:27:41 -07:00 |
Alan Mishchenko
|
68d360c2d0
|
Move truth table code into a separte file.
|
2012-10-28 19:42:20 -07:00 |
Alan Mishchenko
|
ab2dfec272
|
Improvements to LMS code.
|
2012-10-27 17:38:45 -07:00 |
Alan Mishchenko
|
94d722c58e
|
Improvements to LMS code.
|
2012-10-27 17:33:13 -07:00 |
Alan Mishchenko
|
84b54597b4
|
Adding #ifdef to guard windows-specific debugging option.
|
2012-10-20 22:58:42 -07:00 |
Alan Mishchenko
|
dd25b90f8e
|
Improvements to gate sizing.
|
2012-10-09 01:20:51 -07:00 |
Alan Mishchenko
|
9206e6ff80
|
Improvements to gate sizing.
|
2012-10-08 21:20:13 -07:00 |
Alan Mishchenko
|
f11f645f1d
|
Bug fix in loading the timing manager.
|
2012-10-05 16:56:10 -07:00 |
Alan Mishchenko
|
8b4e762e5a
|
Minor bug fix.
|
2012-10-04 12:05:57 -07:00 |
Alan Mishchenko
|
56d3d7cd22
|
C++ portability changes.
|
2012-10-03 21:49:18 -07:00 |
Alan Mishchenko
|
63c9540543
|
Minor bug fixes.
|
2012-10-03 20:38:03 -07:00 |
Alan Mishchenko
|
71bdfae941
|
Replacing 'st_table' by 'st__table' to resolve linker problems.
|
2012-09-29 17:11:03 -04:00 |
Alan Mishchenko
|
6f03813557
|
Testing GIA with time manager.
|
2012-09-24 01:13:51 -07:00 |
Alan Mishchenko
|
40d9b5853b
|
Testing GIA with time manager.
|
2012-09-23 18:34:10 -07:00 |
Alan Mishchenko
|
f7caf84f21
|
Modified structural constraint extraction (unfold -s) to work for multi-output testcases.
|
2012-09-23 14:30:17 -07:00 |
Alan Mishchenko
|
a50a38155c
|
Integrating time manager into choice computation.
|
2012-09-22 17:57:06 -07:00 |
Alan Mishchenko
|
fdd043ca34
|
Upgrading hierarchy timing manager.
|
2012-09-21 22:00:39 -07:00 |
Alan Mishchenko
|
bc44087bac
|
Modified 'read' to read all types of libraries (genlib, liberty, scl).
|
2012-09-20 12:41:59 -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
|
790ea6545f
|
Moving binary IO streams to the vector package.
|
2012-09-17 01:01:47 -07:00 |
Alan Mishchenko
|
201cb24596
|
Several minor changes.
|
2012-09-03 17:15:44 -07:00 |
Alan Mishchenko
|
7772a4af05
|
Added printout of library cells.
|
2012-08-27 19:58:15 -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
|
13bd7b334c
|
New package to read/write a subset of Liberty for STA.
|
2012-08-24 21:31:46 -07:00 |
Alan Mishchenko
|
12c776ed6e
|
Added new algorithm for NPN semi-canonical form computation.
|
2012-08-23 22:20:27 -07:00 |
Alan Mishchenko
|
65b652fadb
|
Added purification of UNSAT core in &gla.
|
2012-08-10 09:31:03 -07:00 |
Alan Mishchenko
|
5b80d704a1
|
Improved abstraction refinement.
|
2012-08-09 17:53:38 -07:00 |
Alan Mishchenko
|
41fa9a1016
|
New command 'testnpn' to compare semi-canonical forms.
|
2012-08-08 01:42:14 -07:00 |
Alan Mishchenko
|
cd39fd6b05
|
Fixing performance bug with old proof-logging (adding clauses multiple times).
|
2012-07-30 11:05:54 -07:00 |
Alan Mishchenko
|
8982bf58cb
|
Reducing memory usage in proof-based abstraction.
|
2012-07-29 22:31:00 -07:00 |
Alan Mishchenko
|
8a2d237f78
|
Adding memory reporting to vectors.
|
2012-07-29 12:34:32 -07:00 |
Alan Mishchenko
|
a40c13a93c
|
Recording and reusing learned util clauses in bmc2.
|
2012-07-22 22:28:24 -07:00 |
Alan Mishchenko
|
6df122bda6
|
Updated code for lazy man's synthesis (memory optimization).
|
2012-07-20 18:56:26 -07:00 |
Alan Mishchenko
|
6c9b59bfc0
|
Updated code for lazy man's synthesis.
|
2012-07-20 15:54:08 -07:00 |
Alan Mishchenko
|
e53ffc6408
|
New procedures to generate NPN-classes for a library of 6-input functions.
|
2012-07-20 08:48:14 -07:00 |
Alan Mishchenko
|
2279a538b7
|
New procedures to generate NPN-classes for a library of 6-input functions.
|
2012-07-19 20:38:03 -07:00 |
Alan Mishchenko
|
fd33975aa5
|
Fixing the integer print-out problem.
|
2012-07-13 20:16:52 -07:00 |
Alan Mishchenko
|
5d01ed7fc6
|
Fixing the integer print-out problem.
|
2012-07-13 19:30:04 -07:00 |
Alan Mishchenko
|
bbf4b9a58d
|
Debugging a proof error.
|
2012-07-13 18:47:04 -07:00 |
Alan Mishchenko
|
4ebda996d7
|
Debugging a proof error.
|
2012-07-13 18:22:10 -07:00 |
Alan Mishchenko
|
c50d108f98
|
Debugging a proof error.
|
2012-07-13 18:15:32 -07:00 |
Alan Mishchenko
|
c25f488a83
|
Debugging a proof error.
|
2012-07-13 17:53:08 -07:00 |
Alan Mishchenko
|
3fb103dadc
|
Debugging a proof error.
|
2012-07-13 16:31:12 -07:00 |
Alan Mishchenko
|
da525b2a23
|
Debugging a proof error.
|
2012-07-13 16:25:07 -07:00 |
Alan Mishchenko
|
b7b60ebdcb
|
Fixing a mismatch in regular/shadow page memory appending procedure.
|
2012-07-13 16:10:20 -07:00 |
Alan Mishchenko
|
b9ee5d8564
|
Improvements in the proof-logging SAT solver.
|
2012-07-11 12:45:46 -07:00 |
Alan Mishchenko
|
908d5e696c
|
Replacing Mb/Gb to be MB/GB.
|
2012-07-09 22:57:03 -07:00 |
Alan Mishchenko
|
c265d2449a
|
Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).
|
2012-07-09 15:57:18 -07:00 |
Alan Mishchenko
|
1c33107cbb
|
Updating project settings to have simpler include paths.
|
2012-07-07 20:14:12 -07:00 |
Alan Mishchenko
|
3aab724573
|
Fixing time primtouts throughout the code.
|
2012-07-07 17:46:54 -07:00 |
Alan Mishchenko
|
8b881d235a
|
Making 'pdr', &gla, &vta print correctly in batch mode.
|
2012-07-07 10:44:34 -07:00 |
Alan Mishchenko
|
00eafb2325
|
Fixing time printouts in 'pdr'.
|
2012-07-07 09:27:28 -07:00 |
Alan Mishchenko
|
70331b585b
|
Fixing time printouts in 'pdr'.
|
2012-07-07 08:43:03 -07:00 |
Alan Mishchenko
|
735a831e13
|
Added memory reporting to &vta.
|
2012-06-22 10:30:22 -07:00 |
Alan Mishchenko
|
675b0892a8
|
Reporing memory usage by the SAT solver in 'bmc3'.
|
2012-06-15 09:51:33 -07:00 |
Alan Mishchenko
|
082d27ede8
|
Added option to compile on windows without DLL support.
|
2012-06-15 08:39:46 -07:00 |
Alan Mishchenko
|
d4399dbf92
|
Misc changes.
|
2012-05-03 19:54:40 +08:00 |
Alan Mishchenko
|
74d0ffee69
|
Misc changes.
|
2012-04-22 19:14:22 -07:00 |
Alan Mishchenko
|
73789120c1
|
Misc changes.
|
2012-04-20 10:12:29 -07:00 |
Alan Mishchenko
|
f16457aaf5
|
Added/moved several APIs.
|
2012-04-10 00:28:36 -07:00 |
Alan Mishchenko
|
993c2027d8
|
Added several new APIs.
|
2012-03-31 16:33:22 -07:00 |
Alan Mishchenko
|
9520736621
|
Added several new APIs to GIA and for file management.
|
2012-03-30 21:09:08 -07:00 |
Alan Mishchenko
|
38494b41a6
|
Moving Vec_Set_t to the vector directory.
|
2012-03-28 10:19:12 -07:00 |
Alan Mishchenko
|
265e3e5cd4
|
Moving Vec_Set_t to the vector directory.
|
2012-03-28 10:13:42 -07:00 |
Alan Mishchenko
|
309bcf2dec
|
Logic sharing for multi-input gates.
|
2012-03-25 01:24:26 -07:00 |
Alan Mishchenko
|
92539a91a0
|
Added one currently unused iterator.
|
2012-03-21 15:27:47 -07:00 |
Alan Mishchenko
|
49c13f4f03
|
Added new procedures to read files.
|
2012-03-11 23:07:27 -07:00 |
Alan Mishchenko
|
66eb3cf472
|
Silencing remaining gcc warnings.
|
2012-03-09 19:08:34 -08:00 |
Niklas Een
|
12d9aaa7b4
|
Some fixes for VTA under Bridge.
|
2012-03-03 11:03:59 -08:00 |
Niklas Een
|
5b800e05de
|
Counterexamples now work in Bridge
|
2012-03-03 10:10:07 -08:00 |
Niklas Een
|
929e5e16e6
|
Some fixes to the Bridge code. More to do.
|
2012-03-03 08:58:25 -08:00 |
Niklas Een
|
1e40c5b79f
|
Removed warning in Abc_Print
|
2012-03-02 16:28:32 -08:00 |
Alan Mishchenko
|
7fa9de2da4
|
Redirecting printf messages.
|
2012-03-02 01:31:44 -08:00 |
Alan Mishchenko
|
c47dc99a94
|
Redirecting printf messages.
|
2012-03-02 01:15:40 -08:00 |
Alan Mishchenko
|
7926d75ecb
|
Adding features related to the communication bridge.
|
2012-03-02 00:57:48 -08:00 |
Alan Mishchenko
|
a6f363d461
|
Created a communication bridge.
|
2012-03-01 22:36:34 -08:00 |
Alan Mishchenko
|
325ac583e6
|
Created a communication bridge.
|
2012-03-01 21:20:18 -08:00 |
Alan Mishchenko
|
3f525b0d42
|
Silenced a gcc warning.
|
2012-02-24 16:18:38 -08:00 |
Alan Mishchenko
|
ea13085fe3
|
Added printout of BMC tents in &ps.
|
2012-02-19 13:33:21 -08:00 |
Alan Mishchenko
|
c2b2e99284
|
Added QuickSort based on 3-way partitioning.
|
2012-02-19 13:19:35 -08:00 |
Alan Mishchenko
|
596bbbe6dc
|
Added QuickSort based on 3-way partitioning.
|
2012-02-19 13:16:51 -08:00 |
Alan Mishchenko
|
97a2e6f29e
|
Isomorphism checking code.
|
2012-02-17 19:04:28 -08:00 |
Alan Mishchenko
|
ee9f66e2c4
|
Isomorphism checking code.
|
2012-02-17 13:19:09 -08:00 |
Alan Mishchenko
|
82cd6ae7cc
|
Silencing some of the gcc warnings.
|
2012-02-17 00:55:58 -08:00 |
Alan Mishchenko
|
32eb2e223d
|
Silencing some of the gcc warnings.
|
2012-02-17 00:53:07 -08:00 |
Alan Mishchenko
|
97856d021a
|
Silencing some of the gcc warnings.
|
2012-02-16 23:40:23 -08:00 |
Alan Mishchenko
|
791b107e7a
|
Silencing some of the gcc warnings.
|
2012-02-16 21:53:16 -08:00 |
Alan Mishchenko
|
a9980135a0
|
Isomorphism checking code.
|
2012-02-14 22:15:49 -08:00 |
Alan Mishchenko
|
c5067f7d04
|
Graph isomorphism checking code.
|
2012-02-11 00:22:05 -08:00 |
Alan Mishchenko
|
274e8ada94
|
Removed unused 'bool' definition and unused memory management macros.
|
2012-02-07 19:59:14 -08:00 |
Alan Mishchenko
|
044149593d
|
Graph isomorphism checking code.
|
2012-01-30 23:11:38 -08:00 |
Alan Mishchenko
|
e511b87237
|
Moving Vec_IntPrint to where it belongs.
|
2012-01-29 21:22:26 -08:00 |
Alan Mishchenko
|
8014f25f6d
|
Major restructuring of the code.
|
2012-01-21 04:30:10 -08:00 |
Alan Mishchenko
|
d8d705c717
|
New hierarchy manager.
|
2012-01-17 23:19:47 -08:00 |
Alan Mishchenko
|
10478a9cbf
|
Variable timeframe abstraction.
|
2012-01-15 20:47:58 -08:00 |
Alan Mishchenko
|
1aeaacc03d
|
Added bit vector.
|
2012-01-13 19:31:58 -08:00 |
Alan Mishchenko
|
095345fc4a
|
Added new name manager and modified hierarchy manager to use it.
|
2012-01-13 15:43:09 -08:00 |
Alan Mishchenko
|
cd4752b565
|
Added utility to sort lines in a file alphabetically.
|
2011-12-17 13:57:56 -08:00 |
Alan Mishchenko
|
5161978d05
|
Started proof transformations.
|
2011-12-01 01:14:32 -05:00 |
Alan Mishchenko
|
3beb36778e
|
Enabled counter-example minimization in 'write_counter'.
|
2011-11-11 20:56:05 -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
|
1dcdba1bee
|
New proof-based abstraction code (bug fix).
|
2011-10-27 10:10:10 -07:00 |
Alan Mishchenko
|
efd310af3e
|
Skip NULL entry when freeing vector of vectors.
|
2011-10-19 14:22:33 +07:00 |
Alan Mishchenko
|
6f0b87dd5c
|
New abstraction code.
|
2011-10-15 22:04:05 +03:00 |
Alan Mishchenko
|
976f5f5a12
|
Changes to Boolean matching.
|
2011-09-24 20:15:54 -07:00 |
Alan Mishchenko
|
8f74276edb
|
Initial changes to enable gate-level abstraction.
|
2011-09-22 09:37:44 -07:00 |
Alan Mishchenko
|
81b040e61c
|
Fixed minor issues having to do with the number of BDD vars used.
|
2011-09-18 17:28:00 -07:00 |
Alan Mishchenko
|
c1edeccc60
|
64-bit portability changes.
|
2011-09-17 16:24:40 -07:00 |
Alan Mishchenko
|
49df91f071
|
Several bug fixes.
|
2011-08-02 12:58:37 +07:00 |
Alan Mishchenko
|
02b04efe9c
|
Changes and simplifications in Vec_Vec_t data-structure.
|
2011-08-01 11:56:19 +07:00 |
Alan Mishchenko
|
d5955db960
|
Added new APIs to integer vector.
|
2011-07-31 20:20:10 +07:00 |
Alan Mishchenko
|
5303465ed6
|
Added new sorting procedures.
|
2011-07-31 16:17:21 +07:00 |
Alan Mishchenko
|
4ffe37b34b
|
Added new sorting procedures.
|
2011-07-31 16:16:49 +07:00 |
Alan Mishchenko
|
67e84b719d
|
Enhancing printing of counter-examples.
|
2011-07-25 20:33:55 +07:00 |
Alan Mishchenko
|
15cc374fe3
|
Updated 'iprove' to generate seq CEX when CEC fails.
|
2011-06-25 09:23:44 -07:00 |
Alan Mishchenko
|
6e74c46bcf
|
Enabled new BDD-based reachability engine 'reachy'.
|
2011-04-13 22:41:54 -07:00 |
Alan Mishchenko
|
302f41e908
|
Added procedure to vector package and manager template file.
|
2011-04-10 12:55:57 -07:00 |
Alan Mishchenko
|
a28fe0d324
|
Unsuccessful attempt to improve PDR and a few minor changes.
|
2011-04-07 13:49:03 -07:00 |
Alan Mishchenko
|
4dcf8cee2d
|
Improvements in Vec_Vec_t.
|
2011-03-27 11:35:31 -07:00 |
Alan Mishchenko
|
d97e5d6803
|
Added Max/Min/Abs as static inline functions.
|
2011-03-27 11:35:18 -07:00 |
Alan Mishchenko
|
badbb5a6cc
|
Fixing bugs in the new procedures added to the library.
|
2011-03-05 16:17:12 -08:00 |
Alan Mishchenko
|
edcb769b3e
|
Adding new procedures to the library.
|
2011-03-05 13:09:11 -08:00 |
Alan Mishchenko
|
148a786b69
|
Made abc.h independent of CUDD and Extra.
|
2011-03-03 12:28:52 -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
|
2619edf8c0
|
Added two new APIs for reading/writing CEX from/into ABC.
|
2011-02-19 16:43:00 -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
|
d99de60e6c
|
Portability changes to the st package.
|
2011-02-13 13:40:21 -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
|
1d54983bc4
|
Minor changes to hash table and utilSignal.c.
|
2011-02-01 16:35:50 -08:00 |
Baruch Sterin
|
35e05b7e5a
|
merge pyabc changes into mainline
|
2011-02-01 16:19:38 -08:00 |
Baruch Sterin
|
3a41da37a2
|
src/misc/util/utilSignal.c
|
2011-02-01 15:54:01 -08:00 |
Alan Mishchenko
|
d4291dab37
|
Cumulative changes of the last two weeks.
|
2011-02-01 15:47:55 -08:00 |
Baruch Sterin
|
b538a5fad0
|
1. Replace system() with a function that responds to SIGINT. 2. Add functions to cleanup temporary files on SIGINT. 3. Fix bugs related to signal handling.
|
2011-02-01 11:13:53 -08:00 |
Alan Mishchenko
|
ae4b51351c
|
Cumulative changes in the last few weeks.
|
2011-01-13 12:38:59 -08:00 |
Alan Mishchenko
|
ffb04d244f
|
Code formatting change
|
2010-11-29 01:40:49 -08:00 |
Alan Mishchenko
|
cdcbd60b39
|
Adding missing license agreements
|
2010-11-29 01:23:21 -08:00 |
Baruch Sterin
|
093774c1b8
|
fixed compilation in linux
|
2010-11-01 02:06:26 -07:00 |
Alan Mishchenko
|
6130e39b18
|
initial commit of public abc
|
2010-11-01 01:35:04 -07:00 |
Alan Mishchenko
|
51a646a355
|
Version abc90901
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:05:13 -07:00 |
Alan Mishchenko
|
b288bac6b3
|
Version abc90807
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:05:02 -07:00 |
Alan Mishchenko
|
da65e88e3b
|
Version abc90804
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:04:59 -07:00 |
Alan Mishchenko
|
0398ced824
|
Version abc90714
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:04:53 -07:00 |
Alan Mishchenko
|
df6fdd1dff
|
Version abc90408
|
2009-04-08 08:01:00 -07:00 |
Alan Mishchenko
|
770bc99e79
|
Version abc90315
|
2009-03-15 08:01:00 -07:00 |
Alan Mishchenko
|
32314347ba
|
Version abc90310
|
2009-03-10 08:01:00 -07:00 |
Alan Mishchenko
|
0871bffae3
|
Version abc90215
|
2009-02-15 08:01:00 -08:00 |
Alan Mishchenko
|
f936cc0680
|
Version abc90118
|
2009-01-18 08:01:00 -08:00 |
Alan Mishchenko
|
c9ad5880cc
|
Version abc81029
|
2008-10-29 08:01:00 -07:00 |
Alan Mishchenko
|
e917dda1d3
|
Version abc81013
|
2008-10-13 08:01:00 -07:00 |
Alan Mishchenko
|
eb75697fe0
|
Version abc81004
|
2008-10-04 08:01:00 -07:00 |
Alan Mishchenko
|
91effd8148
|
Version abc80922
|
2008-09-22 08:01:00 -07:00 |
Alan Mishchenko
|
2c96c8af36
|
Version abc80721
|
2008-07-21 08:01:00 -07:00 |
Alan Mishchenko
|
13f52980da
|
Version abc80718
|
2008-07-18 08:01:00 -07:00 |
Alan Mishchenko
|
d63a0cbbfd
|
Version abc80717
|
2008-07-17 08:01:00 -07:00 |
Alan Mishchenko
|
303baf27cf
|
Version abc80702
|
2008-07-02 08:01:00 -07:00 |
Alan Mishchenko
|
fa67e3c19e
|
Version abc80701_2
|
2008-07-01 20:01:00 -07:00 |
Alan Mishchenko
|
4a9789e58d
|
Version abc80701
|
2008-07-01 08:01:00 -07:00 |
Alan Mishchenko
|
6da56f1f0f
|
Version abc80516
|
2008-05-16 08:01:00 -07:00 |