Formal
and semi-formal verification 
Efficient Hybrid Solving for RTL circuits |
| In this project, we develop a new methods for checking satisfiability of register-transfer level (RTL) circuits with both Boolean and integer arithmetic primitives -- Hybrid SAT solving. This has wide application in verification and validation of RTL circuits. |
|
|
| Hybrid DPLL search |
| We use a DPLL-style decision procedure for the solver. The satisfiability of a mixed Boolean-Arithmetic constraint on a general RTL circuit is translated into checking for simultaneous satisfiability of arithmetic and Boolean constraints in the circuit. |
| Decision Strategy |
|
Our decision strategy
operates on a subset of variables on the boundary between control and
datapath to bound the search space. This enables the efficient
combination of Boolean SAT and linear integer-arithmetic-solving
techniques. Efficient finite-domain constraint propagation can improve the efficiency of the modified DPLL procedure. Conflict-based learning, using the variables on the boundary of control and data-path, yields additional performance benefits. |
| Hybrid Sequential Search |
| In our work on Boolean sequential searches, we showed that state cubes are very effective in bounding the search space for sequential circuits. |
|
|
| The same idea can be extended to search in sequential RTL circuits, by using relations of Boolean and word-level variables to represent sets of states that have been visited. An example is shown in the above figure. We can represent a huge number of states depending on the word-size in just a few relations. |
| Current Status & Availability |
| The hybrid solver package is currently experimental and is not available for download. |
| Publications: • M.K. Iyer, G. Parthasarathy, and K.-T. Cheng, "SHIVA - A Hybrid Constraint Solver for Circuits", Proceedings of the SRC TechCon, July, 2003. |
