Y. Kim, S. Kopuri, and N. Mansouri (USA)
Formal verification, synthesis, RTL design, pipelining.
We propose a formal methodology based on higher or der logic theorem proving for completely automated verification of register transfer level (RTL) designs with pipelined iterative control constructs. Viability of au tomating the entire verification process is a result of: (1) a two step verification approach, that relies on transforming the design into an equivalent non pipelined RTL to serve as an intermediary between the design and its specification; and (2) identification of three correctness conditions for RTL designs with pipelined control flow, that allow for a concise proof decomposition based on the control and data proper ties of this class of designs. We use the theorem prov ing environment PVS (Prototype Verification System) [9], integrated with a synthesis tool for conducting the verification task.
Important Links:
Go Back
