SVA to check sequence repitition

SystemVerilog
1

Hi,

I have a requirement where I need to check the repetition of sequence 11011010 on the valid signal when idle is low. Valid is pulled low when Idle is high. So, until idle is low I have to check for the sequence. Attached is the waveform for reference.

1024×251 27.9 KB

Thanks

2

In reply to nimitz_class:
I can easily provide the code, but it would be more beneficial for you to write something. Conceptually these are the steps:

  1. declare a sequence that has that signature.
  2. the property you need has as antecedent $fell(idle)
  3. the property is of the form
 
 $fell(a) |-> ##1 sequence_name[*1:$] ##1 $rose(a);
// another property needed

Idle |-> valid ==1'b0;
[/systemverilog[
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
3

In reply to ben@SystemVerilog.us:


sequence rep
   Valid[*2] ##1 !Valid ##1 Valid[*2] ##1 !Valid ##1 Valid ##1 !Valid;
endsequence

property check;
  @(posedge clk) $fell(Idle) |-> ##1 rep[*1:$] ##1 $rose(idle);
endproperty

property check2;
  @(posedge clk) Idle |-> Valid == 1'b0;
endproperty

I had the first property in place, but it did not work for me. Please let me know if this one is correct?

Thanks

4

In reply to nimitz_class:

Seeing the diagram, the check property should be:


property check;
  @(posedge clk) $fell(Idle) |-> rep[*1:$] ##1 $rose(idle);
endproperty
5

In reply to nimitz_class:
The error is the implication on the property check
SHould have been |-> instead of |-> ##1 …


module m; //OK now
  bit clk, idle, valid;
  event e1, e2;
  initial forever #10 clk = !clk;
  sequence rep;
        valid[*2] ##1!valid ##1 valid[*2] ##1 !valid ##1valid ##1!valid;
  endsequence

  property check;
    @(posedge clk) $fell(idle) |->  rep[*1:$] ##1 $rose(idle); // <<< Fixed this 
  endproperty

 property check2;
    @(posedge clk) idle |->valid == 1'b0;
 endproperty

 ap_check:  assert property(@ (posedge clk) check );  
 ap_check2: assert property(@ (posedge clk) check2 );  

   task automatic rpt(int x); //x==1 at init, 2 after 
    -> e1; 
     repeat(x) @(posedge clk)  valid <= 1'b1; 
     repeat(1) @(posedge clk)  valid <= 1'b0; 
     repeat(2) @(posedge clk)  valid <= 1'b1; 
     repeat(1) @(posedge clk)  valid <= 1'b0; 
     repeat(1) @(posedge clk)  valid <= 1'b1; 
     repeat(1) @(posedge clk)  valid <= 1'b0; 
     -> e2;
   endtask 
   
   initial begin 
    repeat(4) @(posedge clk) idle <= 1'b1; 
    @(posedge clk) idle <= 1'b0; 
    valid <= 1'b1; 
    rpt(1);
    rpt(2);
    rpt(2);  
    repeat(4) @(posedge clk) idle <= 1'b1; 
    $finish;
   end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: