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

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.


    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.


Review Article Be the first to review this article
Featured Video
More Editorial  
Verification Engineer for Ambarella at Santa Clara, CA
ASIC Design Engineer 2 for Ambarella at Santa Clara, CA
Staff Software Engineer - (170059) for brocade at San Jose, CA
Engr, Elec Des 2 for KLA-Tencor at Milpitas, CA
Senior FPGA Designer for Fidus Electronic Product Development at Fremont, CA
Upcoming Events
CDNLive Silicon Valley 2017 at Santa Clara Convention Center Santa Clara CA - Apr 11 - 12, 2017
10th Anniversary of Cyber-Physical Systems Week at Pittsburgh, PA, USA PA - Apr 18 - 21, 2017
DVCon 2017 China, April 19, 2017, Parkyard Hotel Shanghai, China at Parkyard Hotel Shanghai Shanghai China - Apr 19, 2017
Zuken Innovation World 2017 at Hilton Head Marriott Resort & Spa Hilton Head Island NC - Apr 24 - 26, 2017
S2C: FPGA Base prototyping- Download white paper

Internet Business Systems © 2017 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