Sciweavers

Share
DAC
2002
ACM

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

10 years 3 months ago
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
Kanna Shimizu, David L. Dill
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2002
Where DAC
Authors Kanna Shimizu, David L. Dill
Comments (0)
books