Commit Graph

1159 Commits

Author SHA1 Message Date
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