SystemVerilog Assertion for toggling signal

Hello,

I’m trying to write a property to check a signal that behaves with the following requirements

1- signal ‘a’ should be high for a number of cycles (first_hi)
2- After that signal ‘a’ should go low for a number of cycles (first low)
3- Following that ‘a’ should go high again for a number of cycles (second_hi)
4- Finally ‘a’ should go low for a number of cycles (second_lo)

I have very little knowledge on SVA syntax and most of the times I get confused with writing SVAs that actually work, so far my assertion looks like this
Version 1:


   property double_beat_signal_check(clk, areset_n, signal, first_hi, first_low, second_hi, second_low);
      @(posedge clk) disable iff(!areset_n) 
      $rose(signal) |-> ##(first_hi) signal ##(first_low) !signal ##(second_hi) signal ##(second_low) !signal;
   endproperty

Version 2:


     property double_beat_signal_check(clk, areset_n, signal, first_hi, first_low, second_hi, second_low);
      @(posedge clk) disable iff(!areset_n) 
      $rose(signal) |-> signal[*first_hi] ##0 $fell(signal) ##0 !signal[*first_low]
                        ##0 $rose(signal) ##0 signal[*second_hi]
                        ##0 $fell(signal) ##0 signal[*second_low];
   endproperty

I tried to create a module to test both implementations (both are failing) but from what I can see from the waveform the signal has the correct behaviour

Any help on this is really appreciated.

-R

In reply to rgarcia07:
Several issues with your assertion:

 a[*first_hi] ##0 $fell(a)  // using "a" instead of signal
//This sequence is always a no match, regardless of the values of the repeat.
//For simplicity, let first_hi==1.  Now you have as a sequence
(a[*1] ##0 fell(a) // or more simply
a ##0 fell(a) // and that says that in the very SAME cycle, a==1 and a==0
// What you need is
a[*first_hi] ##1 $fell(a)
// Your property would then read
property double_beat_signal_check(clk, areset_n, signal, first_hi, first_low, second_hi, second_low);
@(posedge clk) disable iff(!areset_n)
$rose(signal) |-> signal[*first_hi] ##1 $fell(signal) ##1 !signal[*first_low]
##1 $rose(signal) ##1 signal[*second_hi]
##1 $fell(signal) ##1 signal[*second_low];
endproperty

  1. A second issue is that depeding upon the values of the repeats, a 2nd attempt of the assertion may fail. An attempt ocurs at every $rose(a) in this property. For example:

// assertion  $ose(a) |-> a[*2] ##1 !a[*3] ##1 a[*1] ##1 !a[*1]
a    000011111111100000000000011110000
clk     |   |   |   |   |   |   |   |   |   |   |   |   |   |   |   |
Attempt1    ^
count a==1  1    2              1   P // assertion pases
count a==0          1   2   3      1
----
Attempt2                        ^
count a==1                      1   F  // assertion FAILS, a[*2] failed
count a==0                         1   2   3      1

If you want the assertion to trigger once, use the model (my reply) at
https://verificationacademy.com/forums/systemverilog/system-verilog-assertion-2
You ca also use the action block to reset that block to zero for pass or fail at the ed of a triggered assertion.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thank you very much for your detailed explanation I was able to write the assertion thanks to your comments and observations.

-R

In reply to rgarcia07:
Glad it helped. One more comment on yout testbench at SVA test - EDA Playground

  • Use nonblocking assignments (e.g., db <= 1’b1;)instead of blocking blocking assignments. SystemVerilog is very loose in the syntax, but to avoid issues, it is always best to use best practice and recommended rules.
  • There are cases where directed tests are needed. However, in most cases it is easier, faster, and probably better to use constrained-random tests. For this, I use the following template stored in PhaseExpress application https://www.phraseexpress.com/ You need to modify the constraints to fit the needs.
    PhraseExpress is a text expander software, that manages frequently used text templates for insertion into any program. It is free for personal use. I highly recommend it.

module top;
timeunit 1ns/100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
initial begin
$timeformat(-9, 1, "ns", 8);
$display("%t", $realtime);
end
always  @(posedge clk)  begin
end
initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb)  with
{ va dist {1'b1:=1, 1'b0:=3};
vb dist {1'b1:=1, 1'b0:=2};
})  `uvm_fatal("RAND", "This is a randomize error")
#1; a <= va;
b <= vb;
end
$stop;
end
endmodule     

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy