Commit Graph

915 Commits

Author SHA1 Message Date
Alan Mishchenko c17a22ef8a Disabled verbose print-out in the SAT solvers. 2012-02-26 08:51:14 -08:00
Alan Mishchenko b06908d1e8 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default (bug fix). 2012-02-25 15:54:11 -08:00
Alan Mishchenko 3f525b0d42 Silenced a gcc warning. 2012-02-24 16:18:38 -08:00
Alan Mishchenko b4fe108d86 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. 2012-02-24 16:11:49 -08:00
Alan Mishchenko 3552d39b71 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. 2012-02-24 13:37:31 -08:00
Alan Mishchenko d80f43a185 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. 2012-02-24 13:21:32 -08:00
Alan Mishchenko 8f4457772a Added a way to disable support for dynamic linking. 2012-02-24 09:44:16 -08:00
Alan Mishchenko c20d29e7e7 Silenced a gcc warning. 2012-02-23 13:49:49 -08:00
Baruch Sterin f42131935e pyabc: silnce more warnings 2012-02-23 13:45:51 -08:00
Baruch Sterin 4ade9fc7c8 pyabc: python 2.6 compatibility fix for previous commit (which silenced warnings) 2012-02-23 13:28:07 -08:00
Baruch Sterin af51bdaf3e pyabc: silenced warnings in gcc 2012-02-23 13:01:17 -08:00
Alan Mishchenko a87a3b4e33 Bug fix in stadard cell library representation. 2012-02-23 11:58:59 -08:00
Baruch Sterin 871684d2a0 pyabc changes with main branch 2012-02-23 11:11:21 -08:00
Baruch Sterin b879786e73 pyabc: added a function pyabc.iso_eq_classes() that retrieves the results of the "&iso" command 2012-02-23 11:09:57 -08:00
Alan Mishchenko 99e7d1d193 Bug fix in stadard cell library representation. 2012-02-23 10:24:01 -08:00
Alan Mishchenko 1d25ae3b1a Experiment with technology mapping. 2012-02-22 17:54:24 -08:00
Alan Mishchenko d2cab85976 Adding flag -s to &put to disable status clearing. 2012-02-22 08:06:22 -08:00
Alan Mishchenko 8ba2398138 Undoing a previuos change to not reset the status after &put. 2012-02-22 00:46:52 -08:00
Alan Mishchenko db3a005402 Experiment with technology mapping. 2012-02-20 21:34:50 -08:00
Alan Mishchenko e60d6c94a3 Experiment with technology mapping. 2012-02-20 21:33:51 -08:00
Alan Mishchenko 18ea60a06b Isomorphism checking code. 2012-02-20 16:43:15 -08:00
Alan Mishchenko 9f71a9f67b Isomorphism checking code. 2012-02-20 16:09:20 -08:00
Alan Mishchenko e43ca9f850 Isomorphism checking code. 2012-02-19 15:05:59 -08:00
Alan Mishchenko 2377ae60e9 Isomorphism checking code. 2012-02-19 14:52:43 -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 9aab58f601 Isomorphism checking code. 2012-02-19 12:57:58 -08:00
Alan Mishchenko af8cac095d Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity). 2012-02-19 10:41:16 -08:00
Alan Mishchenko c9147d76cc Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity). 2012-02-19 09:55:52 -08:00
Alan Mishchenko 7ca9c116df Isomorphism checking code. 2012-02-18 19:20:02 -08:00
Alan Mishchenko 78cad5e176 Isomorphism checking code. 2012-02-17 23:26:20 -08:00
Alan Mishchenko 97a2e6f29e Isomorphism checking code. 2012-02-17 19:04:28 -08:00
Alan Mishchenko 5d7c568589 Changes to properly save current GIA after &miter -t and not erase the comb cex after &put. 2012-02-17 15:51:12 -08:00
Alan Mishchenko ee9f66e2c4 Isomorphism checking code. 2012-02-17 13:19:09 -08:00
Alan Mishchenko f2a413029c Silencing some of the gcc warnings. 2012-02-17 12:46:08 -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 fe2d7d9612 Silencing some of the gcc warnings. 2012-02-17 00:24:38 -08:00
Alan Mishchenko 4743884de4 Silencing some of the gcc warnings. 2012-02-17 00:12:53 -08:00
Alan Mishchenko 2d316b86e2 Silencing some of the gcc warnings. 2012-02-17 00:06:39 -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 16dc02e7f6 Improved memory management of proof-logging and propagated changes. 2012-02-16 20:54:41 -08:00
Alan Mishchenko f1dba69c57 Improved memory management of proof-logging and propagated changes. 2012-02-16 14:23:52 -08:00
Alan Mishchenko ce945006e1 Changing how BMC report runtime. 2012-02-16 00:28:33 -08:00
Alan Mishchenko 8587ebe797 Variable timeframe abstraction. 2012-02-16 00:11:09 -08:00
Alan Mishchenko ecd14d4daf Isomorphism checking code. 2012-02-15 18:40:05 -08:00
Alan Mishchenko e405d71398 Isomorphism checking code. 2012-02-14 22:16:01 -08:00
Alan Mishchenko a9980135a0 Isomorphism checking code. 2012-02-14 22:15:49 -08:00
Alan Mishchenko faa934e2e6 Added restarts to PDR. 2012-02-14 00:17:01 -08:00
Alan Mishchenko 77b5dc261e Added restarts to PDR. 2012-02-13 23:31:01 -08:00
Alan Mishchenko e0650dce0a Timeout crash fix in 'reachy'. 2012-02-13 21:10:15 -08:00
Alan Mishchenko 59ea100dbf Variable timeframe abstraction. 2012-02-13 20:40:38 -08:00
Alan Mishchenko d931de7feb Variable timeframe abstraction. 2012-02-13 20:03:55 -08:00
Alan Mishchenko 6f4bb33ce1 Variable timeframe abstraction. 2012-02-13 14:35:00 -08:00
Alan Mishchenko f80841a5fd Variable timeframe abstraction. 2012-02-13 14:17:01 -08:00
Alan Mishchenko d0713831a0 Lazy man's logic synthesis. 2012-02-12 17:30:05 -08:00
Alan Mishchenko 9f331ae915 Isomorphism checking code. 2012-02-12 15:45:07 -08:00
Alan Mishchenko d9edb7e549 Variable timeframe abstraction. 2012-02-12 02:16:36 -08:00
Alan Mishchenko 862ebb214d Variable timeframe abstraction. 2012-02-11 22:54:59 -08:00
Alan Mishchenko 49c5beefd4 Variable timeframe abstraction. 2012-02-11 22:30:04 -08:00
Alan Mishchenko 95d7b478fd Variable timeframe abstraction. 2012-02-11 21:56:05 -08:00
Alan Mishchenko 309ab1c12b Variable timeframe abstraction. 2012-02-11 20:48:23 -08:00
Alan Mishchenko d81aa6d697 Variable timeframe abstraction. 2012-02-11 19:32:45 -08:00
Baruch Sterin 33261c33cb pyabc: replace 'bool' with 'int' as it was removed from the rest of ABC 2012-02-11 15:01:55 -08:00
Alan Mishchenko c395afe225 Graph isomorphism checking code. 2012-02-11 14:13:11 -08:00
Alan Mishchenko 112f797c73 Added switch -f to 'print_io' to suppress printing flops. 2012-02-11 00:43:37 -08:00
Alan Mishchenko c5067f7d04 Graph isomorphism checking code. 2012-02-11 00:22:05 -08:00
Alan Mishchenko 71891354b4 Bug fixes in &cec command. 2012-02-10 00:07:31 -08:00
Alan Mishchenko b186f362a7 Bug fix in flop-level abstraction refinement. 2012-02-09 13:38:09 -08:00
Alan Mishchenko 274e8ada94 Removed unused 'bool' definition and unused memory management macros. 2012-02-07 19:59:14 -08:00
Alan Mishchenko 25859eefb6 Graph isomorphism checking code. 2012-02-02 15:45:48 -08:00
Alan Mishchenko 16fd67f0ab Trying to fix a false-positive due to incorrect inductive termination check in 'int' when K is more than 1 (not fixed yet). 2012-02-01 14:54:32 -08:00
Alan Mishchenko 61211df4ff Lazy man's logic synthesis. 2012-02-01 12:24:04 -08:00
Alan Mishchenko 5004aa1940 Graph isomorphism checking code. 2012-01-30 23:16:40 -08:00
Alan Mishchenko 044149593d Graph isomorphism checking code. 2012-01-30 23:11:38 -08:00
Alan Mishchenko 7ea40494eb Graph isomorphism checking code. 2012-01-29 21:22:54 -08:00
Alan Mishchenko e511b87237 Moving Vec_IntPrint to where it belongs. 2012-01-29 21:22:26 -08:00
Alan Mishchenko 5e91f13247 Variable timeframe abstraction. 2012-01-28 23:17:31 -08:00
Alan Mishchenko 095bf1c91b Variable timeframe abstraction. 2012-01-28 23:03:25 -08:00
Alan Mishchenko 5e1c28338b Generation of dual-rail miter. 2012-01-28 21:09:31 -08:00
Alan Mishchenko 99b408fcb1 Generation of dual-rail miter. 2012-01-28 20:10:34 -08:00
Alan Mishchenko 5aeab257ed Generation of dual-rail miter. 2012-01-28 15:05:33 -08:00
Alan Mishchenko a2df331852 Variable timeframe abstraction. 2012-01-28 13:48:48 -08:00
Alan Mishchenko 7a87f20c18 Variable timeframe abstraction. 2012-01-27 00:57:42 -08:00
Alan Mishchenko ce0e8caf79 Variable timeframe abstraction. 2012-01-27 00:48:06 -08:00
Alan Mishchenko c7e855619a Variable timeframe abstraction. 2012-01-24 14:39:49 -08:00
Alan Mishchenko 94d35a2592 Variable timeframe abstraction. 2012-01-24 01:04:56 -08:00
Alan Mishchenko f8e933c718 Variable timeframe abstraction. 2012-01-23 13:45:46 -08:00
Alan Mishchenko c39fd3741a Added returning counter-example after BMC, which was recently added to 'dprove'. 2012-01-23 12:41:55 -08:00
Alan Mishchenko 14457af21a Bug fix for incorrect memory allocation in main SAT solver, leading to crashes in 'dsec' (correction to the previous fix). 2012-01-23 12:21:29 -08:00
Alan Mishchenko 3906e37c12 Bug fix for incorrect memory allocation in main SAT solver, leading to crashes in 'dsec'. 2012-01-22 22:24:23 -08:00
Alan Mishchenko fb918249ca Variable timeframe abstraction. 2012-01-21 22:57:18 -08:00
Baruch Sterin 6e72e2fb35 pyabc: adapt build to recent changes in the rest of ABC 2012-01-21 18:21:03 -08:00
Alan Mishchenko 8014f25f6d Major restructuring of the code. 2012-01-21 04:30:10 -08:00
Alan Mishchenko c44cc5de94 Deleting file added by mistake. 2012-01-20 20:30:24 -08:00
Alan Mishchenko 2c50c2c5c0 Preserving CI/CO varible names when moving between the main space and &-space. 2012-01-20 19:54:26 -08:00
Alan Mishchenko 7d4545126d Variable timeframe abstraction. 2012-01-20 19:04:01 -08:00
Alan Mishchenko 719b06f912 Variable timeframe abstraction. 2012-01-20 17:55:34 -08:00