luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
4,977 Commits 27 Branches 57 Tags 58 MiB
Commit Graph

2758 Commits

Author SHA1 Message Date
Alan Mishchenko 3f35ac8180 New command 'lutexact'. 2017-12-05 18:22:27 -08:00
Alan Mishchenko 1743979b75 Adding switch -a to 'write_verilog' to write factored forms without XORs and MUXes. 2017-12-03 14:39:11 -08:00
Alan Mishchenko a49dfbcf91 Portability changes for gcc-6 suggested by Clifford. 2017-12-03 08:08:36 -08:00
Alan Mishchenko 46175d0429 Portability changes for gcc-6 suggested by Clifford. 2017-12-02 19:47:24 -08:00
Alan Mishchenko 3cc4080c55 Portability changes for gcc-6 suggested by Clifford. 2017-12-02 19:44:08 -08:00
Baruch Sterin 7bcfe64369 C++ comaptibility: add namespace support to Glucose 2017-11-23 23:32:44 -08:00
Baruch Sterin 77ca1b7470 C++ compatibility: fix bad pointer comparison 2017-11-23 23:32:42 -08:00
Alan Mishchenko d85bc1dd68 Changes to make GIA structural hashing use a dedicated array instead of pObj->Value. 2017-11-13 18:50:04 -08:00
Alan Mishchenko 716969190a Profiling quantification and other changes. 2017-11-06 16:43:32 -08:00
Alan Mishchenko accf4825e5 Adding API to dump MiniAIG into a Verilog file and other small changes. 2017-10-22 15:44:13 -07:00
Alan Mishchenko 15908929ca Adding random search in exact synthesis. 2017-10-20 07:49:01 +09:00
Alan Mishchenko 8f690fe862 Integrating old SAT solver into majexact and twoexact. 2017-10-19 13:38:09 +09:00
Alan Mishchenko c1b4b79e99 Integrating Glucose into &qbf. 2017-10-17 13:53:48 +09:00
Alan Mishchenko 222d7c7a92 Fix the build. 2017-10-11 18:12:20 +07:00
Alan Mishchenko 711ea3dfec Another variation on exact synthesis. 2017-10-11 18:07:35 +07:00
Alan Mishchenko f97b8d2882 Improvements to SAT based SOP computation. 2017-10-06 17:16:16 +03:00
Alan Mishchenko 02972e53c2 Improvements to truth table manipulation. 2017-10-05 22:39:38 +03:00
Alan Mishchenko d0286dce37 Fixing minimize_assuptions using Glucose. 2017-10-02 21:31:34 +03:00
Alan Mishchenko 05ca7dbf47 Adding printout of slack distribution for mapped networks. 2017-10-02 13:44:48 +03:00
Alan Mishchenko c272188946 Exact synthesis of majority gates. 2017-10-01 19:49:28 +03:00
Alan Mishchenko d3152aefa7 Exact synthesis of majority gates. 2017-10-01 18:00:09 +03:00
Alan Mishchenko c696ae95d0 Maintenance and updates. 2017-09-24 23:38:01 -07:00
Alan Mishchenko 287f9efcce Maintenance and updates. 2017-09-20 19:27:46 -07:00
Alan Mishchenko 1e0bbef1ef Uncommenting handling of initial values of the flops. 2017-09-19 17:29:03 -07:00
Alan Mishchenko 36858c5365 Enabling Glucose in SAT sweeping: &fraig -g. 2017-09-18 09:36:08 -07:00
Alan Mishchenko b5d42e8bf3 Adding support for Dimacs input to &satoko. 2017-09-16 13:13:30 -07:00
Alan Mishchenko b63e3ee4b4 Experiment with mapping. 2017-09-15 12:40:43 -07:00
Alan Mishchenko 4c0b78cf7f Updates to &bmcs to help debugging. 2017-09-12 11:43:14 -07:00
Alan Mishchenko efbf5208a2 Adding switch '-c' to 'dsec' to disable internal netlist check. 2017-09-09 08:24:57 -07:00
Alan Mishchenko af4c76e21a Disabling CNF simplification in &bmcs -g. 2017-09-07 19:37:46 -07:00
Alan Mishchenko ba0d855fd4 Trying to enable CNF simplification in &bmcs -g. 2017-09-07 19:16:13 -07:00
Alan Mishchenko 97dd6019bf Integrating Glucose into bmc3 -g. 2017-09-06 19:56:53 -07:00
Alan Mishchenko f68bd519c6 Integrating Glucose into &bmcs -g. 2017-09-06 17:57:44 -07:00
Alan Mishchenko 8063887ffe Compiler warning. 2017-09-06 16:40:38 -07:00
Alan Mishchenko 9e46ebe3f8 Adding Glucose 3.0 as a separate package. 2017-09-06 16:28:00 -07:00
Alan Mishchenko 7857b7fd8b Renaming command-line option '-s' to be '-q' in 'pdr'. 2017-09-06 08:39:23 -07:00
Alan Mishchenko f06056d85d Changes to 'pdr' to run with updated Satoko. 2017-09-06 08:34:04 -07:00
Alan Mishchenko 4b286febe0 Several small changes. 2017-09-06 07:29:12 -07:00
Alan Mishchenko 5a9fded57f Several small changes. 2017-09-05 21:54:27 -07:00
Alan Mishchenko ecae67e3bf Several changes to various packages. 2017-09-04 15:57:00 -07:00
Alan Mishchenko 23d36a8d56 Integrating Satoko into 'bmc' and 'bmc2'. 2017-08-16 14:20:52 +07:00
Alan Mishchenko 2280c2e8fe Trying &bmcs with external solvers. 2017-08-15 18:13:31 +07:00
Alan Mishchenko ca87c1a6a0 Unfold several timeframes at the same time in &bmcs. 2017-08-15 11:36:15 +07:00
Alan Mishchenko a64957a526 Adding an option to bmc3 to use Satoko intead of the default SAT solver. 2017-08-13 17:53:19 +07:00
Alan Mishchenko 8ae4ed5de5 Experiments with BMC. 2017-08-13 15:19:49 +07:00
Alan Mishchenko ab8f784b6a Experiments with BMC. 2017-08-13 13:37:48 +07:00
Baruch Sterin cf427690a5 add frame done callback support for command &bmcs 2017-08-09 12:01:07 -07:00
Baruch Sterin 590ae69652 add a new field to the ABC Frame. The new field is a callback that may be called by a BMC-like engine when a frame is done and a PO is either known to be SAT or UNSAT up to a specific frame 2017-08-09 12:00:59 -07:00
Alan Mishchenko a1d1a7b8cd Experiments with BMC. 2017-08-09 17:38:40 +09:00
Alan Mishchenko 9edf6ea091 New commands for backing up networks. 2017-08-04 14:40:51 +09:00
Alan Mishchenko ee4d794111 Transforming miter by swapping sides. 2017-07-23 11:12:37 +07:00
Alan Mishchenko 2e56f44c66 Compiler warnings. 2017-07-22 11:41:17 +07:00
Alan Mishchenko 9ff1776d06 Experiments with logic optimization. 2017-07-21 12:38:18 +07:00
Alan Mishchenko 4886a4ef4c Adding new type of MUX blasting. 2017-07-07 23:40:59 -07:00
Alan Mishchenko 1676df19e7 Adding new command line options for &verify and &synch2. 2017-07-06 21:13:53 -07:00
Alan Mishchenko 0b7dcbbcfb Merged in boschmitt/abc (pull request #77) 
Small fixes for C++ compilers
 2017-07-04 22:24:57 +00:00
Alan Mishchenko 859e769f22 Synchronizing various data-structures. 2017-07-04 15:23:51 -07:00
Bruno Schmitt f302e6f6ef Small fixes for C++ compilers 2017-07-04 09:35:42 +02:00
Alan Mishchenko bf6a053c64 Saturating floating point computation. 2017-07-01 13:48:31 -07:00
Alan Mishchenko 584d52ba85 Temp changes 2017-06-15 23:26:24 -07:00
Yen-Sheng Ho 584e28e8f4 merge 2017-06-06 23:16:55 -07:00
Yen-Sheng Ho 10f5e944c9 %pdra: fixed a bug 2017-06-06 23:15:38 -07:00
Alan Mishchenko e140ef7e5a Bug fix in SMT handling: 'distinct' with more than two inputs. 2017-06-05 12:36:26 +02:00
Alan Mishchenko 8de04d36b3 Several new procedures for GIA manipulation. 2017-06-01 15:42:50 +02:00
Alan Mishchenko 867c90d114 Small change to gate names. 2017-05-16 22:21:57 -07:00
Alan Mishchenko 41314cea01 Adding switch %blast -d to dump dual-output miter after blasting. 2017-04-29 18:34:56 -07:00
Alan Mishchenko 0de189f4db Two small fixes. 2017-04-24 08:52:12 -07:00
Alan Mishchenko bef247a4cb Logic restructuring after mapping. 2017-04-23 09:45:23 -07:00
Alan Mishchenko 4124a00d4b Logic restructuring after mapping. 2017-04-19 22:53:01 -07:00
Alan Mishchenko 7d15b00e13 Logic restructuring after mapping. 2017-04-19 22:51:19 -07:00
Alan Mishchenko f401c17fac Logic restruturing after mapping. 2017-04-17 17:57:41 -04:00
Alan Mishchenko fb12c23ad5 Logic restruturing after mapping. 2017-04-17 17:50:10 -04:00
Yen-Sheng Ho 38e5c8c9e6 %pdra: added an option for disabling incremental solving 2017-04-16 22:03:47 -07:00
Alan Mishchenko b1eaf714f2 Experiments with SAT sweeping. 2017-04-11 22:12:18 -07:00
Yen-Sheng Ho 2c443d20de merge 2017-04-10 16:21:13 -07:00
Yen-Sheng Ho 0f1a758c2f %pdra: bug fix 2017-04-09 17:59:34 -07:00
Yen-Sheng Ho 3c43851c36 %pdra: bug fix 2017-04-09 17:22:14 -07:00
Yen-Sheng Ho 3401ed364b %pdra: added top level callbacks 2017-04-09 14:38:37 -07:00
Alan Mishchenko fe3d334151 Experiments with hashing. 2017-04-08 18:37:32 -07:00
Alan Mishchenko dd51c29934 Experiments with don't-cares. 2017-04-08 14:35:29 -07:00
Yen-Sheng Ho 72c23923da merge 2017-04-06 14:18:50 -07:00
Yen-Sheng Ho 2761e5e35b small changes 2017-04-06 14:18:28 -07:00
Yen-Sheng Ho 131a51a4b5 %pdra: handled real CEXs; refactor 2017-04-06 14:15:26 -07:00
Alan Mishchenko 2373c5b15c Adding stand-alone cut computation to GIA. 2017-04-05 22:02:05 -07:00
Alan Mishchenko 304c63e860 Experiments with don't-cares. 2017-04-04 15:37:10 -07:00
Alan Mishchenko 44605f5af6 Experiments with don't-cares. 2017-04-04 03:17:24 -07:00
Alan Mishchenko f765e666ca Experiments with don't-cares. 2017-04-02 21:51:47 -07:00
Alan Mishchenko 3898ba5486 Experiments with don't-cares. 2017-03-31 21:24:19 -07:00
Alan Mishchenko ac59789e9b Experiments with don't-cares. 2017-03-31 21:07:19 -07:00
Yen-Sheng Ho 1531dd8ec5 %pdra: added an option -t for disabling trace reuse 2017-03-31 15:34:21 -07:00
Yen-Sheng Ho 04bd8631e0 merge 2017-03-31 07:42:06 -07:00
Yen-Sheng Ho 16ef095f9c %pdra: fixed bugs 2017-03-30 15:22:39 -07:00
Alan Mishchenko 96056c377c Experiments with multipliers. 2017-03-30 14:53:35 -07:00
Yen-Sheng Ho 1cb140bb11 %pdra: fixed bugs 2017-03-30 13:53:18 -07:00
Yen-Sheng Ho 4d47904831 %pdra: fixed bugs 2017-03-29 14:20:40 -07:00
Alan Mishchenko 7285f1051e Experiments with multipliers. 2017-03-28 23:28:04 -07:00
Yen-Sheng Ho bf4be3fc25 %pdra: improved performance 2017-03-28 15:20:53 -07:00
Alan Mishchenko fdfb888891 Experiments with don't-cares. 2017-03-28 14:29:56 -07:00
Yen-Sheng Ho 2fea987ec6 %pdra: added an option -s 2017-03-28 14:08:04 -07:00
Yen-Sheng Ho 7a423e4fbe %pdra: added a procedure to shrink abstraction 2017-03-27 17:09:23 -07:00
Yen-Sheng Ho 758270d663 %pdra: refactor 2017-03-27 15:18:35 -07:00
Yen-Sheng Ho e6098d20be %pdra: added a procedure to rebuild traces 2017-03-27 15:10:33 -07:00
Alan Mishchenko 2ccd0f9b85 Experiments with don't-cares. 2017-03-26 21:46:09 -07:00
Alan Mishchenko 23151498fa Experiments with don't-cares. 2017-03-26 20:35:31 -07:00
Alan Mishchenko 036be3a541 Experiments with don't-cares. 2017-03-26 20:32:46 -07:00
Alan Mishchenko d0ea4853ec Experiments with multipliers. 2017-03-26 14:38:04 -07:00
Alan Mishchenko a34d8cbb36 Experiments with don't-cares. 2017-03-23 19:19:29 -07:00
Alan Mishchenko 1ac9d2997c Experiments with don't-cares. 2017-03-22 13:04:24 -07:00
Alan Mishchenko d92bfbaddc Experiments with new network data-structure. 2017-03-20 23:45:03 -07:00
Alan Mishchenko 245532cad1 Merged in ysho/abc (pull request #69) 
Improvements to %pdra
 2017-03-20 05:01:40 +00:00
Alan Mishchenko 027bb83e81 Experiments with new network data-structure. 2017-03-19 21:59:41 -07:00
Alan Mishchenko 9510da0b30 Experiments with new network data-structure. 2017-03-19 21:54:25 -07:00
Alan Mishchenko 19ccaf21df Experiments with new network data-structure. 2017-03-19 21:51:03 -07:00
Yen-Sheng Ho 875411985c %pdra: working on bmc3 2017-03-19 14:21:19 -07:00
Yen-Sheng Ho 51fbf37cb4 %pdra: working on bmc3 2017-03-19 12:41:06 -07:00
Yen-Sheng Ho 3bddf93876 %pdra: working on bmc3 2017-03-19 12:07:45 -07:00
Yen-Sheng Ho 0d054904e0 %pdra: working on bmc3 2017-03-18 15:23:50 -07:00
Yen-Sheng Ho 7713e94a1a %pdra: isolated the procedure for checking comb. unsat 2017-03-18 14:23:09 -07:00
Alan Mishchenko 1e5d826c4c Code for structural unateness checking. 2017-03-18 13:38:37 -07:00
Alan Mishchenko 60aa7baa47 Synthesis for mesh of LUTs. 2017-03-17 16:22:10 -07:00
Alan Mishchenko 4e492ea0b7 Merged in ysho/abc (pull request #68) 
Improvements to %pdra
 2017-03-17 20:55:13 +00:00
Alan Mishchenko 9e668f1b10 Synthesis for mesh of LUTs. 2017-03-17 13:53:37 -07:00
Yen-Sheng Ho 06a8d50544 %pdra: cleanup, refactor 2017-03-17 13:04:03 -07:00
Yen-Sheng Ho 3974ff7518 merge 2017-03-17 12:21:28 -07:00
Yen-Sheng Ho 4d7cec5051 %pdra: disabled an experimental procedure 2017-03-17 12:18:39 -07:00
Alan Mishchenko d66ff2cf54 New word-level transformation. 2017-03-17 08:48:27 -07:00
Alan Mishchenko 34bcabcbf4 Small changes. 2017-03-16 18:31:15 -07:00
Yen-Sheng Ho ddd349cf96 %pdra: created a new manager; refactored 2017-03-16 16:14:45 -07:00
Yen-Sheng Ho b9971b2348 added another function for printing wlc 2017-03-16 13:33:14 -07:00
Yen-Sheng Ho 6bf50cbb86 %pdra: added a structural support profiling of PPIs 2017-03-16 12:50:27 -07:00
Alan Mishchenko 876c2c353a Integration of new SAT sweeper. 2017-03-11 20:54:49 -08:00
Yen-Sheng Ho 70511b001c %pdra: added an option -i for weaker proof-based refinement 2017-03-09 21:43:18 -08:00
Yen-Sheng Ho 566beb9c92 %pdra: added more stats 2017-03-09 17:33:00 -08:00
Yen-Sheng Ho eede1bc7f8 bug fix 2017-03-09 13:20:56 -08:00
Yen-Sheng Ho 3ae83d376a %pdra, %abs: added option -d for apple-to-apple comparison 2017-03-09 13:07:30 -08:00
Yen-Sheng Ho 6f8820fb95 %pdra: count the number of reused clauses 2017-03-09 11:07:58 -08:00
Mathias Soeken 74e445ad66 Exact synthesis. 2017-03-06 16:39:51 +01:00
Mathias Soeken 1cd5f76800 Fix exact command for multiple-output functions. 2017-03-06 16:32:07 +01:00
Mathias Soeken d971505402 Merged alanmi/abc into default 2017-03-04 20:22:53 +01:00
Alan Mishchenko 59348e227c Clone of the main SAT solver to eneable independent work. 2017-03-03 15:16:05 -08:00
Yen-Sheng Ho 154f4b642d merge 2017-03-03 13:46:32 -08:00
Yen-Sheng Ho 40d29e7813 only try scorr on small circuits 2017-03-03 12:29:15 -08:00
Heinz Riener 59f09c10d5 removed unnecessary declaration 2017-03-03 12:09:36 +01:00
Heinz Riener 5318619c64 added missing ABC_NAMESPACE_HEADER 2017-03-03 12:04:39 +01:00
Mathias Soeken f03871ab22 Merged alanmi/abc into default 2017-03-03 10:33:59 +01:00
Yen-Sheng Ho cb603c5ea1 added scorr to %pdra -u 2017-03-02 22:16:16 -08:00
Alan Mishchenko 2f69fa134e Moving global declarations into 'abcapi.h' and moving it into 'main' package. 2017-03-02 20:50:56 -08:00
Yen-Sheng Ho 7eac1f5766 added experimental codes 2017-03-02 17:31:30 -08:00
Alan Mishchenko 64035e52ab Macro to prevent writing history file. 2017-03-02 17:27:24 -08:00
Alan Mishchenko 96a399568d Adding experimental command. 2017-03-02 15:26:29 -08:00
Alan Mishchenko d850599020 Adding command 'glitch' for glitch simulation. 2017-03-02 14:26:04 -08:00
Yen-Sheng Ho 18b47dfbd5 %pdra: added an option -u for checking comb. unsat 2017-03-01 14:57:43 -08:00
Yen-Sheng Ho da0f4ef33b %pdra: now checks if cex is real before refinement 2017-03-01 12:12:42 -08:00
Alan Mishchenko b71d2ab2ba Fixed a few compilcation issues with Windows compiler. 2017-02-28 20:15:33 -08:00
Yen-Sheng Ho 007195ddd8 small tweaks 2017-02-28 19:25:11 -08:00
Yen-Sheng Ho 777c77785d merge 2017-02-28 19:21:31 -08:00
Yen-Sheng Ho 902a78eeb8 added an option -r to %pdra: proof-based refinement only 2017-02-28 18:05:58 -08:00
Yen-Sheng Ho d95d51c474 improved profiling in %pdra 2017-02-28 11:30:13 -08:00
Yen-Sheng Ho 43f34ddc02 added -L to %abs 2017-02-28 08:05:33 -08:00
Yen-Sheng Ho 46b6ac1539 improved %pdra -L 2017-02-27 20:44:19 -08:00
Yen-Sheng Ho 9195192f65 %pdra -L: now applies to all types 2017-02-27 14:31:59 -08:00
Yen-Sheng Ho bb3eacf480 small tweaks 2017-02-27 13:45:22 -08:00
Alan Mishchenko ed31679759 Enabling LUT pairing. 2017-02-27 12:18:24 -08:00
Yen-Sheng Ho ff745ca1a5 fixed a bug 2017-02-26 15:45:35 -08:00
Yen-Sheng Ho 86b3cb3da9 added an option -L to %pdra for limiting the number of muxes 2017-02-26 15:39:48 -08:00
Yen-Sheng Ho 27bdffd5a2 small tweaks 2017-02-26 14:38:38 -08:00
Yen-Sheng Ho cba376cfff improved %pdra -b 2017-02-25 22:26:51 -08:00
Yen-Sheng Ho a8f6e5c60a added an option -b to %pdra 2017-02-25 18:32:43 -08:00
Yen-Sheng Ho a7bc919b69 imported proof-based codes from ufar 2017-02-25 15:22:30 -08:00
Yen-Sheng Ho 7508a37a51 imported proof-based codes from ufar 2017-02-25 14:58:01 -08:00
Yen-Sheng Ho 14cf117968 imported proof-based codes from ufar 2017-02-25 09:37:59 -08:00
Yen-Sheng Ho 06797fb611 mege 2017-02-24 14:21:45 -08:00
Alan Mishchenko db36c65bce Small changes in the usage message for &gla. 2017-02-23 14:12:56 -08:00
Yen-Sheng Ho d5bbf9188c added %pdra -a: run with pdr -nct 2017-02-23 08:48:53 -08:00
Mathias Soeken 28e8e7f3e7 Merged alanmi/abc into default 2017-02-22 19:00:28 -08:00
Yen-Sheng Ho f01c63f712 working on %pdra -m 2017-02-22 17:57:19 -08:00
Yen-Sheng Ho 2f90e5e15d added an option -m for %pdra 2017-02-22 15:37:49 -08:00
Alan Mishchenko 53b1d46b8d Remapping flops in '%pdra. 2017-02-21 22:20:03 -08:00
Alan Mishchenko 0e9f8093c3 Merged in ysho/abc (pull request #59) 
added a new abstraction
 2017-02-22 04:31:10 +00:00
Yen-Sheng Ho fb2fbd70bd clean up 2017-02-21 20:10:11 -08:00
Yen-Sheng Ho 01e6beea8e clean up 2017-02-21 20:06:13 -08:00
Yen-Sheng Ho 9f43c84501 added options of checking and pushing to %pdra 2017-02-20 12:51:04 -08:00
Alan Mishchenko ac1eb60db9 Experiments with SAT sweeping. 2017-02-20 12:32:32 -08:00
Yen-Sheng Ho 19510bd38e added datastructure for %pdra options 2017-02-20 11:07:12 -08:00
Yen-Sheng Ho 222b3741a4 fixed time profiling in pdr 2017-02-20 10:13:18 -08:00
Yen-Sheng Ho 1a66a5823a working on pdr with wla 2017-02-19 16:09:59 -08:00
Yen-Sheng Ho 2d1792040a working on pdr with wla 2017-02-19 15:57:13 -08:00
Yen-Sheng Ho 2732cbc1ee working on pdr with wla 2017-02-19 12:31:28 -08:00
Yen-Sheng Ho 840f5d1ca8 working on pdr with wla 2017-02-19 10:22:15 -08:00
Yen-Sheng Ho 6cf289dadd working on pdr with wla 2017-02-19 09:55:58 -08:00
Yen-Sheng Ho 24fdcecb2d started %pdra 2017-02-19 09:20:44 -08:00
Alan Mishchenko 27caed8dc8 Experiments with SAT sweeping. 2017-02-18 20:20:50 -08:00
Alan Mishchenko 429f52ce15 Experiments with SAT sweeping. 2017-02-18 14:20:10 -08:00
Yen-Sheng Ho b93a805129 copied some functions from pdr 2017-02-18 12:43:03 -08:00
Yen-Sheng Ho 91a0a0fc3b copied pdr_mansolve 2017-02-18 10:28:16 -08:00
Yen-Sheng Ho 196b359183 started pdrIncr.c 2017-02-18 09:51:54 -08:00
Yen-Sheng Ho 1d3ff5338a added ipdr 2017-02-17 18:55:00 -08:00
Alan Mishchenko 632ca7ed11 Promising alternative of CEX minimization in 'pdr'. 2017-02-16 13:37:46 -08:00
Alan Mishchenko c7b68c5e3f Promising modification of the generalization procedure in 'pdr'. 2017-02-16 10:03:34 -08:00
Alan Mishchenko ab387953ab Word-level abstraction engine. 2017-02-15 17:16:19 -08:00
Alan Mishchenko 2a5fa67d36 Adding APIs to mark cones. Creating test-bench for incremental solving &satoko -i. 2017-02-11 17:28:37 -08:00
Alan Mishchenko 5d717256d3 Updates to the autotuner. 2017-02-10 18:14:06 -08:00
Alan Mishchenko f7a1fe88fb Merged in boschmitt/abc (pull request #51) 
Modifications to satoko.
 2017-02-11 01:41:19 +00:00
Alan Mishchenko 8bff9aa1cd Adding PDR with abstraction. 2017-02-10 17:36:20 -08:00
Bruno Schmitt d69735309d Merged alanmi/abc into default 2017-02-10 17:28:17 -08:00
Bruno Schmitt 342d2d9f5c New fixed point data type. 
Expose all options to command line.
Expose search statistics to users.
 2017-02-10 17:26:45 -08:00
Alan Mishchenko fce2b16a60 Re-introducing floating-point activity in the SAT solver. 2017-02-10 13:31:29 -08:00
Alan Mishchenko f2d096c9f0 Improving CEX minimization. 2017-02-10 13:20:20 -08:00
Alan Mishchenko d335ee096e Standardizing the use of new CNF generator. Adding CNF variable connectivity information. 2017-02-10 11:05:00 -08:00
Alan Mishchenko 7a2984bbe9 Word-level abstraction. 2017-02-09 16:38:08 -08:00
Alan Mishchenko 2fe17c1f4b Word-level abstraction. 2017-02-09 14:30:10 -08:00
Alan Mishchenko 32712ec9ab Making sure 'inv_out' can match flops by name. 2017-02-09 14:17:19 -08:00
Alan Mishchenko e20ef654d9 Word-level abstraction. 2017-02-09 13:31:07 -08:00
Alan Mishchenko 040b88a7c6 Editing output messages. 2017-02-08 19:12:57 -08:00
Alan Mishchenko 2a9902eec7 Accidental change. 2017-02-08 19:10:15 -08:00
Alan Mishchenko 778ea6bb8a Editing output messages. 2017-02-08 19:07:21 -08:00
Alan Mishchenko 1e62fb4a92 Compiler warning. 2017-02-08 18:59:07 -08:00
Alan Mishchenko 77e2b1ff53 Autotuner for 'satoko'. 2017-02-08 18:57:16 -08:00
Alan Mishchenko de4bf41c53 New command &satoko. 2017-02-08 14:10:08 -08:00
Bruno Schmitt 0fb4442a82 Small changes to support old compilers. 2017-02-06 19:50:57 -08:00
Bruno Schmitt cac3967b52 Adding a new SAT solver to ABC. (Satoko) 
The command is ‘satoko’
 2017-02-06 11:34:52 -08:00
Alan Mishchenko aed9a87282 Adding specialized flop ordering before generalization in 'pdr'. 2017-02-06 00:54:18 -08:00
Alan Mishchenko f34029dd09 Improvements in AIG visualization. 2017-02-05 12:28:34 -08:00
Alan Mishchenko 45bf0369a8 Adding structural flop priority heuristics in 'pdr'. 2017-02-03 19:51:53 -08:00
Alan Mishchenko 6d088bc440 Enabling new X-valued simulation in 'pdr'. 2017-02-03 17:02:36 -08:00
Alan Mishchenko e91abd6307 Improvements to inductive generalization in IC3/PDR by Zyad Hassan. 2017-02-02 16:03:40 -08:00
Alan Mishchenko a226496bf9 Adding API for generating a monitor of a set of internal signals in a sequential logic network. 2017-01-31 19:53:57 -08:00
Alan Mishchenko 452a19f70c Improvements to SMT-LIB parser (bug fixes). 2017-01-30 18:30:59 -08:00
Alan Mishchenko e21c7d72f3 Updates to arithmetic verification. 2017-01-30 08:39:26 -08:00
Alan Mishchenko 3020d57ea6 Commenting out debug code. 2017-01-29 13:39:35 -08:00
Alan Mishchenko e9566a1e3d Updates to arithmetic verification. 2017-01-29 13:37:29 -08:00
Alan Mishchenko f701a0c659 Commenting out &mfs report message. 2017-01-27 10:48:56 -08:00
Alan Mishchenko c2b805dc85 Adding visualization of word-level networks Wlc_Ntk_t. 2017-01-26 22:22:22 -08:00
Alan Mishchenko 64d7119ddc Adding visualization of word-level networks Wlc_Ntk_t. 2017-01-26 21:43:28 -08:00
Alan Mishchenko 7d82819d51 Adding visualization of word-level networks Wlc_Ntk_t. 2017-01-26 15:17:02 -08:00
Alan Mishchenko 3c8c807ac1 Improvements to SMT-LIB parser. 2017-01-26 11:56:17 -08:00
Alan Mishchenko 3119e1e30f Adding features for invariant minimization. 2017-01-25 13:56:16 -08:00
Alan Mishchenko cf1106aba8 Adding features for invariant minimization. 2017-01-24 22:28:28 -08:00
Alan Mishchenko 849f180764 Adding features for invariant minimization. 2017-01-24 20:44:25 -08:00
Alan Mishchenko 51f4dab475 Adding features for invariant minimization. 2017-01-24 20:02:19 -08:00
Alan Mishchenko cf539dcca4 Fix mismatch in output formatting. 2017-01-21 12:48:40 +08:00
Alan Mishchenko a28be94ac7 Small fixes and a change to &cec to allow two files names given as command-line arguments. 2017-01-21 11:59:01 +08:00
Alan Mishchenko 153b71c140 Updates to arithmetic verification. 2017-01-15 20:59:59 +07:00
Alan Mishchenko 1b86911c4f Updates to arithmetic verification. 2017-01-14 20:28:26 +07:00
Alan Mishchenko 79701f8b46 Updates to arithmetic verification. 2017-01-14 16:11:59 +07:00
Alan Mishchenko 6d606b51ab Updates to arithmetic verification. 2017-01-13 21:17:00 +07:00
Alan Mishchenko 1a39fb3946 Adding print-out of critical path for mapped AIGs to &show. 2017-01-13 17:32:58 +07:00
Alan Mishchenko d52dafa6c2 Updates to arithmetic verification. 2017-01-12 16:12:48 +07:00
Alan Mishchenko 55b6b4bdab Updates to arithmetic verification. 2017-01-11 16:08:23 +07:00
Alan Mishchenko fbdf28e4c9 Updated to arithmetic verification. 2017-01-09 19:50:05 +07:00
Alan Mishchenko 9514c327e3 Bug fix in delay-opt framework. 2017-01-09 11:04:48 +07:00
Alan Mishchenko feb57982a9 Change suggested by Udi Finkelstein. 2017-01-09 10:46:29 +07:00
Alan Mishchenko 3dd2325aa8 Adding an option to not add buffers to decouple COs driven by the same internal node. 2017-01-07 09:51:38 +07:00
Alan Mishchenko 460167ec74 Compiler warnings. 2017-01-07 08:57:08 +07:00
Alan Mishchenko 74c8d35f33 Updates to delay optimization project. 2017-01-02 16:29:10 +07:00
Alan Mishchenko 3f2899d6ea Compiler warnings. 2016-12-31 22:00:26 +07:00
Alan Mishchenko 01924ca118 Updates to delay optimization project. 2016-12-31 20:21:46 +07:00
Alan Mishchenko 54b4692d4b Updates to delay optimization project. 2016-12-29 21:26:02 +07:00
Alan Mishchenko b56a532682 Several changes in arithmetic circuit manipulation. 2016-12-22 17:27:32 +07:00
Alan Mishchenko cf5d4ad07f Converting some errors into warnings. 2016-12-21 15:34:02 +07:00
Bruno Schmitt 5351ab4b13 xSAT is an experimental SAT Solver based on Glucose v3(see Glucose copyrights below) and ABC C version of 
MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko. It’s development has reached
sufficient maturity to be committed in ABC, but still in a beta state.

TODO:
* Read compressed CNF files.
* Study the use of floating point for variables and clauses activity.
* Better documentation.
* Improve verbose messages.
* Expose parameters for tuning.
 2016-12-12 16:20:38 -02:00
Mathias Soeken 5af44731bf Merged alanmi/abc into default 2016-12-07 10:08:44 +01:00
Alan Mishchenko 3169bd96b7 Compiler warnings. 2016-12-05 17:48:21 -08:00
Alan Mishchenko 6a351c4dc0 Adding support for minimalistic representation of LUT mapping. 2016-12-05 17:45:15 -08:00
Alan Mishchenko 8ba6071a76 New SAT-based optimization package. 2016-12-04 21:59:10 -08:00
Alan Mishchenko 91aab10757 Analysis of arithmetic logic cones. 2016-12-04 13:05:51 -08:00
Alan Mishchenko b3514ee7e0 Commenting out bailout in 'print_cex' when CEX has latches initialized to 1. 2016-11-30 12:07:08 -08:00
Alan Mishchenko 329cee4981 Small changes in handling arithmetic logic. 2016-11-30 11:30:38 -08:00
Alan Mishchenko de71ef44cd New command to profile arithmetic logic cones. 2016-11-26 17:06:54 -08:00
Alan Mishchenko 6b55bf0205 New SAT-based optimization package. 2016-11-26 14:28:12 -08:00
Alan Mishchenko 64bdbe1a74 Adding switch '-c' to generate only stuck-at faults in 'faultclasses -g'. 2016-11-22 20:09:25 -08:00
Alan Mishchenko b483c97fdd Minor bug fixes. 2016-11-21 11:52:50 -08:00
Vinicius Callegaro 9f99f08d4c Merged alanmi/abc into default 2016-11-16 20:57:39 -02:00
Alan Mishchenko 71a52ae9e5 Renaming command 'detect' to be 'faultclasses'. 2016-11-10 09:38:07 -08:00
Alan Mishchenko 460a5700a5 Compiler warnings. 2016-11-09 21:19:52 -08:00
Alan Mishchenko c6afb9db63 Equivalent fault detection code. 2016-11-09 21:17:44 -08:00
Vinicius Callegaro faf8d6ecea Disjoint-support decomposition with cofactoring and boolean difference analysis 
from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis" presented in ICCD'15.
 2016-11-08 17:00:35 -02:00
Alan Mishchenko 6cd66183e4 Isolating CBA types into a separate header. 2016-11-08 06:13:47 -08:00
Alan Mishchenko 85abb6bde7 Isolating CBA types into a separate header. 2016-11-07 09:39:29 -08:00
Mathias Soeken f9b7e92904 Exact synthesis. 2016-11-02 19:27:12 +01:00
Mathias Soeken 16109b11f6 Exact synthesis. 2016-10-29 09:34:34 +02:00
Mathias Soeken bab90943dc Exact synthesis. 2016-10-26 17:54:00 +02:00
Mathias Soeken 0a87e72c6d Exact synthesis. 2016-10-26 13:36:29 +02:00
Mathias Soeken a25faed14c Merged alanmi/abc into default 2016-10-26 13:31:28 +02:00
Alan Mishchenko 76c4d22229 Parser for JSON format. 2016-10-25 17:17:37 -07:00
Mathias Soeken f47a4377e4 Exact synthesis. 2016-10-25 16:28:02 +02:00
Alan Mishchenko f5069d6675 Code for profiling arithmetic circuits. 2016-10-21 17:50:05 -07:00
Alan Mishchenko 40375f8b93 Updates to arithmetic verification. 2016-10-09 19:38:30 -07:00
Alan Mishchenko 50e324ce11 Adding switch &mfs -b to preserve white boxes during optimization. 2016-10-07 18:05:20 -07:00
Alan Mishchenko eb65c01888 Change Verilog reader to take a string rather than file name. 2016-10-06 22:04:11 -07:00
Alan Mishchenko c01f5fc4e0 Adding module name when reading SMT-LIB from stdin. 2016-10-02 11:14:34 -07:00
Alan Mishchenko 7f3842e186 Bug fix in SMT parser. 2016-10-02 11:11:10 -07:00
Alan Mishchenko 44550a67fa Bug fix in the SMT parser to address multi-argument operators and large constants. 2016-09-30 19:55:21 -07:00
Alan Mishchenko 50da7c290c Compiler warnings. 2016-09-30 14:40:07 -07:00
Mathias Soeken f5be157583 Merged alanmi/abc into default 2016-09-29 22:10:16 -07:00
Alan Mishchenko 9a35f82d5f Supporting 'define-fun' with an expression rather than a constant. 2016-09-29 18:00:52 -07:00
Alan Mishchenko 4f0f2e09f8 Adding flag 'pdr -e' to output only support variables in the invariant. 2016-09-28 16:27:39 -07:00
Mathias Soeken e601df9dea Some fixes in BMS. 2016-09-14 10:06:00 +02:00
Mathias Soeken bb8e1808e6 New search strategy in BMS. 2016-09-14 09:53:06 +02:00
Mathias Soeken 452303b77a Updates to BMS. 2016-09-10 14:23:43 +02:00
Mathias Soeken b44c519620 Fix in BMS. 2016-09-09 15:39:33 +02:00
Mathias Soeken 2f2ed1bce1 Fixes in BMS. 2016-09-09 12:40:55 +02:00
Mathias Soeken 5b2472d4b7 Missing case in BMS. 2016-09-09 12:08:52 +02:00
Mathias Soeken 6d7f2c4d54 Improvements to BMS. 2016-09-09 11:51:53 +02:00
Mathias Soeken b11406c566 Merged alanmi/abc into default 2016-09-09 11:49:43 +02:00
Alan Mishchenko ca93730781 Experimental code for polynomial construction. 2016-09-05 23:54:44 +03:00
Alan Mishchenko 198fe99416 Experimental code for polynomial construction. 2016-09-05 23:47:58 +03:00
Mathias Soeken a46af9de7b Improvements to BMS. 2016-08-29 22:40:30 +02:00
Mathias Soeken 7e3032c0dd Improvements to BMS. 2016-08-29 13:37:29 +02:00
Mathias Soeken 2d71abd581 Symmetric variables in BMS. 2016-08-28 13:44:59 +02:00
Mathias Soeken 610fcb2712 Improvements to BMS. 2016-08-26 09:45:52 +02:00
Mathias Soeken e5636522bf BMS fixes and start gates parameter. 2016-08-25 10:56:59 +02:00
Mathias Soeken 360e85fce2 Fix errors in BMS. 2016-08-24 17:08:06 +02:00
Mathias Soeken fcf3335041 Improvements to BMS. 2016-08-24 15:03:52 +02:00
Mathias Soeken ea3836ea5d Improvements to BMS. 2016-08-24 09:29:02 +02:00
Mathias Soeken db1daf7b8a Merged alanmi/abc into default 2016-08-24 09:28:21 +02:00
Mathias Soeken 30b3a7ab91 BMS: Store I/O, better implications to stop search. 2016-08-22 10:57:38 +02:00
Mathias Soeken 6e7fb2ea52 BMS: restart solver instead of re-allocating it. 2016-08-21 19:28:55 +02:00
Mathias Soeken 8ec44da3fb More logging in exact synthesis. 2016-08-21 18:13:57 +02:00
Mathias Soeken 9bb5a2dd0d Merged alanmi/abc into default 2016-08-21 18:12:05 +02:00
Mathias Soeken 9ac7b05e2a Fix compile errors when using namespace with clang. 2016-08-19 13:24:29 +02:00
Mathias Soeken 792e7e662d Merge with parent. 2016-08-18 10:32:17 +02:00
Alan Mishchenko 118eea8465 Changes to report quantum cost in Exorcism. 2016-08-17 21:26:16 +09:00
Mathias Soeken 433b9fe722 Missing code for CLI integration. 2016-08-16 18:55:20 +02:00
Mathias Soeken 85c751fbb8 Functions to compute T-count. 2016-08-16 18:46:45 +02:00
Mathias Soeken 2f149364eb Provide number of max cubes as parameter. 2016-08-16 18:33:53 +02:00
Mathias Soeken 0d1786d829 Don't output if not verbose. 2016-08-16 18:32:42 +02:00
Mathias Soeken 821029038d Used wrong truth table function in exact synthesis. 2016-08-16 08:20:28 +02:00
Mathias Soeken 077f8bdbb8 Merged alanmi/abc into default 2016-08-16 08:16:30 +02:00
Alan Mishchenko b83c6aaf97 Fix compiler problems by #including the header from FXCH package. 2016-08-16 11:20:43 +09:00
Mathias Soeken baca7e477f Fixes to exact synthesis. 2016-08-15 16:20:30 +02:00
Mathias Soeken 68f29c527e Merged alanmi/abc into default 2016-08-15 10:33:54 +02:00
Alan Mishchenko 9dc2f48858 Changes to report quantum cost in Exorcism. 2016-08-15 08:04:36 +08:00
Mathias Soeken 24af634508 Exact synthesis (revert one change). 2016-08-09 10:55:40 +02:00
Mathias Soeken ca8256fb4d Exact synthesis. 2016-08-09 10:53:58 +02:00
Mathias Soeken 80551de3c5 Small change in exact synthesis. 2016-08-08 18:52:11 +02:00
Mathias Soeken 7cc0094a0e Resource constraints in exact synthesis, arrival times in exact command. 2016-08-08 18:50:19 +02:00
Mathias Soeken 95d2ab9c17 Improvements in exact synthesis. 2016-08-08 12:59:21 +02:00
Mathias Soeken 5b9e520caa Bugfixes in exact synthesis. 2016-08-08 10:59:29 +02:00
Alan Mishchenko 2ded05127a Merged in petkovska/abc-pullreq/hier-npn_fast-exact (pull request #29) 
Exact hierarchical NPN classification
 2016-08-06 00:20:47 -07:00
Alan Mishchenko f03512bad1 Unsuccessful attempt to improve quality of factoring by limiting distance-1 merge during preprocessing. 2016-08-06 00:17:18 -07:00
Alan Mishchenko 9f02d23832 Fix some warnings. 2016-08-05 20:47:53 -07:00
Alan Mishchenko 92023a2925 Fix some warnings. 2016-08-05 20:45:56 -07:00
Alan Mishchenko c42aeb81a4 Handling constant and buffer cut in exact synthesis. 2016-08-05 20:43:45 -07:00
Alan Mishchenko 640100954a Updates to arithmetic verification. 2016-08-05 20:34:44 -07:00
Mathias Soeken 46a1c81603 Read and write to exact store. 2016-08-04 18:51:35 +02:00
Mathias Soeken 11ec43181c Exact synthesis minimization. 2016-08-04 14:22:31 +02:00
Mathias Soeken 718266f64a Update from parent. 2016-08-03 15:44:46 +02:00
Mathias Soeken 333bd87353 Free memory. 2016-08-03 15:23:34 +02:00
Alan Mishchenko af20a8177b Bug in 'dump_equiv -n'. 2016-08-02 12:20:19 -07:00
Mathias Soeken 33c6d01291 Tests and bug fixes for exact store manager. 2016-08-02 13:24:21 +02:00
Mathias Soeken 1f47fb7151 Dynamic number of variables in exact store manager. 2016-08-02 11:25:16 +02:00
Mathias Soeken 8246af894d Fixes in DelayCost and BuildNode. 2016-08-01 08:37:14 +02:00
Mathias Soeken a7b244c5a9 Merged alanmi/abc into default 2016-08-01 08:29:37 +02:00
Alan Mishchenko fd8eb8c855 Adding one argument to the delay-estimation API used for exact synthesis. 2016-07-31 13:31:57 -07:00
Mathias Soeken a4f8e601b9 Create and cleanup store, revert arrival times. 2016-07-31 13:08:14 +02:00
Mathias Soeken fdc9b180f8 Create network from solution in store. 2016-07-31 12:47:09 +02:00
Mathias Soeken 19e78a35d4 Store for exact results. 2016-07-31 12:24:02 +02:00
Mathias Soeken a6352369a5 Depth optimal synthesis. 2016-07-30 15:21:57 +02:00
Mathias Soeken 59077dab9f Implementation of Abc_ExactDelayCost. 2016-07-30 15:01:59 +02:00
Mathias Soeken 3641a3f18b Extract delay information into solution. 2016-07-30 14:40:12 +02:00
Mathias Soeken 90a6c38329 Check whether exact network can be found. 2016-07-30 14:39:11 +02:00
Mathias Soeken 6d0214edc9 Extract solution into intermediate format. 2016-07-30 13:34:39 +02:00
Alan Mishchenko 0b01f5ec27 Infrastructure for using the results of exact SAT-based synthesis during mapping. 2016-07-29 16:46:28 -07:00
Alan Mishchenko cf91699e05 Infrastructure for using the results of exact SAT-based synthesis during mapping. 2016-07-29 16:34:47 -07:00
Alan Mishchenko 71a051f8cd Compiler warnings. 2016-07-29 16:09:34 -07:00
Alan Mishchenko fb33d69db8 Infrastructure for using the results of exact SAT-based synthesis during mapping. 2016-07-29 16:03:42 -07:00
Alan Mishchenko 02d56ea04c Merged in boschmitt/abc (pull request #31) 
Make FX able to handle SCC
 2016-07-28 11:48:34 -07:00
Mathias Soeken 80fdd58c28 Several updates to exact synthesis. 2016-07-28 20:37:09 +02:00
Bruno Schmitt daadd43b64 Merged alanmi/abc into default 2016-07-27 23:32:15 -03:00
Bruno Schmitt dcd37b6a25 Make FX able to handle SCC and remove its SOP preprocessing. 
Some other small changes.
 2016-07-27 23:30:46 -03:00
Alan Mishchenko 9895f30d95 Extending command 'dump_equv' to match inputs by name. 2016-07-27 18:09:52 -07:00
Alan Mishchenko a6db8bc157 Extending command 'dump_equv' to match inputs by name. 2016-07-27 18:07:51 -07:00
Bruno Schmitt 5604657bdb Make fx able to handle degenerate divisors: 
- Constant-1 (a + !a)
	- Divisors "a + !ab" and "a!b + b" are equal to "a + b"
Change the way divisors are printed.
Removal of dead code from fx.
 2016-07-26 23:53:34 -03:00
Alan Mishchenko 42309cacaa Extending command 'exact' to handle delay constraints. 2016-07-23 13:13:07 -07:00
Alan Mishchenko 4c6444e34a Bug fix in 'dump_equiv'. 2016-07-22 13:36:22 -07:00
Alan Mishchenko 3c2c19ce51 Adding new command 'dump_equiv'. 2016-07-21 16:47:30 -07:00
Alan Mishchenko bfe7333f41 Adding new command 'dump_equiv'. 2016-07-21 16:40:56 -07:00
Alan Mishchenko 2ba46d52f0 Extension in the detection code. 2016-07-19 20:44:02 -07:00
Alan Mishchenko 2f86667326 Adding output range support to %blast. 2016-07-18 08:34:05 -07:00
Alan Mishchenko 32d1516c64 Adding command 'exact' developed by Mathias Soeken to implement Knuth's exact synthesis algorithm. 2016-07-16 07:51:58 -07:00
Alan Mishchenko abdf39711f Several corner-case bugs in %read, &cec, and st. 2016-07-16 07:28:20 -07:00
Alan Mishchenko 3f8b5cd890 Small fixes and improvements in reporting node counts. 2016-07-15 19:11:17 -07:00
Alan Mishchenko 3b76bc2792 Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift). 2016-07-12 13:34:06 -07:00
Alan Mishchenko 4ffc14fd56 Small change to make &if not abort the scripts. 2016-07-04 23:54:07 -07:00
Alan Mishchenko 3ad4be259e Bit-blasting Booth multipliers. 2016-07-04 20:41:50 -07:00
Alan Mishchenko 84a277b491 Bug fix in blasting shifters with large bit-width. 2016-06-29 15:37:37 -07:00
Alan Mishchenko d02f9dd4df Bug fix in blasting shifters with large bit-width. 2016-06-29 15:36:31 -07:00
Alan Mishchenko 7dcba3e27b Experiments with edge-based mapping. 2016-06-29 15:29:24 -07:00
Alan Mishchenko 688f0269db Bug fix in blasting shifters with large bit-width. 2016-06-28 09:53:09 -07:00
Ana Petkovska 8e5af90c41 Return the class representative of each function. 2016-06-18 18:51:38 +02:00
Ana Petkovska 6842b8cdbc Group based exact NPN classification. 2016-06-18 18:42:57 +02:00
Alan Mishchenko a309569390 New multi-output PLA reader and preprocessor (read_plamo) (updated dist-1 merge). 2016-06-17 22:30:54 -07:00
Alan Mishchenko c912875261 New command 'phase_map'. 2016-06-17 20:21:39 -07:00
Alan Mishchenko 3c3a770a17 New multi-output PLA reader and preprocessor (read_plamo) (added dist-1 merge). 2016-06-16 21:09:39 -07:00
Alan Mishchenko e06c04a3ef Change to BENCH reader to read DFF with four inputs. 2016-06-16 16:48:45 -07:00
Alan Mishchenko 0923d543ad Adding a switch 'retime -o' to use old flop naming conventions. 2016-06-16 16:13:13 -07:00
Alan Mishchenko ada21a655f New multi-output PLA reader and preprocessor (read_plamo). 2016-06-16 15:22:03 -07:00
Alan Mishchenko e1b51d1863 Experiments with edge-based mapping. 2016-06-15 18:47:10 -07:00
Alan Mishchenko db43d6fbd8 Adding switch -P <num> to command 'cover'. 2016-06-14 20:43:50 -07:00
Alan Mishchenko 0a1b6f8fcc Detecting properties of internal nodes. 2016-06-14 15:37:59 -07:00
Alan Mishchenko a18da5c878 Detecting properties of internal nodes. 2016-06-12 19:07:46 -07:00
Alan Mishchenko 699dd39035 Support bit-blasting of shifts with more than 32 bits (fix). 2016-06-08 22:25:12 -05:00
Alan Mishchenko cad3d8d419 Support bit-blasting of shifts with more than 32 bits. 2016-06-07 15:20:38 -07:00
Alan Mishchenko 820a48b2cb Changes to Wlc to accommodate signed signals in SMT-LIB. 2016-06-07 15:05:21 -07:00
Alan Mishchenko 4efbd7b3ca Detecting properties of internal nodes. 2016-06-07 14:32:38 -07:00
Alan Mishchenko 31b2e8bebd Switch 'fx -x' to use only canonical divisors in 'fx'. 2016-06-06 19:31:56 -07:00
Alan Mishchenko 00242f2fb2 New profiling features for word-level optimizations. 2016-06-04 17:31:15 -07:00
Alan Mishchenko 93c785e802 Small changes for today's experiments. 2016-06-03 13:22:24 -07:00
Bruno Schmitt fe6a647f37 Merged alanmi/abc into default 2016-06-02 20:30:04 -03:00
Bruno Schmitt b6ab087952 Removing the memory saving mode, it is no longer necessary. 2016-06-02 17:26:12 -03:00
Alan Mishchenko e1b32ee756 Silencing several messages. 2016-06-01 11:57:29 -07:00
Alan Mishchenko 1d26d58a17 Adding switch 'pdr -o' to control using property output in induction. 2016-05-25 13:47:38 -07:00
Alan Mishchenko 58c81ec097 Improving SMT-LIB parser. 2016-05-23 11:15:37 -07:00
Alan Mishchenko c688d1b158 Improving SMT-LIB parser. 2016-05-23 10:42:53 -07:00
Alan Mishchenko 0f29f0aec9 Improving SMT-LIB parser. 2016-05-21 20:08:05 -07:00
Alan Mishchenko 34c5ac88d4 Improving SMT-LIB parser. 2016-05-20 20:38:43 -07:00
Alan Mishchenko 7b570b6241 Enabling AIGs without structural hashing (&get -c to import logic network). 2016-05-20 18:01:01 -07:00
Alan Mishchenko 3b62ee4575 Enabling AIGs without structural hashing. 2016-05-20 16:23:48 -07:00
Alan Mishchenko 27c44fd644 Switch &miter -y to convert a two-word miter into a dual-output miter. 2016-05-20 14:03:07 -07:00
Alan Mishchenko 555ed0b158 Enabling AIGs without structural hashing. 2016-05-20 13:50:19 -07:00
Alan Mishchenko 2ded89cca5 Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver. 2016-05-19 22:33:40 -07:00
Alan Mishchenko 2d0a8fb4cb Improving SMT-LIB parser. 2016-05-19 22:07:52 -07:00
Alan Mishchenko d7912acfca Bug fix in &demiter. 2016-05-16 17:34:25 -07:00
Alan Mishchenko 8a56721494 Experiments with generating sat assignments. 2016-05-15 16:18:23 -07:00
Alan Mishchenko be769ca3e8 Experiments with generating sat assignments. 2016-05-15 14:25:55 -07:00
Alan Mishchenko 0533fc7de9 Experiments with generating sat assignments. 2016-05-15 14:24:38 -07:00
Alan Mishchenko 4ffbd0b2df Adding switch -r to &dch to prevent combo-loops. 2016-05-13 13:40:08 -07:00
Alan Mishchenko 5b6e5b8178 New command 'expand' to expand SOPs against the offset. 2016-05-12 22:41:20 -07:00
Alan Mishchenko ea7d10d45d Adding 'read_pla -d' to read dc-set along with on-set (useful to derive offset). 2016-05-12 13:59:30 -07:00
Alan Mishchenko c5befad518 Cosmetic changes after incorporating new code of 'fxch'. 2016-05-11 20:03:13 -07:00
Alan Mishchenko c30819cb05 Cosmetic changes after incorporating new code of 'fxch'. 2016-05-11 19:59:56 -07:00
Bruno Schmitt 3cf495c831 Add a new module which implements the fast extract with cube hashing (fxch) algorithm. 
Removes old partial implementation of this algorithm from the "pla" module.
 2016-05-11 19:41:31 -03:00
Alan Mishchenko 6e8efec57d Experiments with CEC for arithmetic circuits. 2016-05-11 11:07:34 -07:00
Alan Mishchenko 652b279234 Experiments with CEC for arithmetic circuits. 2016-05-08 19:01:46 -07:00
Alan Mishchenko 236d412255 Experiments with CEC for arithmetic circuits. 2016-05-07 19:47:02 -07:00
Alan Mishchenko 40d90ae69c Small changes. 2016-05-04 13:46:07 -07:00
Alan Mishchenko 21896ba6bc Update to &show to show AIGs with XORs and MUXes (derived by &st -m). 2016-05-04 07:22:13 -07:00
Alan Mishchenko 28cbb280b7 Update to &show to show AIGs with XORs and MUXes (derived by &st -m). 2016-05-04 07:05:43 -07:00
Alan Mishchenko 11f1a249ae Updating GIG parser. 2016-05-01 17:43:50 -07:00
Alan Mishchenko a093091004 Fanout restriction in &edge. 2016-04-30 17:47:23 -07:00
Alan Mishchenko 59f3389c9b Experiments with arithmetic circuits. 2016-04-28 20:54:38 -07:00
Alan Mishchenko 53e8647719 Adding option to rehash AIG after mapping. 2016-04-27 18:33:23 -07:00
Alan Mishchenko e8f961671c Extending &satlut to work for 6-LUTs. 2016-04-27 18:12:41 -07:00
Alan Mishchenko 62f13100d0 Adding missing code to 'dress'. 2016-04-27 17:33:36 -07:00
Alan Mishchenko 6f370462d1 Bug fix in bit-blasting of remainder. 2016-04-26 20:24:46 -07:00
Alan Mishchenko e37ec2aac5 Improved algo for edge computation. 2016-04-24 20:49:05 +03:00
Alan Mishchenko f91f23bed0 Adding new switch 'bdd -s' to translate SOP directly into BDD. 2016-04-24 00:13:07 +03:00
Alan Mishchenko 67bfb4ba09 Improved algo for edge computation. 2016-04-23 15:13:22 +03:00
Alan Mishchenko 1b550cb87b Improved algo for edge computation. 2016-04-22 08:36:05 +03:00
Alan Mishchenko 813b0e5851 Experimental algorithm for edge optimization. 2016-04-13 15:54:14 -07:00
Alan Mishchenko b9e403b46e Bug fix: change in the ordering of the reset flop (should be last, not first). 2016-04-13 09:14:54 -07:00
Alan Mishchenko 847ac96f6e Updates to Exorcism package 2016-04-11 22:55:06 -07:00
Alan Mishchenko 9522aeea19 Updates to Exorcism package 2016-04-11 22:29:37 -07:00
Alan Mishchenko a02be725e9 Updates to Exorcism package 2016-04-11 21:48:54 -07:00
Alan Mishchenko 2d6a6f6654 Added Exorcism package, reading ESOP (read_pla -x file.esop) and deriving AIG (cubes -x; st). 2016-04-11 21:42:00 -07:00
Alan Mishchenko 2d1d315ece Supporting edge information during mapping. 2016-04-11 18:41:18 -07:00
Alan Mishchenko d0a0cf6395 Command &esop to convert AIG into ESOP. 2016-04-09 17:00:46 -07:00
Alan Mishchenko 3b694a7089 Adding AIG rehashing after LUT mapping in Gia. 2016-04-07 20:03:31 -07:00
Alan Mishchenko 26ec3868f6 Adding AIG rehashing after LUT mapping in Gia. 2016-04-07 19:16:51 -07:00
Alan Mishchenko 887f3c21cc Supporting edges in delay-optimization in &satlut. 2016-04-07 17:15:24 -07:00
Alan Mishchenko f05986f7b3 Supporting edges in delay-optimization in &satlut. 2016-04-07 15:54:50 -07:00
Alan Mishchenko 95ab749087 Supporting edges in delay-optimization in &satlut. 2016-04-07 13:20:41 -07:00
Alan Mishchenko b31b6fec77 Supporting edge information during mapping. 2016-04-06 15:43:03 -07:00
Alan Mishchenko ee17cbbf4b Supporting negative and reverse ranges of word-level variables in Wlc. 2016-04-04 18:09:41 -07:00
Alan Mishchenko ac7a799076 Improvements to delay-optimization in &satlut. 2016-04-04 14:27:14 -07:00
Alan Mishchenko 720082753f Improvements to delay-optimization in &satlut. 2016-04-04 12:51:05 -07:00
Alan Mishchenko 4a954c1b23 Improvements to delay-optimization in &satlut. 2016-04-04 08:43:22 -07:00
Alan Mishchenko e0ad9de7ea Improvements to delay-optimization in &satlut. 2016-04-03 16:44:13 -07:00
Alan Mishchenko d53161a7e1 Enabling native Gia visualization in &show. 2016-04-03 15:42:08 -07:00
Alan Mishchenko 9074d19d69 Allowing Cba manager to be derived from another Cba manager. 2016-04-02 16:04:15 -07:00
Alan Mishchenko 7724dfcca2 Windowing for technology mapping. 2016-03-30 21:51:50 -07:00
Alan Mishchenko e026f05ae3 Bug fix in truth table reading for funcs with less than 6 vars. 2016-03-28 10:18:17 -07:00
Alan Mishchenko 72ffddb0ad Sorting multiplier inputs based on the number of constant bits. 2016-03-24 17:45:51 -07:00
Alan Mishchenko a4d6e2f8c9 Typo in operator in Wlc_Ntk_t. 2016-03-18 20:47:21 -07:00
Alan Mishchenko 65ee47c515 Supporting bit-wise XNOR operator in Wlc_Ntk_t. 2016-03-18 13:58:22 +08:00
Alan Mishchenko b2ad140adb Supporting complemented reduction operators. 2016-03-11 15:12:52 +09:00
Alan Mishchenko 74328f52da Supporting complemented reduction operators. 2016-03-10 23:03:53 +09:00
Alan Mishchenko 847d661bee Change error to warning in 'scorr'. 2016-03-09 09:33:10 +09:00
Alan Mishchenko 12fac91fba Supporting ~^ as equality operator in Wlc. 2016-03-04 09:17:39 +09:00
Alan Mishchenko cf702af6f1 New hierarchical TT NPN matching. 2016-02-26 18:20:57 +08:00
Alan Mishchenko c8962e94e2 Improving bit-blasting of a multiplier and squarer. 2016-02-13 18:51:42 -08:00
Alan Mishchenko 390a145f0a Adding support for a different bit-blasting of a multiplier and squarer. 2016-02-13 15:15:01 -08:00
Alan Mishchenko e0616441b3 Adding support for a different bit-blasting of a multiplier and squarer. 2016-02-12 09:46:49 -08:00
Alan Mishchenko 66796c3808 Experiments with SAT-based mapping. 2016-02-08 16:29:36 -08:00
Alan Mishchenko 0224039132 Added recursive bit-blasting of a carry-lookahead adder. 2016-02-06 12:08:23 -08:00
Alan Mishchenko be35a13a4c Preserving internal signal names when 'strash' is not used. 2016-02-03 13:56:27 -08:00
Alan Mishchenko 8bcf8fd3c9 Supporting X-valued constants in Wlc_Ntk_t. 2016-02-02 16:40:29 -08:00
Alan Mishchenko 094c68f921 Supporting X-valued constants in Wlc_Ntk_t. 2016-02-02 16:20:19 -08:00
Alan Mishchenko c81b6cb515 Supporting X-valued constants in Wlc_Ntk_t. 2016-02-02 15:43:19 -08:00
Alan Mishchenko 02725c9eca An add-on to write Verilog for circuits mapped into simple gates. 2016-02-01 15:56:53 -08:00
Alan Mishchenko 9ef447658e Bug fix in 'aig', for the case of non-min-base SOPs. 2016-01-20 15:01:53 -08:00
Alan Mishchenko df34a26216 Generating sorting network as a PLA file. 2016-01-20 15:01:27 -08:00
Alan Mishchenko f5ee46eb3c New command to dump LUT network. 2016-01-16 17:35:46 -08:00
Alan Mishchenko c4446189a9 Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network. 2016-01-14 20:42:22 -08:00
Alan Mishchenko 87f6828d50 Adding support for delay/area tradeoff. 2016-01-13 12:13:54 -08:00
Alan Mishchenko 8dd31fb4a9 Integrating new CNF generation into &bmc. 2016-01-12 22:07:01 -08:00
Alan Mishchenko de695c9d4c Better print-out of SOPs. Changing default of 'fx'. Updating 'satclp' to fine prine SOPs. 2016-01-12 11:55:50 -08:00
Alan Mishchenko 7984628d7f Experiments with SAT-based mapping. 2016-01-10 21:06:04 -08:00
Alan Mishchenko d6178631be Adding support of candinality clause to the SAT solver. 2016-01-10 10:19:26 -08:00