Theorem-proving guided development of formal assertions and their embedding in a high-level VLSI synthesis system

This thesis investigates a formal verification strategy for validating register-transfer level (RTL) designs generated during High-Level Synthesis (HLS). We present a unified formal framework wherein the exercise of design verification is conducted within the framework of the synthesis proms itself.; High-level synthesis is the technique of applying a collection of well-defined optimization algorithms to the problem of generating an efficient hardware design from an abstract behavioral specification. This thesis presents a novel approach to validating such synthesized RTL designs. In this technique, we identify a core set of verification conditions for the entire synthesis process. Each correctness condition in this set is then formulated in higher-order logic and verified for correctness against a formal specification of a task in synthesis that the correctness condition attempts to embody. All proofs are conducted in a higher-order logic theorem proving environment. The formalized verification conditions are embedded as program assertions in the implementation of the high level synthesis tool. We state with high confidence that a system so embedded synthesizes error-free RTL designs.; An appealing aspect of the verification technique is that the formal verification of the RTL design is carried out in the environment of the synthesis tool itself. The design is verified as it is synthesized. This avoids the complexity issues and tool capacity issues that often beset most verification techniques currently in use.; High-level synthesis involves data-path synthesis and controller synthesis. The optimization and mapping routines in high-level synthesis deal primarily with data-path synthesis. Controller synthesis on the other hand, is mainly derived from the input language semantics. Therefore, in addition to verifying that the HLS algorithms generate a correct RTL design, it is equally important to validate the control logic interpretations of the specification language semantics. Only then can one ensure the correctness of a synthesized RTL design. We propose a methodology, based on model checking, to verify the process of controller synthesis. An extensive collection of control-flow properties for a synthesized RTL design is identified. These properties are then formulated in Computation Tree Logic and verified against a formal model of the RTL controller in a model checking environment.; A high-level synthesis system is developed based on this formal verification technique described in this thesis. This synthesis system embedded with formal assertions, generates RTL designs whose correctness can be asserted with a high degree of confidence.