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
Principle Electronic Design Engr for Cypress Semiconductor at San Jose, California
Senior Electrical Engineer for Allen & Shariff Corporation at Pittsburgh, Pennsylvania
Director, Business Development for Kongsberg Geospatial at remote from home, Any State in the USA
Director, Business Development for Kongsberg Geospatial at Ottawa, Canada
Upcoming Events
IPC Technical Education - PCB Layout - Place and Route at Del Mar Fairgrounds 2260 Jimmy Durante Blvd. Del Mar CA - May 2, 2018
IPC Technical Education at Wisconsin Center 400 W Wisconsin Ave. Milwaukee WI - May 8, 2018
IPC High Reliability Forum at Embassy Suites: Baltimore-At BWI Airport 1300 Concourse Drive Linthicum MD - May 15 - 17, 2018
TrueCircuits: IoTPLL

Internet Business Systems © 2018 Internet Business Systems, Inc.
25 North 14th Steet, Suite 710, San Jose, CA 95112
+1 (408) 882-6554 — 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 PolicyAdvertise