Assertion coding for a random pattern

SystemVerilog
1

Hi all, I need to write an assertion for a pattern
bit[3:0] pattern[6] = {'h0,'ha,'h0,'hb,'h0,'hc} which should be generic and not hardcoded…

Can i use the function for generating the assertion, if so how… pls help me with this.

Can this also be written without using function…

2

I’m guessing this is an interview question where you did not understand all the details, or forgot to ask. This is not enough information for us to help you. Assertions are expressed in terms of requirements and there’s nothing stated here.

3

Hi Dave, sorry i think i didn’t frame the question properly… sequence generates the above mentioned pattern…

We need to write an assertion to verify this pattern and to elaborate the complete details , when there is a start command asserted, this pattern like 0,a,0,b,0,c,0,d is to be followed for the data and after this there should be a stop signal asserted… Is this information clear ?

4

This is more detail, but there could be more. Usually with start/stop bits the pattern has a variable length. This example takes care of that.

module top;
  
  bit clk,start,stop;
  bit[3:0] data, pattern[] = {'h0,'ha,'h0,'hb,'h0,'hc};
  
  initial #5 repeat (20) #5 clk = !clk;
  
  initial begin
    @(posedge clk) start<=1;
    foreach(pattern[i])
      @(posedge clk)data <=pattern[i];
    @(posedge clk) stop <=1;
  end
  
  property pcheck;
    int index=0;
    @(posedge clk) $rose(start) |-> ##1 (!stop && data ==pattern[index], index++)[*] ##1 $rose(stop) && index == pattern.size;
  endproperty
  
  assert property(pcheck);
endmodule
5

Thanks for the code Dave… But when i tried running the above code, I see the below errors,

Also one more concern, if the pattern is generic say, incremental values generated in consecutive cycles, how the logic can be made? Can we randomize and generate such traffic and then use it here?

Error-[ETTNATE] Invalid type in temporal expression
assert_pattern.sv, 18
top, “pattern”
Expressions involving real, string, event, tagged union and dynamic
SystemVerilog types are not allowed in Boolean expressions in properties and
sequences.
At property 'unnamed$$2’
“assert_pattern.sv”, 21
Source info: ((@(posedge clk) ( 1, svaispcheck.indexsvais_ = 0 )
##0 $rose(start) |-> @(posedge clk) ( ##1 (( ((!stop) && (data ==
pattern[svaispcheck.indexsvais])),
svaispcheck.indexsvais += 1 ) [* 0:$])) ##1 ($rose(stop) &&
(svaispcheck.indexsvais__ == pattern.size))) )

Error-[ETTNATE] Invalid type in temporal expression
assert_pattern.sv, 18
top, “pattern”
Expressions involving real, string, event, tagged union and dynamic
SystemVerilog types are not allowed in Boolean expressions in properties and
sequences.
At property 'unnamed$$2’
“assert_pattern.sv”, 21
Source info: ((@(posedge clk) ( 1, svaispcheck.indexsvais_ = 0 )
##0 $rose(start) |-> @(posedge clk) ( ##1 (( ((!stop) && (data ==
pattern[svaispcheck.indexsvais])),
svaispcheck.indexsvais += 1 ) [* 0:$])) ##1 ($rose(stop) &&
(svaispcheck.indexsvais__ == pattern.size))) )

1 warning
2 errors

6

You have run into a tool specific issue. Use of dynanic types in assertions has been allowed since at least 1800-2017. There is even an example using a queue in the LRM section 16.6 Boolean expressions.