Automated correctness condition generation for formal verification of synthesized RTL designs

This work presents a formal methodology for verifying the functional correctness of synthesized register transfer level designs (RTL) generated by a high-level synthesis system. The verification is conducted by proving the observation equivalence of the RTL design with a description of its desired behavior.; High-level synthesis tools generate register transfer Level designs from algorithmic behavioral specifications. The high-level synthesis process consists of dependency graph scheduling, function unit allocation, register allocation, interconnect allocation and controller generation tasks. Widely used algorithms for these tasks retain the overall control flow structure of the behavioral specification allowing code motion only within basic blocks. Further, high-level synthesis algorithms are in general oblivious to the mathematical properties of arithmetic and logic operators, selecting and sharing RTL library modules solely based on matching uninterpreted function symbols and constants. Many researchers have noted that these features of high-level synthesis algorithms can be exploited to develop efficient verification strategies for synthesized designs. This dissertation reports a verification methodology that effectively exploits these features to achieve efficient and fully automated verification of synthesized designs.; Contributions of this research include formalization and formulation in higher-order logic in a theorem proving environment mathematical models for the synthesized register transfer level designs and their behavioral Specifications and a set of sufficient correctness conditions for these designs. It presents an in depth study of pipelining in design synthesis, and identifies the complete set of correctness conditions for RTL designs generated through the synthesis processes that employ pipelining techniques.; This method has been implemented in a verification tool (the correctness condition generator, CCG) and is integrated with a high-level synthesis system. CCG generates (1) formal specifications of the behavior and the RTL design including the data path and the controller, (2) the correctness lemmas establishing equivalence between the synthesized RTL design and its behavioral specification, and (3) their proof scripts that can be submitted to a higher-order logic proof checker. The tool performs model extraction, correctness condition generation and proof generation automatically and without human interaction. This approach is based on the identification, by the synthesis tool during the synthesis process, of the binding between critical specification variables and critical registers in the RTL design and between the critical states in the behavior and the corresponding states in the RTL design. CCG is capable of handling a broad range of behavior constructs that may be used for specifying the behavior and a wide variety of algorithms that may be employed during the synthesis process. Also, the verification algorithms of CCG have the appealing feature of relying on symbolic analysis of the uninterpreted values of the variables and registers. This has resulted in a considerable reduction in verification time compared to other post-synthesis verification systems, that are often restrained by this factor.