Assertion to check only one occurence of a pattern

SystemVerilog
, ,
1

Hi,

I am trying to verify, in a serial bit stream, that a given pattern occurs only once. To check this I fed the serial input to a shift register and trying to poll the number of times the pattern was detected. The assertion that will check for the occurrence of the pattern at least once is working.
Could you suggest how to check the max repetitions w/o using the parallel data.

The pattern is 0xF within the stream of 30 bits


module ser_dut(input a, input start, input clk);
  

  reg [3:0] pattern_reg;
  
  bit [4:0] bits_in_frame; 
  bit [1:0] num_header;
  bit toggle;
  
  
  always @(posedge clk)
    begin
      if(start) begin
        
      pattern_reg = {pattern_reg,a};
        bits_in_frame = bits_in_frame +1; 
        if (pattern_reg==4'hF && bits_in_frame <30)
        begin
          num_header = num_header+1;
        end
      end
      if(!start)
        begin
          num_header = 0;
          bits_in_frame =0;
          pattern_reg=0;
        end
    end
    

  
     sequence allfour ;
                 a[*4]; 
     endsequence
   
  

  
  check_sva1: assert property(@(posedge clk) $rose(start) |->  allfour  within 1[*30]   )  $display("Assertion Min PASS at time %t", $time); else $display("Assert Min FAIL at time %t", $time);
  
     check_sva2: assert property(@(posedge clk) $rose(start) |-> (num_header<=1) throughout 1[*30] )  $display("Assertion Max PASS at time %t", $time); else $display("Assert MAX FAIL at time %t", $time);
    
endmodule
2

In reply to Nagarjuna Chary:

Try the following, it is untested, but looks OK to me.


     property p_check_header; 
       bit [3:0] pattern_reg; 
       bit [1:0] num_header;
           @(posedge clk) ($rose(start), pattern_reg=0, num_header=0) |-> 
                         ( (1, pattern_reg = {pattern_reg,a}) ##0  
                           (1, num_header += pattern_reg==4'hF) ) [*30]  ##0 (num_header<=1);
     endproperty  
     ap_check_header: assert property( p_check_header) $display("Assertion Max PASS at time %t", $time); 
                                                   else $display("Assert MAX FAIL at time %t", $time);

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) https://rb.gy/cwy7nb
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Thanks, Ben. The solution works good but I am looking for some means to achieve it without parallelizing the data. There seems to be no way to use sequence repetition and goto operator together. The construct I wanted to use was something like this, for which the compiler fires errors.

$rose(start) |-> not ( a[*4] [->2] )

4

In reply to Nagarjuna Chary:

The following works: AVOID the not opr. Intead check for the positive expected results. Here we’re looking that a[*4] occurs no more than once in 20 cycles.
Since the Non-consecutive repetition operator is a Booleaan (Boolean([=n]), we
can use the endpoints instead.


ap_no4a: assert property(@ (posedge clk) 
		$rose(start) ##4 1 |->  (q_a4.triggered[=1]  intersect 1[*20]));



module m;
	`include "uvm_macros.svh" 	import uvm_pkg::*;
	bit a, start, clk;
	event e;
	initial forever #10 clk = !clk;
	
	function void pass_event();
		-> e; 
	endfunction

	sequence q_a4;
	 @(posedge clk) a[*4] ##0 (1, pass_event());
	endsequence 
  
	ap_no4a: assert property(@ (posedge clk) 
		$rose(start) ##4 1 |->  (q_a4.triggered[=1]  intersect 1[*20]));

	initial begin
		bit once; 
		int count;
		repeat (200) begin
		  @(posedge clk) start<=1'b1;
          @(posedge clk) start <=1'b0;
		  if (!randomize(once) with {
			// a dist {1'b1 := 4, 1'b0 := 1};
			once dist {1'b1 := 1, 1'b0 := 1};
		  })
			`uvm_error("MYERR", "This is a randomize error");
		  if(once) begin 
            repeat(6) @(posedge clk); 
            a <= 1'b1;  repeat(4)  @(posedge clk); 
            a <= 1'b0;  
		  end 
		  else // twice 
		    begin 
		      repeat(2) @(posedge clk); 
			  a <= 1'b1;  repeat(4)  @(posedge clk); 
              a <= 1'b0;  
              repeat(2) @(posedge clk); 
			  a <= 1'b1;  repeat(4)  @(posedge clk); 
              a <= 1'b0;  
		  end
          repeat(20) @(posedge clk);
		end

		$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) https://rb.gy/cwy7nb
  3. Papers: