NDLI: Formal Probabilistic Timing Verification in RTL

Content Provider	IEEE Xplore Digital Library
Author	Kumar, J.A. Vasudevan, S.
Copyright Year	1982
Abstract	Variations in timing can occur due to multiple sources on a chip such as process variations and variations in input patterns. It is desirable to have variation awareness at the register transfer level (RTL), and estimate block level delay distributions early in the design cycle, to evaluate design choices quickly and minimize postsynthesis simulation costs. In previous work, we introduced statistical high-level analysis and rigorous performance estimation (SHARPE), a rigorous, systematic methodology to verify design correctness in RTL in the presence of variations. We described SHARPE in the context of computing statistical delay invariants with respect to input variations. We treated the RTL source code as a program and used static program analysis techniques to compute probabilities. We modeled the probabilistic RTL modules as discrete time Markov chains that are then checked formally for probabilistic invariants using PRISM, a probabilistic model checker. In this paper, we extend SHARPE to perform timing verification in RTL in the context of process variations. We achieved this by obtaining a set of process variation-aware RTL delay models and correspondingly modifying the existing steps in SHARPE. We illustrate SHARPE on the RTL description of the datapath of OR1200, an open source embedded processor. We also apply SHARPE to other data-intensive RTL designs such as nontrivial components of communication systems and a few benchmark designs.
Sponsorship	IEEE Council on Electronic Design Automation IEEE Circuits and Systems Society
Starting Page	788
Ending Page	801
Page Count	14
File Size	432391
File Format	PDF
ISSN	02780070
Volume Number	32
Issue Number	5
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-01-01
Publisher Place	U.S.A.
Access Restriction	One Nation One Subscription (ONOS)
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Delays Logic gates Probabilistic logic Solid modeling Optimization Context register transfer level (RTL) timing analysis Average case design formal methods probabilistic model checking
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Electrical and Electronic Engineering Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog

Analyzing Functional Coverage in Bounded Model Checking

Bounded Model Debugging

Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs

Model checking on timed-event structures

Debugging RTL Using Structural Dominance

A Formal Method for the Specification, Analysis, and Design of Register-Transfer Level Digital Logic

Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking

SAT-based unbounded symbolic model checking

Formal Probabilistic Timing Verification in RTL

Similar Documents

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog

Analyzing Functional Coverage in Bounded Model Checking

Bounded Model Debugging

Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs

Model checking on timed-event structures

Debugging RTL Using Structural Dominance

A Formal Method for the Specification, Analysis, and Design of Register-Transfer Level Digital Logic

Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking

SAT-based unbounded symbolic model checking

Formal Probabilistic Timing Verification in RTL