bounce

| project staff | description | benchmarks | publications |

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.

To evaluate bounce we used some VHDL designs available at http://opencores.org/. First, the blackboxes are inserted into the behavioral VHDL code of the benchmarks allowing us to select specific entities (multiplier, divider,...) of the circuit. Furthermore, errors can be inserted directly into the VHDL code. The VHDL code is compiled using Synopsys Design Compiler and then synthesized to Verilog using a minimized gate library containing only one and two input logic gates and latches. These Verilog designs can be directly translated into BBBLIF format. We used the following designs:

FPU: This design is an IEEE-754 compliant pipelined double precision floating point unit that supports four basic operations (+,-,*,/), multiple rounding modes and exceptions. The instances differ in initialization settings and the locations of errors, which are directly inserted into the netlist by changing some random gates. On average, the instances contain about 21.000 gates and 2.700 latches. With the multiplication and division unit replaced by blackboxes, proper functionality of the sign bit for addition and subtraction operation is falsified.

Plasma-MIPS: The Plasma-MIPS design is a simple pipelined 32-bit microprocessor supporting all MIPS Version I user mode instructions. For the instances, the size of the bootloader was modified resulting in about 17.000 gates and 2.500 latches. With the multiplier and shifter of the ALU blackboxed, it is verified that a certain state of the bootloader can be reached.

UART: The UART design consists of a pipelined UART (universal asynchronous receiver transmitter) pair running on different bit rates. The instances differ in bit rates of the UART modules and contain about 150 latches and 1300 gates. With the UART controller blackboxed, it is verified that all possible 8-bit inputs to the UART can be transmitted and received properly.

QALU: The QALU benchmark is a VLIW ALU supporting several logic operations on four arithmetic untis which are parameterized in their bit width. With different arithmetic units of the ALU blackboxed, an error in the XOR operation is detected. Note, that this benchmark is a modification of the VLIW ALU of the AVACS benchmark set and not available at opencores.org.