SystemVerilog Assertions

2023-04-01 07:51| 来源: 网络整理| 查看: 265

The behavior of a system can be written as an assertion that should be true at all times. Hence assertions are used to validate the behavior of a system defined as properties, and can also be used in functional coverage.

What are properties of a design ?

If a property of the design that is being checked for by an assertion does not behave in the expected way, the assertion fails. For example, assume the design requests for grant and expects to receive an ack within the next four cycles. But if the design gets an ack on the fifth cycle, the property that an ack should be returned within 4 clocks is violated and the assertion fails.

If a property of the design that is being checked for by an assertion is forbidden from happening, the assertion fails. For example, assume a small processor decodes instructions read from memory, encounters an unknown instruction and results in a fatal error. If such a scenario is never expected from the design, the property of the design that only valid instructions can be read from memory is violated and the assertion fails.

As evident from the two examples above, properties of a given design is checked for by writing SystemVerilog assertions.

Why do we need assertions ?

An assertion is nothing but a more concise representation of a functional checker. The functionality represented by an assertion can also be written as a SystemVerilog task or checker that involves more line of code. Some disadvantages of doing so are listed below:

SystemVerilog is verbose and difficult to maintain and scale code with the number of properties Being a procedural language, it is difficult to write checkers that involve many parallel events in the same period of time // A property written in Verilog/SystemVerilog always @ (posedge clk) begin if (!(a && b)) $display ("Assertion failed"); end

SystemVerilog Assertions is a declarative language used to specify temporal conditions, and is very concise and easier to maintain.

// The property above written in SystemVerilog Assertions syntax assert property(@(posedge clk) a && b); Types of Assertion Statements

An assertion statement can be of the following types:

Type Description assert To specify that the given property of the design is true in simulation assume To specify that the given property is an assumption and used by formal tools to generate input stimulus cover To evaluate the property for functional coverage restrict To specify the property as a constraint on formal verification computations and is ignored by simulators Building Blocks of AssertionsSequence

A sequence of multiple logical events typically form the functionality of any design. These events may span across multiple clocks or exist for just a single clock cycle. To keep things simple, smaller events can be depicted using simple assertions which can then be used to build more complex behavior patterns.

// Sequence syntax sequence endsequence // Assert the sequence assert property (); Property

These events can be represented as a sequence and a number of sequences can be combined to create more complex sequences or properties.

It is necessary to include a clocking event inside a sequence or property in order to assert it.

// Property syntax property or endproperty // Assert the property assert property ();

There are two kinds of assertions - Immediate and Concurrent.

Immediate Assertion

Immediate assertions are executed like a statement in a procedural block and follow simulation event semantics. These are used to verify an immediate property during simulation.

always @ () begin ... // This is an immediate assertion executed only // at this point in the execution flow $assert(!fifo_empty); // Assert that fifo is not empty at this point ... end

Click here to learn more on Immediate Assertions

Concurrent Assertions

Concurrent assertions are based on clock semantics and use sampled values of their expressions. Circuit behavior is described using SystemVerilog properties that gets evaluated everytime on the given clock and a failure in simulation indicates that the described functional behavior got violated.

// Define a property to specify that an ack should be // returned for every grant within 1:4 clocks property p_ack; @(posedge clk) gnt ##[1:4] ack; endproperty assert property(p_ack); // Assert the given property is true always

Click here to learn more on Concurrent Assertions

Steps to create assertions

Following are the steps to create assertions:

Step 1: Create boolean expressions Step 2: Create sequence expressions Step 3: Create property Step 4: Assert property Example

The first sequence s_ab validates that b is high the next clock when a is high, and the second sequence s_cd validates that d is high 2 clocks after c is found high. The property asserts that the second sequence is on the next cycle after the first sequence.

module tb; bit a, b, c, d; bit clk; always #10 clk = ~clk; initial begin for (int i = 0; i

Note that there are some violations for the property that is asserted using assert statement.

Simulation Log Compiler version P-2019.06-1; Runtime version P-2019.06-1; Jan 8 05:02 2020 Warning : License for product VCSRuntime_Net(725) will expire within 10 days, on: 17-jan-2020. If you would like to temporarily disable this message, set the VCS_LIC_EXPIRE_WARNING environment variable to the number of days before expiration that you want this message to start (the minimum is 0). 0 a=0 b=1 c=0 d=0 10 a=0 b=0 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 10ns failed at 10ns Offending 'a' 30 a=1 b=0 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 30ns failed at 30ns Offending 'a' 50 a=0 b=0 c=1 d=1 70 a=1 b=1 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 70ns failed at 70ns Offending 'a' "testbench.sv", 28: tb.unnamed$$_3: started at 50ns failed at 70ns Offending 'b' 90 a=1 b=1 c=0 d=1 110 a=0 b=1 c=0 d=1 130 a=0 b=0 c=1 d=0 "testbench.sv", 28: tb.unnamed$$_3: started at 130ns failed at 130ns Offending 'a' "testbench.sv", 28: tb.unnamed$$_3: started at 90ns failed at 130ns Offending 'c' 150 a=0 b=0 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 150ns failed at 150ns Offending 'a' 170 a=1 b=1 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 170ns failed at 170ns Offending 'a' 190 a=0 b=1 c=1 d=0 210 a=1 b=1 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 210ns failed at 210ns Offending 'a' 230 a=1 b=1 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 190ns failed at 230ns Offending 'c' 250 a=1 b=1 c=0 d=0 270 a=1 b=0 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 230ns failed at 270ns Offending 'c' 290 a=0 b=1 c=1 d=0 "testbench.sv", 28: tb.unnamed$$_3: started at 270ns failed at 290ns Offending 'b' "testbench.sv", 28: tb.unnamed$$_3: started at 250ns failed at 290ns Offending 'c' 310 a=0 b=1 c=0 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 310ns failed at 310ns Offending 'a' 330 a=1 b=0 c=1 d=0 "testbench.sv", 28: tb.unnamed$$_3: started at 330ns failed at 330ns Offending 'a' "testbench.sv", 28: tb.unnamed$$_3: started at 290ns failed at 330ns Offending 'c' 350 a=0 b=1 c=0 d=1 370 a=0 b=1 c=1 d=1 "testbench.sv", 28: tb.unnamed$$_3: started at 370ns failed at 370ns Offending 'a' "testbench.sv", 28: tb.unnamed$$_3: started at 390ns failed at 390ns Offending 'a' $finish called from file "testbench.sv", line 13. $finish at simulation time 400 V C S S i m u l a t i o n R e p o r t

【本文地址】

公司简介

联系我们