Deriving a simulation input generator and a coverage metric from a formal specification

This paper presents novel uses of functional interface specifications for verifying RTL designs. We demonstrate how a simulation environment, a correctness checker, and a functional coverage metric are all created automatically from a single specification. Additionally, the process exploits the structure of a specification written with simple style rules. The methodology was used to verify a largescale I/O design from the Stanford FLASH project. Categories and Subject Descriptors B.5.2 [RTL Implementation]: Design Aids General Terms Documentation, Performance, Design, Verification Keywords testbench, input generation, BDD minimization, coverage

• Type: Conference
• Year: 2002
• Where: DAC
• Authors: Kanna Shimizu, David L. Dill
• Keywords: DAC 2002, Design Automation, Functional Coverage Metric, Largescale I/o Design, RTL Implementation