Encoding RTL Constructs for Mathsat: A preliminary report

Formal checking at Register-Transfer Level (RTL) is currently a fundamental step in the design of hardware circuits. Most tools for formal checking, however, work at the boolean level, which is not expressive enough to capture the abstract, high level (e.g., structural, word level) information of RTL designs. Tools for formal checking are thus confronted with problems which are `flattened` down to boolean level, so that a predominant part of their computational effort is wasted in performing useless boolean search on the bitwise encoding of integer data and arithmetical operations. In this paper we present a way of encoding RTL constructs into SMT formulas, that is, boolean combinations of boolean variables and quantifier-free constraints in Integer Linear Arithmetic. Such formulas can be handled by the Mathsat tool (and others) directly, without flattening to boolean level, so that to reduce drastically the computational effort. We propose a mixed boolean/ILP encoding, in which control variables are encoded as boolean variables, datapath variables as integer variables; control constructs are handled as boolean combination of control variables and predicates over datapath variables, and datapath constructs are encoded, as much as possible, as linear arithmetical constraints over datapath variables