Alan Mishchenko
aed9a87282
Adding specialized flop ordering before generalization in 'pdr'.
2017-02-06 00:54:18 -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
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
1a39fb3946
Adding print-out of critical path for mapped AIGs to &show.
2017-01-13 17:32:58 +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
74c8d35f33
Updates to delay optimization project.
2017-01-02 16:29:10 +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
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
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
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
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
Mathias Soeken
f5be157583
Merged alanmi/abc into default
2016-09-29 22:10:16 -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
b11406c566
Merged alanmi/abc into default
2016-09-09 11:49:43 +02:00
Alan Mishchenko
198fe99416
Experimental code for polynomial construction.
2016-09-05 23:47:58 +03:00
Mathias Soeken
e5636522bf
BMS fixes and start gates parameter.
2016-08-25 10:56:59 +02:00
Mathias Soeken
9bb5a2dd0d
Merged alanmi/abc into default
2016-08-21 18:12:05 +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
2f149364eb
Provide number of max cubes as parameter.
2016-08-16 18:33:53 +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
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
Alan Mishchenko
640100954a
Updates to arithmetic verification.
2016-08-05 20:34:44 -07:00