Commit Graph

4237 Commits

Author SHA1 Message Date
Staf Verhaegen e4875df4e5 Value of properties can be expression.
Example found in the 2007.03 Liberty Reference Manual that was also found
in the wild:

    input_voltage(CMOS) {
        vil : 0.3 * VDD ;
        vih : 0.7 * VDD ;
        vimin : -0.5 ;
        vimax : VDD + 0.5 ;
    }

Current implementation just parses the expression but no interpretation is done.
2018-01-03 21:54:38 +00:00
Alan Mishchenko f3dcf87cea New exact synthesis command 'allexact'. 2017-12-30 16:13:52 -08:00
Alan Mishchenko 75d334a0df New exact synthesis command 'allexact'. 2017-12-28 23:05:36 -08:00
Alan Mishchenko 7d7ce3ecd0 New exact synthesis command 'allexact'. 2017-12-28 23:04:24 -08:00
Alan Mishchenko c3dccf3020 Corner-case bug fixed in CNF generation. 2017-12-28 13:32:02 -08:00
Alan Mishchenko feebac4156 Corner-case bug fixed in CNF generation. 2017-12-28 13:26:08 -08:00
Alan Mishchenko 680af1891b Bug fix in 'write_aiger_cex'. 2017-12-20 15:41:39 -08:00
Alan Mishchenko c7b65a15d3 Adding parameter structure to 'twoexact' and 'lutexact'. 2017-12-06 15:09:11 -08:00
Alan Mishchenko 93b96fc35c An improvement to 'twoexact' and 'lutexact'. 2017-12-06 14:34:03 -08:00
Alan Mishchenko c6b962efc8 An improvement to 'twoexact' and 'lutexact'. 2017-12-06 13:51:10 -08:00
Alan Mishchenko e37bbba72d An improvement to 'twoexact' and 'lutexact'. 2017-12-06 13:00:08 -08:00
Alan Mishchenko 9e515ae363 An improvement to 'twoexact' and 'lutexact'. 2017-12-06 12:31:24 -08:00
Alan Mishchenko 67181d0446 An improvement to 'twoexact' and 'lutexact'. 2017-12-06 11:18:43 -08:00
Alan Mishchenko c4322a0afd Switch -a to use only AND-gates in 'twoexact' and 'lutexact'. 2017-12-06 10:31:21 -08:00
Alan Mishchenko b258db83b8 An improvement to 'twoexact' and 'lutexact'. 2017-12-06 09:53:25 -08:00
Alan Mishchenko 3f35ac8180 New command 'lutexact'. 2017-12-05 18:22:27 -08:00
Alan Mishchenko e5d8335268 Experiments with AIG-based simulation. 2017-12-05 09:49:02 -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
Alan Mishchenko c681506b48 Improvements to AIG-based quantification. 2017-11-26 14:41:05 -08:00
Baruch Sterin 7bcfe64369 C++ comaptibility: add namespace support to Glucose 2017-11-23 23:32:44 -08:00
Baruch Sterin d438d9c1b6 C++ compatibility: fix incompatible parameter list 2017-11-23 23:32:43 -08:00
Baruch Sterin 77ca1b7470 C++ compatibility: fix bad pointer comparison 2017-11-23 23:32:42 -08:00
Baruch Sterin d37cc72417 C++ compatibility: cast returned void* 2017-11-23 23:32:41 -08:00
Alan Mishchenko ecccfe0ed5 Experimental CEX minimization code. 2017-11-23 21:06:20 -08:00
Alan Mishchenko 203629fd0f Extracting CSAT interface and several cleanups. 2017-11-13 21:49:52 -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 71d9a16714 Improvements to quantification. 2017-11-13 14:56:40 -08:00
Alan Mishchenko 6bbbbe20af Compiler warnings. 2017-11-06 22:56:28 -08:00
Alan Mishchenko 5fd6dc0fca Profiling quantification and other changes. 2017-11-06 22:08:54 -08:00
Alan Mishchenko 716969190a Profiling quantification and other changes. 2017-11-06 16:43:32 -08:00
Alan Mishchenko 94a575a5b3 Commenting out problematic assertion in resub. 2017-11-04 20:24:01 -07:00
Alan Mishchenko a55cddeda6 Bug fix in old lcorr with constraints. 2017-11-04 20:23:22 -07:00
Alan Mishchenko f61b5d8c12 Supporting XOR in EQN parser. 2017-11-03 19:05:40 -07:00
Alan Mishchenko e21052dfdd Improvements to quantification. 2017-10-29 12:24:07 -07:00
Bruno Schmitt 50e17ae0f4 Small fix. Garanteeing pPars is not NULL before checking pPars->fSlacks 2017-10-24 23:03:32 +02: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
Baruch Sterin 5ab3f0fa6b Patch by Larry Doolittle to allow out-of-source builds of ABC.
Usage:

Starting from an empty directory:

(1) set AS to point to the location of ABC

(2) reconstruct the directory structure of ABC in the new directory:

    mkdir -p `cd $AS && find src -type d`

(3) Build ABC:

    make -f $AS/Makefile VPATH=$AS ABCSRC=$AS
2017-10-20 14:41:30 -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 298ec14efa Integrating Glucose into &qbf. 2017-10-17 14:09:41 +09:00
Alan Mishchenko c1b4b79e99 Integrating Glucose into &qbf. 2017-10-17 13:53:48 +09:00
Alan Mishchenko 1e1d41f3b8 Fix typo on the message reporting max output load. 2017-10-11 18:14:03 +07: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 fbdf438d26 Experiments with SAT-based quantification. 2017-10-04 20:02:05 +03:00