A property on its own is never evaluated for checking an expression. It must be used within a verification statement for this to occur. A verification statement states the verification function to be performed on the property.

The statement can be one of the following:
1)assert to specify the property as a checker to ensure that the property holds for the design
2)assume to specify the property as an assumption for the environment
3)cover to monitor the property evaluation for coverage

A concurrent assertion statement can be specified in any of the following:
1) An always block or initial block as a statement, wherever these blocks can appear
2) A module
3) An interface
4) A program


The assert statement is used to enforce a property as a checker. When the property for the assert statement is evaluated to be true, the pass statements of the action block are executed. Otherwise, the fail statements of the action_block are executed.

a1_assertion:assert property ( @(posedge clk) req inside {0, 1} ) ;
property proto_assertion ;
@(posedge clk) req |-> req[*1:$] ##0 ack;


The environment must be constrained so that the properties that are assumed shall hold. Like an assert property, an assumed property must be checked and reported if it fails to hold. There is no requirement on the tools to report successes of the assumed properties.

a1:assume property ( @(posedge clk) req dist {0:=40, 1:=60} ) ;
property proto ;
@(posedge clk) req |-> req[*1:$] ##0 ack;

Cover Statement:

To monitor sequences and other behavioral aspects of the design for coverage, the same syntax is used with the cover statement. The tools can gather information about the evaluation and report the results at the end of simulation. When the property for the cover statement is successful, the pass statements can specify a coverage function, such as monitoring all paths for a sequence. The pass statement shall not include any concurrent assert, assume, or cover statement.

Coverage results are divided into two categories: coverage for properties and coverage for sequences.

Coverage for sequences:
Number of attempts
Number of matches
Multiple matches per attempt are all counted

Coverage for properties:
Number of attempts
Number of passes
Number of vacuous passes
Number of failures

Expect Statement:

The expect statement is a procedural blocking statement that allows waiting on a property evaluation. The syntax of the expect statement accepts a named property or a property declaration. The expect statement accepts the same syntax used to assert a property. An expect statement causes the executing process to block until the given property succeeds or fails. The statement following the expect is scheduled to execute after processing the Observe region in which the property completes its evaluation. When the property succeeds or fails, the process unblocks, and the property stops being evaluated

program tst;
initial begin
# 200ms;
expect( @(posedge clk) a ##1 b ##1 c ) else $error( "expect failed" );
ABC: ...


To facilitate verification separate from design, it is possible to specify properties and bind them to specific modules or instances. The following are some goals of providing this feature:
It allows verification engineers to verify with minimum changes to the design code and files.
It allows a convenient mechanism to attach verification intellectual Protocol (VIP) to a module or an instance.
No semantic changes to the assertions are introduced due to this feature. It is equivalent to writing properties external to a module, using hierarchical path names.

The bind directive can be specified in any of the following:
A module
An interface
A compilation-unit scope

Event Simulation
Assertion Types
Assertion System Tasks
Concurrent Assertion Layers
Verification Directive

Report a Bug or Comment on This section - Your input is what keeps Testbench.in improving with time!




copyright 2007-2017 :: all rights reserved www.testbench.in::Disclaimer