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.
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.
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.
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)
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.
You can find the full EDACafe event calendar here.
To read more news, click here.
-- Jack Horgan, EDACafe.com Contributing Editor.
Be the first to review this article