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
Bruno Schmitt
871899dcea
- Adding a compile time option to use floats for var activity (now it can be either ‘double’, ‘float’ or ‘unsigned’ (default))
...
- Adding vector of ‘float’
- Adding an option to configure the ratio of learnt clauses to be kept in clause database at each reduction (0 means no reduction).
- Other small changes.
2017-02-09 05:17:50 -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
cf24a0eb0c
Compiler warning.
2017-02-08 14:12:49 -08:00
Alan Mishchenko
de4bf41c53
New command &satoko.
2017-02-08 14:10:08 -08:00
Alan Mishchenko
80f5070dbe
Re-introducing floating-point activity in the SAT solver.
2017-02-07 02:05:03 -08:00
Alan Mishchenko
44dbf992a7
Re-introducing floating-point activity in the SAT solver.
2017-02-06 23:28:00 -08:00
Alan Mishchenko
542f84d2fb
Small changes to compile satoko on Windows.
2017-02-06 20:54:41 -08:00
Bruno Schmitt
6ae1f35fae
Merged alanmi/abc into default
2017-02-06 20:39:53 -08:00
Bruno Schmitt
0fb4442a82
Small changes to support old compilers.
2017-02-06 19:50:57 -08:00
Alan Mishchenko
495a34e3ce
Fixing compilation problem in 'dsc' package.
2017-02-06 18:53:35 -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
89e8e50069
Improving new X-valued simulation in 'pdr'.
2017-02-06 00:21:28 -08:00
Alan Mishchenko
f34029dd09
Improvements in AIG visualization.
2017-02-05 12:28:34 -08:00
Alan Mishchenko
8b6de217f6
Compiler warnings.
2017-02-05 11:08:44 -08:00
Alan Mishchenko
afcbb09717
Corner-case bug-fix in library preprocessor for standard-cell mapping.
2017-02-05 10:43:07 -08:00
Alan Mishchenko
2c4c464ab0
Adding structural flop priority heuristics in 'pdr' (bug fix).
2017-02-03 21:31:40 -08:00
Alan Mishchenko
45bf0369a8
Adding structural flop priority heuristics in 'pdr'.
2017-02-03 19:51:53 -08:00
Alan Mishchenko
a2cebd3e20
Removing dead code in 'pdr'.
2017-02-03 17:32:44 -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
f14ee271ab
Reordering if-statements in the xsat solver.
2017-02-02 12:44:54 -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
dc7445e435
Typo.
2017-01-31 11:09:38 -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
9171bb32ad
Updates to arithmetic verification.
2017-01-28 17:04:22 -08:00
Alan Mishchenko
782125c61e
Custom floating-point number.
2017-01-28 12:01:32 -08:00
Alan Mishchenko
ec6b765314
Custom floating-point number.
2017-01-28 11:46:47 -08:00
Alan Mishchenko
596276152c
Fixing non-reproducability related to floating-point numbers.
2017-01-27 15:22:23 -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
57286e8ab6
Adding features for invariant minimization.
2017-01-25 22:29:51 -08:00
Alan Mishchenko
636332c63e
Adding features for invariant minimization.
2017-01-25 22:27:46 -08:00
Alan Mishchenko
a02bdebcc4
Corner-case bug in MiniLUT.
2017-01-25 14:58:06 -08:00
Alan Mishchenko
32288c6964
Adding features for invariant minimization.
2017-01-25 14:02:14 -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