Exploiting PSL standard assertions in a theorem-proving-based verification environment
Pages 400 - 403
Abstract
Assertion-based design is becoming more widely used in industry. However, little has been done to take advantage of existing design assertions in the theorem-proving verification environments. In this paper, we present our work on development of the semi-automated theorem-proving based verification system ROVERIFIC that makes use of existing design assertions. We have defined generic predicate templates that capture the semantics of PSL, and a subset of Verilog. ROVERIFIC uses these templates, and automatically compiles a design under verification (Verilog) and its assertions (PSL) into the higher-order predicates of the PVS [11] theorem proving system. Design verification can be subsequently conducted by proving the correctness properties.
References
[1]
Accellera. Accellera Standard SystemVerilog 3.1, April 2003.
[2]
Accellera Organization. Open Verification Library, Assertion Monitor Reference Manual, 2003.
[3]
Accellera Organization. Property Specification Language Reference Manual, 2004.
[4]
S. Berezin. The SYMP tool. WWW URL: http://www.cms.edu/modelcheck/symp.html, 2001.
[5]
H. D. Foster, A. C. Krolnik, and D. J. Lacey. Assertion-Based Desi. Kluwer Academic Publishers, 2003.
[6]
M. Gordon, J. Hurd, and K. Slind. Executing the formal semantics of the accellera property specification language by mechanised theorem proving. 2003.
[7]
R. Ho. Assertions aid design for verification strategy.
[8]
D. Korening. Application specification higher order logic theorem proving. 2002.
[9]
T. Kropf. Benchmark-Circuits for Hardware-Verification, 1994. www:http://goethe.ira.uka.de/hvg/.
[10]
C.-J. H. S. Mark D. Aagaard. The formal verification of a pipelined double-precision ieee floating-point multiplier. 1995.
[11]
S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Language Reference. SRI International, November 2001.
[12]
A. G. R. Boulton, M. Gordon, J. Harrison, J. Herbert, and J. Tassel. Experience with embedding hardware description language in hol. 1992.
Index Terms
- Exploiting PSL standard assertions in a theorem-proving-based verification environment
Recommendations
An Automated Framework for Correction and Debug of PSL Assertions
MTV '10: Proceedings of the 2010 11th International Workshop on Microprocessor Test and VerificationFunctional verification is becoming a major bottleneck in modern VLSI design flows. To manage this growing problem, assertion-based verification has been adopted as one of the key technologies to increase the quality and efficiency of verification. ...
PSL Assertion Checking Using Temporally Extended High-Level Decision Diagrams
This paper proposes a novel method for the simulation-based checking of assertions written in the PSL language. The method uses a system representation model called High-Level Decision Diagrams (HLDDs). Previous works have shown that HLDDs are an ...
An automatic ABV methodology enabling PSL assertions across SLD flow for SOCs modeled in SystemC
Property specification languages and ABV (assertion-based verification) driven by simulation are being recognized by many as essential for verification of today's increasingly complex designs. In addition, there are few mature approaches that ...
Comments
Information & Contributors
Information
Published In
April 2005
518 pages
Copyright © 2005 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 17 April 2005
Check for updates
Author Tags
Qualifiers
- Article
Conference
Acceptance Rates
Overall Acceptance Rate 312 of 1,156 submissions, 27%
Upcoming Conference
GLSVLSI '25
- Sponsor:
- sigda
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 266Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)0
Reflects downloads up to 07 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in