IncQuBE
Subproject |
S1 |
Categories |
Core algorithms |
Overview |
Within a cooperation with STAR-LAB (University of Genova, Italy), the search-based QBF solver QuBE7 has been extended to support assumptions and incremental solving, resulting into incQuBE. This extension includes a modification in the conflict analysis and learning procedure for correctly dealing with assumptions. Moreover, it supports don't touch literals, that is a partial preprocessing approach for simplifying a circuit without removing the output lines. This feature can be used when coupled with a bounded model checker, to the purpose of reducing the size of the transition relations. As an application making use of incremental QBF solving, we here provide the tool incBBBMC, a prototype bounded model checker for incomplete designs using the library incQuBE as solver engine. It reads netlists in restrictive verilog format and supports both forward and backward incremental bounded model checking. |
Publications |
--- |
Blackbox BMC Suite |
|
Download |
Click here for the binary. |
Manual |
Just type ./incBBBMC-static on the command line to see how it can be used. |
Status |
Prototype |