SV Assertions using Generate Block

SystemVerilog
1

Hi
I am writing a SV assertion on signal which is an array and I want to generate an assertion for each bit of signal .

for (genvar i =0; i < SIGNAL_WIDTH; i ++) begin: assert_block_1
  property check_P;
  @(posedge clk)
     signal_a[i] |-> signal_b[i];
   endproperty: check_P
  check_A: assert property (check_P)
  else begin
  <fail_statement>
  end
  end: assert_block_1

This generates number of assertions properly but should we write one property with arguments as parameterisable inputs and then loop only on assert block .

1 Like
2

There is no functional difference between the two styles. However, you should always strive to make you code as reusable as possible. Moving the property outside of the generate loop makes it available for you outside that particular loop.

4

Dave, what about efficiency? For example which is more simulator efficient?

property p(v); a[v] |-> b[v+1]; endproperty 
ap_1: assert property(@ (posedge clk)  p(0);  
// or 
ap_2: assert property(@ (posedge clk) a[0] |-> b[0+1] );
5

Concurrent assertions go through an elaboration step similar to module instances and ports collapsing. The elaboration process removes properties and sequence containers and expands them. There is no overhead in passing arguments like there would be for a procedural function.

1 Like
6

I’ve always believed that concurrent assertions arguments are processed as if they were ‘string substitution’, given that they cannot be altered by the property/sequence. With that in mind there can’t be any performance penalty between the two code implementations.

1 Like
7

Yes, I would use the term “text substitution” like a macro. That’s really what they are with more formal syntax semantics.

1 Like