summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmc.h
Commit message (Expand)AuthorAgeFilesLines
* Improvements to command 'twoexact'.Alan Mishchenko2022-08-071-0/+4
* Improvements to command 'twoexact'.Alan Mishchenko2022-08-031-0/+4
* Usability improvements to &fftest.Alan Mishchenko2018-11-111-0/+1
* Adding timeout to twoexact and lutexact.Alan Mishchenko2018-09-081-0/+2
* Integrating SAT-based CEX minimization.Alan Mishchenko2018-03-251-0/+2
* Updates to exact synthesis commands.Alan Mishchenko2018-01-191-0/+2
* New exact synthesis command 'allexact'.Alan Mishchenko2017-12-301-4/+2
* New exact synthesis command 'allexact'.Alan Mishchenko2017-12-281-8/+19
* Adding parameter structure to 'twoexact' and 'lutexact'.Alan Mishchenko2017-12-061-2/+28
* An improvement to 'twoexact' and 'lutexact'.Alan Mishchenko2017-12-061-0/+1
* An improvement to 'twoexact' and 'lutexact'.Alan Mishchenko2017-12-061-0/+1
* An improvement to 'twoexact' and 'lutexact'.Alan Mishchenko2017-12-061-0/+2
* Trying to enable CNF simplification in &bmcs -g.Alan Mishchenko2017-09-071-0/+1
* Integrating Glucose into bmc3 -g.Alan Mishchenko2017-09-061-0/+1
* Integrating Glucose into &bmcs -g.Alan Mishchenko2017-09-061-0/+1
* Integrating Satoko into 'bmc' and 'bmc2'.Alan Mishchenko2017-08-161-2/+2
* Adding an option to bmc3 to use Satoko intead of the default SAT solver.Alan Mishchenko2017-08-131-0/+1
* Experiments with BMC.Alan Mishchenko2017-08-131-0/+1
* add frame done callback support for command &bmcsBaruch Sterin2017-08-091-0/+2
* %pdra: working on bmc3Yen-Sheng Ho2017-03-191-0/+2
* Adding PDR with abstraction.Alan Mishchenko2017-02-101-1/+2
* Improving CEX minimization.Alan Mishchenko2017-02-101-2/+2
* Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.Alan Mishchenko2016-05-191-0/+1
* Integrating new CNF generation into &bmc.Alan Mishchenko2016-01-121-0/+1
* Procedure for extending care CEX to all objects.Alan Mishchenko2015-05-141-0/+1
* Adding support for dumping faults not detected by a given test-set in &fftest...Alan Mishchenko2015-04-171-0/+1
* Adding support for cardinality constraints in &fftest (switches -K and -k).Alan Mishchenko2015-04-161-0/+2
* Adding switch &fftest -e to dump delay-tests in a special format.Alan Mishchenko2015-04-141-0/+1
* Added backward flop order to &icheck (switch -b).Alan Mishchenko2015-04-011-1/+1
* Adding flop-input-only switch -f in &fftest.Alan Mishchenko2015-03-141-0/+1
* Adding switch &fftest -N <num> to detect fixed vars after each <num> iterations.Alan Mishchenko2014-10-251-0/+1
* Adding symbolic fault representation in &fftest.Alan Mishchenko2014-05-141-0/+15
* Adding command to dump UNSAT core of BMC instance.Alan Mishchenko2014-04-071-1/+14
* Better CEX minimization and renaming of write_counter into write_cex.Alan Mishchenko2014-04-041-0/+6
* Adding per-output logging to bmc3.Alan Mishchenko2014-03-291-0/+1
* Experiments with inductive don't-cares.Alan Mishchenko2014-02-111-1/+1
* Specialized inductive check.Alan Mishchenko2013-11-051-0/+1
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-051-0/+1
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-0/+1
* Specialized induction check.Alan Mishchenko2013-10-311-1/+1
* Specialized induction check.Alan Mishchenko2013-10-311-0/+2
* New BMC engine.Alan Mishchenko2013-10-271-0/+1
* New BMC engine.Alan Mishchenko2013-10-271-0/+1
* Multi-output property solver.Alan Mishchenko2013-10-261-0/+12
* Multi-output property solver.Alan Mishchenko2013-10-231-0/+1
* Integrating synthesis into the new BMC engine.Alan Mishchenko2013-10-021-0/+1
* Added bridge integration for multi-output 'bmc3 -a'.Alan Mishchenko2013-09-171-0/+1
* Updates for the new BMC engine.Alan Mishchenko2013-09-101-0/+1
* Updates for the new BMC engine.Alan Mishchenko2013-09-051-0/+1
* Updates for the new BMC engine.Alan Mishchenko2013-09-051-3/+13