Chip Design: Verilog Assertion (SVA) Syntax-EEWORLD

Collect

Assertions are placed in Verilog designs to facilitate checking for abnormalities during simulation. When an abnormality occurs, the assertion will sound an alarm. Generally, assertions are added to digital circuit designs, and the proportion of assertions in the entire design should be no less than 30%. The following is the syntax of assertions:

1. SVA insertion location: In a .v file:

module ABC ();

rtl code

SVA Assertions

endmodule

Note: Do not write SVA outside of enmodule.

2. The general format for writing assertions is:

[Example] Assertion name 1: assert property(event 1) // no semicolon

$display("........",$time); //with semicolon

else

$display("........",$time); //with semicolon

Assertion name 2: assert property (event 2)

$display("........",$time);

else

$display("........",$time);

The purpose of assertion is to determine whether "Event 1" and "Event 2" will occur. If they occur, they are recorded as pass, and if they do not occur, they are recorded as fail. Note: There is no if in the above example, only else. The assertion itself plays the role of if.

In the above example, event 1 and event 2 can be written in two ways:

(1) Sequence block: sequence name;

. . . . . . . . . ;

endsequence

(2) Property block: property name;

. . . . . . . . . ;

endsequence

From the definition, the sequence block is used to define an event (brick), while the property block is used to organize events to form a more complex process (building). The content of the sequence block cannot be empty. You can write random characters, but it cannot be nothing. A sequence can also contain another sequence, such as:

sequence s1;

s2(a,b);

endsequence //s1 and s2 are both sequence blocks

Both the sequence block and the property block have name, and when using assert call, it is: "assert property(name);"

In SVA, sequence blocks are generally used to define combinational logic assertions, while property blocks are generally used to define an assertion with a time concept, which will often call sequence. This is why some timing operations such as "|->" can only be used for property.

Note: The SVA syntax introduced below can be written in both sequence and property. The syntax is universal.

3. Property with parameters, sequence with parameters

Property can also have parameters, which can be events or signals. When calling, it is written as: assert property (p1(a,b))

The slave sequence called by the master sequence can also take parameters, for example, the slave sequence is named s2 and the master sequence is named s1:

sequence s1;

s2(a,b);

endsequence

4. Local variables can be defined inside a property, just like a normal program.

property p1;

int cnt;

.....................

endproperty

[Note] Before introducing the syntax, let's first emphasize the general format of writing assertions:

Generally, assertions are based on sequential logic. It is rare to see assertions based on pure combinational logic because they consume too much memory (sequential logic is judged once per clock cycle, while combinational logic is judged multiple times per clock cycle, which is too much for the memory).

Therefore, the general rule for writing assertions is: time + event. To assert what event occurred, you must first specify the time when the event occurred, for example

Every rising edge of the clock + something happens

When a signal drops + something happens

5. Syntax 1: "Combinatorial logic" relationship between signals (or events):

(1) Common ones are: &&, ||, !, ^

(2) Either a or b can be true, but if both are true, a is considered true: firstmatch(a||b), which is basically the same as “||”, except that a is considered true only when both a and b are true.

(3) a ? b:c ———— If event a succeeds, b is triggered; if event a fails, c is triggered.

6. Syntax 2: Determine the behavior of an independent signal in "sequential logic":

@ (posedge clk) A event; ———— When clk rises, if event A occurs, the assertion will alarm.

Edge-triggered built-in function: (assuming there is a signal a)

$rose( a );———— signal rises

$fell( a );———— signal drops

$stable( a );———— The signal value remains unchanged

7. Syntax 3: Determine the behavioral relationship between multiple events/signals in "temporal logic":

(1) intersect(a,b)———— Determine that events a and b occur at the same time and end at the same time.

(2) a within b ———— Determine that the time period in which event b occurs includes the time period in which event a occurs.

(3) a ##2 b ———— It is determined that event b will occur within 2 units of time after event a occurs.

a ##[1:3] b ———— Determine that event b will occur within 1 to 3 units of time after event a occurs.

a ##[3:$] b ———— Determine that event b will definitely occur 3 cycles after event a occurs.

(4) c throughout (a ##2 b) ———— asserts that in the process from the occurrence of event a to the occurrence of event b, event c “always” occurs.

(5) @ (posedge clk) a |-> b ———— After determining the rising edge of clk, event a "starts to occur" and at the same time, event b occurs.

(6) @ (posedge clk) a.end |-> b ———— After determining the rising edge of clk, event a is executed for a period of time and then "ends". At the same time, event b occurs.

Note: "a |-> b" is a judgment sentence in logic, that is:

if a

else

succeed;

Therefore, once a happens, b must happen for the assertion to succeed. If a does not happen, go to else and it will also succeed.

(7) @ (posedge clk) a |=> b ———— After determining the rising edge of clk, event a starts to occur, and after the next clock edge, event b starts to occur.

(8) @ (posedge clk) a |=>##2b ———— After determining the rising edge of clk, event a starts to occur, and after the next three clock edges, event b starts to occur.

(9) @ (posedge clk) $past(a,2) == 1'b1 ———— Determine that the level value of signal a was 1 "before" 2 clock cycles.

(10) @ (posedge clk) a [*3] ———— Assert that “@ (posedge clk) a” holds for three consecutive clock cycles.

@ (posedge clk) a [*1:3] ———— Asserts that “@ (posedge clk) a” holds for 1 to 3 consecutive clock cycles.

@ (posedge clk) a [->3] ———— Asserts that “@ (posedge clk) a” holds for 3 non-consecutive clock cycles.

Let's take a more complex example:

property ABC;

int tmp;

@(posedge clk) ($rose(a),tmp = b) |-> ##4 (c == (tmp*tmp+1)) ##3 d[*3];

endproperty

A property description in the above example: When clk rises, the assertion starts. First, it is asserted that signal a changes from low to high, and the value of signal b at this time is assigned to variable tmp. After 4 clock cycles, it is asserted that the value of signal c is b^2+1 4 cycles ago. After another 3 cycles, it is asserted that signal d will definitely rise. After another 3 cycles, signal d rises again. Only if these assertions are successful, the assertion succeeds. Otherwise, if signal a does not rise from the beginning, the assertion also succeeds.

8. Syntax 4: Multiple clock domain joint assertion: An assertion can represent the signal relationship of multiple clock domains, for example:

@ (posedge clk1) a |-> ##1 @ (posedge clk2) b

When clk1 rises, event a occurs. If the second clock clk2 rises, event b occurs. "##1" does not represent a clock cycle when crossing clocks, but only means waiting for the most recent crossing clock event. So it cannot be written as ##2 or other. But it can be written as:

@ (posedge clk1) a |=> @ (posedge clk2) b

9. Syntax 5: Bus assertion function

A bus is a collection of bit lines that together represent a number. SVA provides a function to determine the status of multiple bits together, namely the bus assertion function:

(1) $onehot(BUS) ————There is only one bit in BUS that is high, and the others are low.

(2) $onehot0(BUS) ————No more than 1 bit in BUS is high, and all 0s are also allowed.

(3) $isunknown(BUS) ————There is a high impedance state or an unknown state in BUS.

(4) countones(BUS)==n ————Only n bits in BUS are high, the others are low.

10. Syntax 6: Masking the indefinite state

When a signal is asserted, if the signal is in an unreset, indeterminate state, no matter how it is asserted, it will report: "Assertion failed". In order not to report problems in an indeterminate state, it can be shielded during assertion.

For example: @(posedge clk) (q == $past(d)), when it is not reset, an error is reported. The shielding method is to rewrite the sentence as follows:

@(posedge clk) disable iff (!rst_n) (q == $past(d)) //rst is low level valid

10. Syntax 6: Assertion coverage detection:

name: cover property (func_name)

11. Enable assertion compilation and display in modelsim:

(1) [Compile Verilog code according to system Verilog] vlog -sv abc.v

(2) [Add -assertdebug to the simulation command] vsim -assertdebug -novopt testbench

(3) [If you want to see an analysis of whether the assertion succeeded or not, use the command to open the assertion window] view assertions

12. Add assertion compilation and display functions to VCS:

Add a sentence in the fsdb file: $fsdbDumpSVA

Add some options to the VCS compilation parameters: system "vcs $VCS_SIMULATION":

-assert enable_diag\

-assert vpiSeqBeginTime\

-assert vpiSeqFail\

-assert report=path\

-assert finish_maxfail=100

*************************************************** *********************************************

[Experience] Here are some experiences for writing assertions:

1. Purpose of assertion: The traditional verification method is to add stimulus and observe the output. This method relies heavily on cases. If the cases are not well designed, the problems are not easy to expose. Assertions are accompanied by RTL code, do not rely on test cases, but are relatively "static". For example: we want to test a serial data read/write unit, there is only one data line, and the four-bit address is transmitted first, and then the data is transmitted.

(1) Case verification method: write an address, then write a piece of data, and then read the address to see if the output is the data just written.

(2) Assertion method: There is no need to specially design the address and data. When a write is initiated, the address is stored in a variable during the address transmission time, and the data is stored in a variable during the data transmission time. It is then observed whether the data exists at the address in the RAM.

Assertion design is equivalent to implementing the RTL functions again on a computer.

2. Assertions can contain functions and tasks. Functions are often used in assertions because some processing is very complex, and assertions are "one-sentence" and cannot be divided into several sentences to express, so functions are needed to share the work for assertions.

3. Assertions allow you to specify events that occur simultaneously, which is combinatorial logic. You can write it as: a && b, or a ##0 b. You cannot write ##0.5, and decimals are not supported.

4. Assertions are to use computers to simulate the running process of RTL. When the RTL functions are complex, you must use variables. Assertions support int and array declarations in C language, but when assigning values, you "cannot" write: ##4 var = Signal, where var is a variable in the assertion and has nothing to do with RTL, and Signal is a signal in RTL. This sentence is to assign the value of Signal to var in the 4th cycle so that the value can be used later. However, this sentence only has variable assignments and no assertions for RTL signals, so an error will be reported. The solution is: ##4 ("nonsense", var = Signal). If there must be an assertion, we can write "nonsense", for example: data == data, etc. If there are multiple variables to be assigned, it is also OK, ##4 (nonsense, variable 1 assignment, variable 2 assignment...........)

5. About the expression style of assertion: The "a |-> b" in the grammar introduction is actually the logic of "if a, then b". When a does not happen, b will not be judged, and the assertion will succeed naturally. But when our logic is

if a1

{

if a2

then

}

How do you express this with an assertion? Maybe you can write it as: "a1 |-> a2 |-> b", which is also OK, but the commonly used expression is:

"a1 && a2 |-> b" or "a1 ##3 a2 |-> b"

6. Regarding the timing of assertions: There is one issue that needs to be noted about assertions of sequential logic:

For example: suppose that when the rising edge of clk arrives, b<=a. When writing the above logic as an assertion, if it is written as "@(posedge clk) b==a", it looks the same as b<=a, but it is actually wrong. Because when the clock rises, b has not yet obtained the value of a, and a still needs a period of holding time. That is, the signal value in the assertion is actually the value before the clock edge arrives, not the value they will be programmed after the clock edge arrives. Therefore, the assertion of the b<=a logic should be: "@ (posedge clk) (a==a,tmp=a) |=> (b==tmp);"

In view of the above points, let’s take a complex example:

The function of assertion wr is to check whether the serial address input is correct. The serial address input line is DataIn. The return value of $time is in units of 0.1ns (because the unit in my testbench is specified as `timescale 1ns/100ps, the accuracy is 100ps = 0.1ns), so $time/10 is ns.

///////////////////////////////////////////////////// //////////////////////////////

wr: assert property(wr_p)

$display("succeed：",$time/10);

else

$display("error: ",$time/10);

///////////////////////////////////////////////////// //////////////////////////////

//Assert that an int array arr[4] can be declared,

//“@(posedge clk) !vld_pulse_r[0] && !DataIn” is the real precondition

//“##4 (read==read, arr[0] = DataIn)” is just for assigning values within a specific time. The useful statement is “arr[0] = DataIn”. //“read==read” is nonsense just for compilation to pass.

//After arr is assigned, enter function for processing to determine whether the actual address addr is the same as the data processed by junc.

//“addr == junc(arr[0],arr[1],arr[2],arr[3]);” is the junction call.

property wr_p;

int arr[4];

@(posedge clk) !vld_pulse_r[0] && !DataIn

##4 (read==read, arr[0] = DataIn)

##1 (read==read, arr[1] = DataIn)

##1 (read==read, arr[2] = DataIn)

##1 (read==read, arr[3] = DataIn) |=>

addr == junc(arr[0],arr[1],arr[2],arr[3]);

endproperty

///////////////////////////////////////////////////// ///////////////////////////

function [3:0] junc;

input a,b,c,d;

reg [3:0] a1;

reg [3:0] b1;

reg [3:0] c1;

reg [3:0] d1;

a1 = {3'b0,a};

b1 = {3'b0,b};

c1 = {3'b0,c};

d1 = {3'b0,d};

junc = a1+(b1<<1)+(c1<<2)+(d1<<3);

$display(junc);

endfunction

///////////////////////////////////////////////////// ////////////////////////

7. If you want to use functions similar to for(){....} in SVA, don’t forget [*3] introduced in the syntax. This is the only way to implement for in assertions.

##4 (nonsense, cnt = 0, arr[cnt] = DataIn, cnt++) // Initialize,

##1 (read==read, arr[cnt] = DataIn, cnt++)[*3] //Loop 3 times

8. Each assertion is a small program: As in the above example, at time point ##4, (nonsense, cnt = 0, arr[cnt] = DataIn, cnt++) is a small program. The signal assertion must be the first sentence, and other operations are performed in order.

9. In addition to int and float in C language, asserted variables can also be digital circuit types such as reg [n:0].

10. Note:

Like this:

propertyept_p;

@(posedge rd_clk) ((rd_num == 0) |-> rd_ept)

&& (rd_ept |-> (rd_num == 0));

endproperty

This is wrong. After writing |->, you can no longer use event combination logic such as &&.

The solution is to use 2 assertions, there is no better way.

Reference address：Chip Design: Verilog Assertion (SVA) Syntax

Previous article：Chip design: modelsim do script
Next article：Problems and solutions when downloading IAR!

Recommended ReadingLatest update time:2024-11-16 13:25

FPGA/CPLD Implementation of Simple UART in Verilog

Test platform: MACHXO640 Programming language: Verilog Random testing: Yes Baud rate: 9600 Bit error rate: 1%oooooo Goal: Implement a simple UART on xo640 that can parse serial port data and store it in registers , using FIFO to transfer data. Then, later, various data

[Embedded]

Popular Resources
Popular amplifiers