How to use throughout operator in systemverilog assertions

system-verilog assertions system-verilog-assertions
wisemonkey picture wisemonkey · Jun 8, 2015 · Viewed 12.4k times · Source

Here is a spec: If signal a is asserted then it must be asserted till signal b is asserted and then it should de-assert on next clock edge. I'm reading through 16.9.9 of LRM (as well as http://www.testbench.in/AS_06_SEQUENCES.html) and the way I understood it, above mentioned spec can be written as

   property a2b_notA;
        @(posedge clk) ($rose (a) ##0 (a throughout b)) |=> (~a);
   endproperty
   a_a2b_notA: assert property (a2b_notA);

However this fails immediately on second clock edge after starting, and I can't figure out why.

Answer

Tudor Timi picture Tudor Timi · Jun 8, 2015

You're correct in wanting to use the throughout operator for your assertion, but the code you wrote has some problems. Let's look at it piece by piece.

Whenever I write an assertion I pay attention to the natural language description of what I want to check. In your case, we know we want to trigger when a goes from 0 to 1. Everything that happens afterwards is the behavior that we want to check, so it should be on the right hand side of an implication operator:

$rose(a) |-> ... something ...

The way you wrote your assertion, it would only trigger checks if the throughout sequence also happened after rose(a). This would cause you to ignore bad behavior.

The next piece of the puzzle is "a must stay high until b is asserted". Here we'll use the throughout operator. The sequence "until b is asserted" is expressed as b [->1]. This is equivalent to !b [*] ##1 b. Our sequence should thus be a throughout b [->1].

The throughout sequence will end when b goes high. At this point we need to check that a goes low on the next cycle: ##1 !a. I've used logical negation here because I find it clearer than bitwise negation, but the result should be the same.

Putting it all together, the whole property should be:

$rose(a) |-> (a throughout b [->1]) ##1 !a;

I've used overlapping implication here because b could already be high when a goes high, in which case I'm assuming that a should go low immediately on the next cycle. If not, you can fiddle with the details yourself.

You can find a working example on EDAPlayground.

Related questions

what is the difference between -> and => in system verilog assertions?

I wanted to know when to use -> and => in SVA ? Are there any differences between sequence A; req |-> ##1 gnt; endsequence and sequence B; req |=> ##1 gnt; endsequence Please let me know.. Thank you.

Read More
Verilog: How to instantiate a module

If I have a Verilog module 'top' and a verilog module 'subcomponent' how do I instantiate subcomponent in top? top: module top( input clk, input rst_n, input enable, input [9:0] data_rx_1, input [9:0] data_rx_2, output [9:0] data_tx_2 ); subcomponent: module …

Read More
Indexing vectors and arrays with +:

I am seeing a code in SystemVerilog which has something like this: if(address[2*pointer+:2]) do_something; How should I understand the +: when indexing this vector? I found that it is called bit slicing, but I can't find an explanation …

Read More