bounce
Subproject |
S1, H1/2 |
Categories |
Systems of systems / blackbox tools |
Overview |
Bounce is a bounded model checking tool for partial designs to prove unrealizability of an invariant. To model the unknown behavior of the blackboxes, bounce supports both 01X modeling and multiple QBF modeling techniques. As back-end solvers, it uses MiraXT for SAT formulas, and QuBE, AIGsolve and QMiraXT for QBF formulas. Making use of the ability of MiraXT to compute Craig interpolants, bounce can prove 01X hardness of an incomplete design, which means that applying 01X to all blackbox outputs is not accurate enough to prove unrealizability. Based on the computed Craig interpolants and unsatisfiable cores, bounce provides heuristics to determine those blackbox outputs which should be modeled more precisely. Bounce reads netlists given in BBBLIF format, an extension to BLIF by blackbox descriptions. |
C. Miller, S. Kupferschmid, M. Lewis, and B. Becker. Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs. In O. Strichman and S. Szeider, editors, Theory and Applications of Satisfiability Testing (SAT), LNCS 6175, pp. 194-208, 2010. |
|
Blackbox BMC Suite |
|
Download |
Click here for the binary. |
Manual |
Just type ./bounce-static on the command line to see how it can be used. |
Status |
Prototype |