Alan Mishchenko
fd390aae9d
Extending MiniLUT to return attributes.
2018-02-11 17:14:07 -08:00
Alan Mishchenko
f716948c27
Experiments with LUT mapping.
2018-02-10 15:45:54 -08:00
Alan Mishchenko
c6bce9c20e
Fixing input swapping issue in MUXes derived from NDR.
2018-02-07 09:02:28 -08:00
Alan Mishchenko
f8d9fc3a9d
Improvements to NDR to represent hierarchical designs.
2018-02-05 00:41:05 -08:00
Alan Mishchenko
28602ccf2c
Improvements to NDR to represent hierarchical designs.
2018-02-05 00:39:10 -08:00
Alan Mishchenko
3202c2581e
Improvements to NDR to represent hierarchical designs.
2018-02-05 00:37:39 -08:00
Alan Mishchenko
00fb1d706b
Suggested fix to compile on FreeBSD.
2018-02-04 21:09:33 -08:00
Alan Mishchenko
30a06d002a
Adding support of reading and writing designs using a new internal format (bug fix).
2018-01-29 17:01:01 -08:00
Alan Mishchenko
99ddb64095
Adding support of reading and writing designs using a new internal format.
2018-01-28 18:53:20 -08:00
Alan Mishchenko
c8008383cf
Experiments with circuit-based SAT.
2018-01-27 20:29:46 -08:00
Alan Mishchenko
20603c7585
Experiments with circuit-based SAT.
2018-01-27 15:25:31 -08:00
Alan Mishchenko
f826956b07
Experiments with circuit-based SAT.
2018-01-27 14:33:49 -08:00
Alan Mishchenko
99c4dda767
Experiments with circuit-based SAT.
2018-01-27 14:05:00 -08:00
Alan Mishchenko
5158acb113
Experiments with circuit-based SAT.
2018-01-27 13:05:37 -08:00
Alan Mishchenko
e4cd0d60f1
Experiments with SAT-based simulation.
2018-01-25 00:09:27 -08:00
Alan Mishchenko
066e8d1b17
Experiments with SAT-based simulation.
2018-01-23 19:45:17 -08:00
Alan Mishchenko
67e820a5eb
Updates to exact synthesis commands.
2018-01-22 14:28:49 -08:00
Alan Mishchenko
6274498e01
Updates to exact synthesis commands.
2018-01-19 14:03:24 -08:00
Alan Mishchenko
c2b6e03c61
Backing up node's truth-table to make sure it is not destroyed while deriving AIG.
2018-01-19 12:22:48 -08:00
Alan Mishchenko
0ec5d2f7bc
Fixed crash in &nf when there is no buffer gate.
2018-01-12 22:28:30 -08:00
Alan Mishchenko
29895ca2f8
Merged in Fatsie/abc/liberty_value_expression (pull request #87 )
...
Allow expression in value in liberty file
2018-01-05 06:47:44 +00:00
Alan Mishchenko
7d781c37e8
New command 'testexact'.
2018-01-04 22:35:11 -08:00
Alan Mishchenko
834e248019
New command 'testexact'.
2018-01-04 22:33:29 -08:00
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
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
Alan Mishchenko
0a3af509bc
Experiments with SAT-based quantification.
2017-10-04 19:10:00 +03:00
Alan Mishchenko
396215532c
Updates and bug fixes.
2017-10-04 12:37:38 +03:00
Alan Mishchenko
343f77a395
Valgrind-ispired fix in CUDD by Kai-hui Chang.
2017-10-03 19:14:27 +03:00
Alan Mishchenko
21aa0ee0e8
Addressing recently reported Bitbucket Issue #72 and #73 .
2017-10-03 16:20:10 +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
ce8dbc4ac6
Exact synthesis of majority gates.
2017-10-01 18:40:30 +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
5585ce8aa6
Enabling Glucose in SAT sweeping: &fraig -g.
2017-09-18 09:37:20 -07:00
Alan Mishchenko
36858c5365
Enabling Glucose in SAT sweeping: &fraig -g.
2017-09-18 09:36:08 -07:00
Alan Mishchenko
12d21480de
Changes to Glucose to enable resetting the solver.
2017-09-18 08:43:55 -07:00
Alan Mishchenko
3a1032c151
Maintenance and updates.
2017-09-18 08:27:05 -07:00
Alan Mishchenko
7e7ba1562e
Compiler warning.
2017-09-16 14:30:02 -07:00
Alan Mishchenko
e7def3d4a2
Enabling variable elim in &bmcs -g.
2017-09-16 14:28:32 -07:00
Alan Mishchenko
b5d42e8bf3
Adding support for Dimacs input to &satoko.
2017-09-16 13:13:30 -07:00
Alan Mishchenko
6d2efdf28f
Improvements in Glucose integration.
2017-09-16 12:48:23 -07:00
Alan Mishchenko
f5cb9d6448
Bug fix in Glucose integration.
2017-09-16 12:37:27 -07:00
Baruch Sterin
adce11979f
bridge relates: (1) fix netlist reader to read the latest version written by ZZ, (2) replace printf() with Abc_Print() in pdr so that it will not interfer with bridge messages
2017-09-15 23:28:57 -07:00
Alan Mishchenko
2da820455e
Undoing updates to &bmcs to help debugging.
2017-09-15 20:54:27 -07:00
Alan Mishchenko
b63e3ee4b4
Experiment with mapping.
2017-09-15 12:40:43 -07:00
Alan Mishchenko
50bed57cae
Changes and fixed suggested by Clifford Wolf.
2017-09-15 10:59:39 -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
f1b7f9062e
Experiments with Glucose.
2017-09-07 23:02:26 -07:00