Write an assertion such that a given 2-bit command can't be equal to 2 more than 4 times within 60 clock cycles

SystemVerilog
1

I have written a assertion as below to verify command=2 doesnot happen more than 4 times in 60 clock cycles but seeing a compilation issue for sequence sequence_60_cycles;

module tb();
  
  bit clk;
  bit [1:0] cmd;
  
  initial begin
    clk = 0;
    forever #5 clk = ~clk;
  end

  sequence cmd_seq;
    
    (cmd[1:0] == 2'b10) [=4:$];
    
  endsequence
  
  sequence seq_60_cycles;
    ##60;
  endsequence
 property command_2_in_60_cycles;
   int tmp;
   @(posedge clk)
  // int tmp; 
   (cmd[1:0] ==2'b10) |-> not( cmd_seq) within seq_60_cycles;  
   
 endproperty
  
 A1 : assert property(command_2_in_60_cycles);
    initial begin
      $dumpfile("dump.vcd");
      $dumpvars;
      #600 $finish;
    end
    
    initial begin
      repeat(20) begin
        @(posedge clk);
        cmd = $random;
      end
      repeat(200) begin
        @(posedge clk);
        cmd = 2'b11;
      end
  end
endmodule

Error-[SE] Syntax error
Following verilog source has syntax error :
“testbench.sv”, 19: token is ‘;’
##60;

2

Your assertion is probematic because of the within and [=4] (more than 1 )
See the last example in my paper on Degeneracy
Paper: Understanding SVA Degeneracy
A MUST READ PAPER FOR SVA USERS!

sequence cmd_seq;
    (cmd[1:0] == 2'b10) [=4:$];
  endsequence

  sequence seq_60_cycles;
    ##60;
  endsequence
 property command_2_in_60_cycles;
   int tmp;
   @(posedge clk)
  // int tmp; 
   (cmd[1:0] ==2'b10) |-> not( cmd_seq) within seq_60_cycles; // probematic because of the within and [=4] (more than 1 )
 endproperty

 A1 : assert property(command_2_in_60_cycles); // BAD,

 A2_better: assert property(@(posedge clk) (cmd[1:0] ==2'b10) |=>
                                not (cmd_seq==2'b10[=5:60] intersect  1 [*60]);

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

3

This is better

A2_better3: assert property(@(posedge clk) 
 (cmd[1:0] ==2'b10) |=>
 (cmd_seq==2'b10[=0:4] intersect 1 [*60]);

I never liked the “not” operator.

4

Ben,
I observe following 2 issues with your code

  1. Goto and nonconsecutive repetition operators are not valid for sequences.
    i.e cmd_seq[=0:4] would be illegal
  2. If I re-write consequent to
    (cmd[1:0] == 2'b10)[=0:4] intersect 1 [*60]);
    Due to [=0] the consequent admits empty match and violates the quote from
    LRM 16.12.22 Nondegeneracy

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.

One possible way to avoid (2)

assert property(@(posedge clk)  ( (cmd[1:0] == 2'b10)[=1:4] or (cmd[1:0] != 2'b10)[*60] ) intersect 1 [*60]);
5

From my degeneracy paper

1493×571 81.8 KB

b[=0] // is equivalent to: 
##0 !b[*0]) or (##0 !b[*1:$])

Thus, you are correct in that due to [=0] the consequent admits empty match and violates the quote from
2.LRM 16.12.22 Nondegeneracy*

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
I like your solution

assert property(@(posedge clk)  ( (cmd[1:0] == 2'b10)[=1:4] or (cmd[1:0] != 2'b10)[*60] ) intersect 1 [*60]);

I sent this to members of the SV and SVA committee to address this degenracy issue for the next 1800 revision.
Issue:
When faced with degenerate sequences, 1800’2023 is unclear on what a simulator should do, particularly in situations resulting from parameter substitution that creates a degenerate sequence. In that situation, it would be undesirable to have to rewrite the code to get to a successful compilation. Existing tools differ in their interpretation of degenerate sequences - some report it as a degenerate situation, some issue a warning, and some proceed with the simulation.

document identifies the sections in the LRM that define degeneracy and highlights cases that pose challenges for users and tool vendors. Additionally, it proposes solutions for the next revision of the LRM.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

1 Like
6

Below code worked.

Thanks hdlcohen .

sequence cmd_seq;

(cmd[1:0] == 2'b10) [=5:60];

endsequence

sequence seq_60_cycles;
bit [6:0] counter_60=0;

(1, counter_60 = counter_60+1'b1, $display("The counter value = %0d", counter_60)) ##60 ##0 (counter_60 == 60,$display("End Counter value = %0d", counter_60));

endsequence
property command_2_in_60_cycles;
int tmp;
@(posedge clk)
// int tmp;
(cmd[1:0] ==2’b10) |-> not ((cmd_seq) within seq_60_cycles);

endproperty

COMMAND_4_TIME_IN_60_CYCLES: assert property(command_2_in_60_cycles) else $error(“%0t Assertion got failed”, $time);

7

COnsider what the assertion should do, instead of what it should not do.
assert property(@(posedge clk) ( (cmd[1:0] == 2’b10)[=1:4] or (cmd[1:0] != 2’b10)[*60] ) intersect 1 [*60]);
Ben

8

ALso, use the intersect, not the within.
See my paper on the within and the [=2]