2014 · 16 citations · 10 references
EngineeringHardware Verification LanguageVerificationComputer ArchitectureComputer-aided VerificationSource Code AnalysisCode CoverageSoftware AnalysisFormal VerificationHardware Verification LanguagesHardware SecurityHardware VerificationSource CodeRuntime VerificationStatic AnalysisComputer EngineeringComputer ScienceRtl Source CodeStatic Program AnalysisHardware EmulationProgram AnalysisSoftware TestingFormal MethodsFunctional Verification
Assertions are gaining importance in pre-silicon hardware verification to ensure expected design behavior. Coverage of an assertion in terms of statements of a Register Transfer Level (RTL) source code is a very accessible metric for understanding the scope of assertions and for debug. However, few methods to report it currently exist. We present a methodology to define and compute code coverage of an assertion. Our method is based on static and dynamic analysis of the RTL source code. We demonstrate the scalability and effectiveness of our approach with experimental results on real designs for both manual and automatically generated assertions.
10
The temporal logic of programs
Amir Pnueli · 1977 · 5.6K citations
The Verilog hardware description language
Choice Reviews Online · 1991 · 502 citations
Coverage estimation for symbolic model checking
Yatin Hoskote, Timothy Kam, Pei-Hsin Ho et al. · 1999 · 133 citations · Full text