October 25, 2004
Assertion Based Verification
Please note that contributed articles, blog entries, and comments posted on EDACafe.com are the views and opinion of the author and do not necessarily represent the views and opinions of the management and staff of Internet Business Systems and its subsidiary web-sites.
Jack Horgan - Contributing Editor


by Jack Horgan - Contributing Editor
Posted anew every four weeks or so, the EDA WEEKLY delivers to its readers information concerning the latest happenings in the EDA industry, covering vendors, products, finances and new developments. Frequently, feature articles on selected public or private EDA companies are presented. Brought to you by EDACafe.com. If we miss a story or subject that you feel deserves to be included, or you just want to suggest a future topic, please contact us! Questions? Feedback? Click here. Thank you!




Open Verification Library (OVL)


The OVL is a freely downloadable open source library available in two versions. One contains Verilog modules, and the other contains VHDL modules. These modules are used to specify properties of an HDL design to be verified, either in simulation or using formal or semi-formal methods. The modules are instantiated as assertion monitors that will flag violations of the specified property. These modules provide a standard interface for multiple design verification tools, thus enabling a more seamless flow. OVL defines approximately 30 checkers.


assert_always assert_implication assert_quiescent_state
assert_always_on_edge assert_increment assert_range
assert_cycle_sequence assert_never assert_time
assert_decrement assert_next assert_transition
asset_delta assert_underflow assert_unchange
asset_ever_parity assert_odd_parity assert_width
assert_fifo_index assert_one_cold assert_win_change
assert_frame assert_one_hot assert_win_unchange
assert_handshake assert_proposition assert_window
assert_no_overflow assert_no_underflow assert_zero_one_hot
assert_no_transition    

Table OVL Supported Assertions


Every assertion library definition contains a severity_level, options, and a message. As an example consider the following. The assert_always assertion continuously monitors the test_expr at every positive edge of the triggering event or clock clk. It contends that the specified test_expr will always evaluate TRUE. If test_expr evaluates to FALSE, the assertion will fire (that is, an error condition has been detected in the code). The syntax is


assert_always [#(severity_level, options, msg)] inst_name (clk, reset_n, test_expr);




Property Specification Language (PSL)


A PSL specification consists of assertions regarding properties of a design under a set of assumptions. A property is built from Boolean expressions, which describe behavior over one cycle, sequential expressions, which describe multi-cycle behavior, and temporal operators, which describe relations over time between Boolean expressions and sequences.
assertion: A statement that a given property is required to hold and a directive to verification tools to verify that it does hold.

assumption: A statement that the design is constrained by the given property and a directive to verification tools to consider only paths on which the given property holds.

constraint: A condition (usually on the input signals) that limits the set of behaviors to be considered.

property: A collection of logical and temporal relationships between and among subordinate Boolean expressions, sequential expressions, and other properties that in aggregate represent a set of behaviors.
Assertions (or constraints) may be expressed either declaratively or procedurally. A declarative assertion is always active, and is evaluated concurrently with other components in the design. A procedural assertion, on the other hand, is a statement within procedural code, and is executed sequentially in its turn within the procedural description.


PSL consists of four layers: Boolean, temporal, verification, and modeling. The Boolean layer is used to build expressions composed of variables within the design
model that are, in turn, used by the other layers. Boolean layer expressions are evaluated in a single evaluation cycle. The temporal layer is used to describe properties of the design. It is known as the temporal layer because, in addition to simple properties, it can also describe properties involving complex temporal relations between signals. Temporal expressions (always, never, next, until, before) are evaluated over a series of evaluation cycles. Sugar Extended Regular Expressions (SERE) provide an easy way to string together sequences of boolean expressions over time. The verification layer is used to tell the verification tools what to do (assume, assert, ) with the
properties described by the temporal layer. The modeling layer is used to model the behavior of design inputs (for tools, such as formal verification tools, which do not use test cases) and to model auxiliary hardware that is not part of the design, but is needed for verification. PSL comes in four flavors: one for each of the hardware description languages SystemVerilog, Verilog, VHDL, and GDL.




System Verilog Assertions (SVA)


According to SystemVerilog.org “In SystemVerilog, assertion information is built into the language, eliminating the need for the special modules, pragmas or PLI calls used in traditional Verilog. Embedded assertions capture real “design intent” in terms of functionality and constraints, and are verified by simulation before application of any formal or dynamic verification methods. This approach helps to avoid recoding errors, increase test accuracy, simplify the testbench, and enable test reuse. The full controllability and observability of internal circuit nodes afforded by ABV can significantly reduce design debug time. For example, IBM reports a 50% reduction in
debug time using this
methodology. Very importantly, this controllability and observability will spur the innovation of advanced design and verification tools, with one area of interest being assertion-based synthesis.”


Assertions are described in Section 17 of System Verilog 3.1 Language Reference Manual (LRM). The following paragraphs give some idea of the language.


There are two kinds of assertions: concurrent and immediate. The immediate assertion statement is a test of an expression performed when the statement is executed in procedural code. The expression is non-temporal and treated as a condition as in an “if statement”. The statement specifies the actions to taken depending upon success or failure of the assertion.


Immediate_assertion_statement:

    assert (expression) [[pass_statement] else fail_statement]


Concurrent assertions describe behavior that spans over time. The expression in the immediate formulation above would be replaced by a sequential expression or property. Concurrent assertions are based on clock semantics and use sampled values of variables. The timing model employed in a concurrent assertion specification is based on clock ticks. This way, a predictable result can be obtained from the evaluation, regardless of the simulator's internal mechanism of ordering events and evaluating events.


« Previous Page 1 | 2 | 3 | 4 | 5  Next Page »


You can find the full EDACafe event calendar here.


To read more news, click here.



-- Jack Horgan, EDACafe.com Contributing Editor.


Rating:


Review Article Be the first to review this article

EMA:

Featured Video
Editorial
Peggy AycinenaWhat Would Joe Do?
by Peggy Aycinena
Retail Therapy: Jump starting Black Friday
Peggy AycinenaIP Showcase
by Peggy Aycinena
REUSE 2016: Addressing the Four Freedoms
More Editorial  
Jobs
AE-APPS SUPPORT/TMM for EDA Careers at San Jose-SOCAL-AZ, CA
Principal Circuit Design Engineer for Rambus at Sunnyvale, CA
Development Engineer-WEB SKILLS +++ for EDA Careers at North Valley, CA
ACCOUNT MANAGER MUNICH GERMANY EU for EDA Careers at MUNICH, Germany
Manager, Field Applications Engineering for Real Intent at Sunnyvale, CA
FAE FIELD APPLICATIONS SAN DIEGO for EDA Careers at San Diego, CA
Upcoming Events
Zuken Innovation World 2017, April 24 - 26, 2017, Hilton Head Marriott Resort & Spa in Hilton Head Island, SC at Hilton Head Marriott Resort & Spa Hilton Head Island NC - Apr 24 - 26, 2017
CST Webinar Series



Internet Business Systems © 2016 Internet Business Systems, Inc.
595 Millich Dr., Suite 216, Campbell, CA 95008
+1 (408)-337-6870 — Contact Us, or visit our other sites:
AECCafe - Architectural Design and Engineering TechJobsCafe - Technical Jobs and Resumes GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy Policy