Alan Mishchenko
|
99444597f7
|
New semi-canonical form computation package.
|
2012-08-07 20:19:56 -07:00 |
Alan Mishchenko
|
f9b032ee02
|
Scalable gate-level abstraction.
|
2012-08-07 11:46:50 -07:00 |
Alan Mishchenko
|
c35471dac4
|
Scalable gate-level abstraction.
|
2012-08-07 10:43:01 -07:00 |
Alan Mishchenko
|
173303b464
|
Scalable gate-level abstraction.
|
2012-08-06 22:03:35 -07:00 |
Alan Mishchenko
|
8e31b4c047
|
Scalable gate-level abstraction.
|
2012-08-06 22:02:50 -07:00 |
Alan Mishchenko
|
b3dd1f82f1
|
New cut-based refinement.
|
2012-08-06 21:59:50 -07:00 |
Alan Mishchenko
|
ca9803fc98
|
Scalable gate-level abstraction.
|
2012-08-06 21:59:14 -07:00 |
Alan Mishchenko
|
94949287fe
|
Changing the default value '&gla -n' to the opposite.
|
2012-08-06 21:58:18 -07:00 |
Alan Mishchenko
|
4c36d2513c
|
New semi-canonical form computation package.
|
2012-08-06 19:56:21 -07:00 |
Alan Mishchenko
|
1917321c4e
|
Scalable gate-level abstraction.
|
2012-08-06 09:58:34 -07:00 |
Alan Mishchenko
|
6a9eaec3b5
|
Changing the default value '&gla -n' to the opposite.
|
2012-08-06 07:44:55 -07:00 |
Alan Mishchenko
|
294c06f162
|
Scalable gate-level abstraction.
|
2012-08-04 09:37:49 -07:00 |
Alan Mishchenko
|
a01b479013
|
Scalable gate-level abstraction.
|
2012-08-03 21:44:00 -07:00 |
Alan Mishchenko
|
5760c3225d
|
Scalable gate-level abstraction.
|
2012-08-03 18:31:16 -07:00 |
Alan Mishchenko
|
30ae05f0a5
|
Scalable gate-level abstraction.
|
2012-08-03 18:25:47 -07:00 |
Alan Mishchenko
|
e9af6c3cec
|
Scalable gate-level abstraction.
|
2012-08-02 23:44:48 -07:00 |
Alan Mishchenko
|
cb66aa429d
|
Scalable gate-level abstraction.
|
2012-08-02 10:54:21 -07:00 |
Alan Mishchenko
|
b939e16006
|
Scalable gate-level abstraction.
|
2012-08-02 09:44:48 -07:00 |
Alan Mishchenko
|
352060122b
|
Scalable gate-level abstraction.
|
2012-08-02 09:40:19 -07:00 |
Alan Mishchenko
|
fe93162114
|
Scalable gate-level abstraction.
|
2012-08-02 01:05:14 -07:00 |
Alan Mishchenko
|
8822e811ca
|
Scalable gate-level abstraction.
|
2012-08-02 00:29:57 -07:00 |
Alan Mishchenko
|
68c70bcb8e
|
Scalable gate-level abstraction.
|
2012-08-01 13:46:46 -07:00 |
Alan Mishchenko
|
99e8ef14cb
|
Scalable gate-level abstraction.
|
2012-08-01 13:43:33 -07:00 |
Alan Mishchenko
|
e7ddde3f5a
|
Scalable gate-level abstraction.
|
2012-08-01 08:59:02 -07:00 |
Alan Mishchenko
|
e3e4a98792
|
Scalable gate-level abstraction.
|
2012-07-31 21:18:39 -07:00 |
Alan Mishchenko
|
dc56a65582
|
Scalable gate-level abstraction.
|
2012-07-31 14:51:48 -07:00 |
Alan Mishchenko
|
7517c78522
|
Scalable gate-level abstraction.
|
2012-07-31 12:02:06 -07:00 |
Alan Mishchenko
|
a457cf496a
|
Scalable gate-level abstraction.
|
2012-07-31 10:36:03 -07:00 |
Alan Mishchenko
|
b20ca62e00
|
Scalable gate-level abstraction.
|
2012-07-31 00:00:34 -07:00 |
Alan Mishchenko
|
51d5055e68
|
Saving variable activity during rollback.
|
2012-07-30 12:02:30 -07:00 |
Alan Mishchenko
|
a22db31d6d
|
Saving variable activity during rollback.
|
2012-07-30 11:47:24 -07:00 |
Alan Mishchenko
|
ed564664f1
|
Disabling learned clause removal when incremental proof-logging is running (tends to generate smaller abstarctions).
|
2012-07-30 11:31:26 -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
|
401aa6994a
|
Fixing a problem with printing out factored forms.
|
2012-07-30 10:29:35 -07:00 |
Alan Mishchenko
|
216fc33a47
|
Fixed compiler warnings.
|
2012-07-29 22:36:21 -07:00 |
Alan Mishchenko
|
8982bf58cb
|
Reducing memory usage in proof-based abstraction.
|
2012-07-29 22:31:00 -07:00 |
Alan Mishchenko
|
5838789ee7
|
Scalable gate-level abstraction.
|
2012-07-29 12:34:59 -07:00 |
Alan Mishchenko
|
8a2d237f78
|
Adding memory reporting to vectors.
|
2012-07-29 12:34:32 -07:00 |
Alan Mishchenko
|
e8d690f2a4
|
Adding command 'testdec'.
|
2012-07-28 18:30:21 -07:00 |
Alan Mishchenko
|
1b18583840
|
Fixed the problem with 'write_cnf' after recent changes to the SAT solver.
|
2012-07-28 14:55:55 -07:00 |
Alan Mishchenko
|
1e159a826e
|
Started implementing command 'testdec'.
|
2012-07-28 12:42:17 -07:00 |
Alan Mishchenko
|
4598c76e88
|
Scalable gate-level abstraction.
|
2012-07-28 12:18:59 -07:00 |
Alan Mishchenko
|
18737f7408
|
Fixed the problem with 'write_cnf' after recent changes to the SAT solver.
|
2012-07-28 11:03:56 -07:00 |
Alan Mishchenko
|
467728828e
|
Scalable gate-level abstraction.
|
2012-07-27 22:58:26 -07:00 |
Alan Mishchenko
|
7e486af832
|
Minor updates to the BMC engines.
|
2012-07-27 15:59:20 -07:00 |
Alan Mishchenko
|
a57a452d7e
|
Changes in command 'bm' to report timeout (thanks to S.W.)
|
2012-07-26 22:55:20 -07:00 |
Alan Mishchenko
|
950777ed50
|
Fixing interpolation to run without resource limits by default.
|
2012-07-25 20:42:55 -07:00 |
Alan Mishchenko
|
bb68d0b7f6
|
Removed unused files from the project.
|
2012-07-25 12:42:25 -07:00 |
Alan Mishchenko
|
b2ad079a2a
|
Allow for skipping structural hashing when reading GIA from file.
|
2012-07-25 12:37:19 -07:00 |
Alan Mishchenko
|
160b196a70
|
Updated code for lazy man's synthesis.
|
2012-07-25 12:37:07 -07:00 |
Alan Mishchenko
|
7dc8c81ff6
|
Allow for skipping structural hashing when reading GIA from file.
|
2012-07-25 08:59:24 -07:00 |
Alan Mishchenko
|
a40c13a93c
|
Recording and reusing learned util clauses in bmc2.
|
2012-07-22 22:28:24 -07:00 |
Alan Mishchenko
|
2379dea445
|
Recording and reusing learned util clauses in bmc3.
|
2012-07-22 16:52:24 -07:00 |
Alan Mishchenko
|
8d5fdf6232
|
Scalable gate-level abstraction.
|
2012-07-21 14:31:55 -07:00 |
Alan Mishchenko
|
1d89ae52c3
|
Correcting &gla to update status as 'sat' after CEX is found.
|
2012-07-20 20:22:10 -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
|
f09afdf24c
|
Added switch &trim -c to additionally remove direct connections (POs fed by PIs).
|
2012-07-20 13:52:39 -07:00 |
Alan Mishchenko
|
aa78ce56e7
|
Updated code for lazy man's synthesis.
|
2012-07-20 11:52:51 -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
|
febe2c6ae0
|
Merging recent changes.
|
2012-07-20 08:17:08 -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
|
a8f4d4e6bc
|
Making GIA use independent truth table number storage when computing truth tables.
|
2012-07-19 08:41:38 -07:00 |
Alan Mishchenko
|
72c09b86a0
|
Scalable gate-level abstraction.
|
2012-07-18 23:53:02 -07:00 |
Alan Mishchenko
|
1fe2ba9ac0
|
Enabling &gla for combinational miters.
|
2012-07-18 23:52:41 -07:00 |
Alan Mishchenko
|
6b2da3978f
|
Adding new file to the build file.
|
2012-07-17 20:46:45 -07:00 |
Alan Mishchenko
|
1b95ee06f1
|
Small bug in bmc2 timeout.
|
2012-07-16 07:48:45 -07:00 |
Alan Mishchenko
|
226c24e49d
|
Updated code for lazy man's synthesis.
|
2012-07-15 15:56:03 -07:00 |
Alan Mishchenko
|
96d7699698
|
Updated code for lazy man's synthesis.
|
2012-07-15 15:54:36 -07:00 |
Alan Mishchenko
|
1ca94c1023
|
Added new refinement manager for &gla and &abs_refine.
|
2012-07-14 16:43:43 -07:00 |
Alan Mishchenko
|
cfc7fe7d31
|
Added new refinement manager for &gla and &abs_refine.
|
2012-07-14 16:39:11 -07:00 |
Alan Mishchenko
|
94193472c8
|
Fixing assertion mismatch in bmc2.
|
2012-07-14 09:25:18 -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
|
3c4351aee4
|
Debugging a proof error.
|
2012-07-13 19:06:32 -07:00 |
Alan Mishchenko
|
8c162f0577
|
Debugging a proof error.
|
2012-07-13 18:56:15 -07:00 |
Alan Mishchenko
|
08bb2e70b7
|
Debugging a proof error.
|
2012-07-13 18:51:24 -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
|
5ec4db2d44
|
Debugging a proof error.
|
2012-07-13 18:11:02 -07:00 |
Alan Mishchenko
|
7913c1d84f
|
Debugging a proof error.
|
2012-07-13 17:58:56 -07:00 |
Alan Mishchenko
|
c25f488a83
|
Debugging a proof error.
|
2012-07-13 17:53:08 -07:00 |
Alan Mishchenko
|
6578d9cd00
|
Debugging a proof error.
|
2012-07-13 17:46:30 -07:00 |
Alan Mishchenko
|
4051572726
|
Debugging a proof error.
|
2012-07-13 17:39:52 -07:00 |
Alan Mishchenko
|
0f82d82ba0
|
Debugging a proof error.
|
2012-07-13 17:36:31 -07:00 |
Alan Mishchenko
|
f37d0544de
|
Debugging a proof error.
|
2012-07-13 17:23:30 -07:00 |
Alan Mishchenko
|
47b5ad1dfb
|
Debugging a proof error.
|
2012-07-13 17:17:12 -07:00 |
Alan Mishchenko
|
7b367f5ecb
|
Debugging a proof error.
|
2012-07-13 17:06:22 -07:00 |
Alan Mishchenko
|
04d1c4e476
|
Fixing compiler warning.
|
2012-07-13 16:35:52 -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
|
be95437d1a
|
Debugging a proof error.
|
2012-07-13 15:44:45 -07:00 |
Alan Mishchenko
|
f54bf25d70
|
Debugging a proof error.
|
2012-07-13 15:12:21 -07:00 |
Alan Mishchenko
|
d3ad7fbaf3
|
Several small changes and fixes.
|
2012-07-13 15:02:46 -07:00 |
Alan Mishchenko
|
86a0ae0bca
|
Removed useless file.
|
2012-07-12 19:07:24 -07:00 |
Alan Mishchenko
|
743ab55fad
|
Upgraded &equiv3 to periodically restart simulation from the init state.
|
2012-07-12 18:56:26 -07:00 |
Alan Mishchenko
|
97d2c9a264
|
Added procedure for checking satisfied clauses.
|
2012-07-12 18:55:24 -07:00 |
Alan Mishchenko
|
17305bd563
|
Fixing temporary linker problem.
|
2012-07-12 18:54:44 -07:00 |