How to assert a bit sequence using concurrent assertions

SystemVerilog
, ,
7

In reply to raku:

  1. I made a slight mistake, which I corrected above, I missed the “1” in
    (1, v_collected[i]=serial, i=i-1’b1)

 property p_data_lsb2msb; // Updated 
      bit[7:0] v_data, v_collected;
      bit[2:0] i;
      @(posedge clk)(sync, v_data=data, i=7) |=> // serial output is from msb to lsb 
          (1, v_collected[i]=serial, i=i-1'b1)[*8] ##1 v_collected==v_data; 
  endproperty

Please explain when or if sync is high thought 8 cycles does this assertion creates multiple threads or a single thread is created.Also if multiple thread are creates whether “i” value of assertion in each thread remains different from each or all will have same value

I assumed that sync was one pulse, indicating the start of the serial transmission, before the first bit of data, like the one in a UART. I don’t know your design, but if sync is high for all 8 bits, then you can do something like


module par2ser;
  bit[7:0] data; 
  bit clk, sync, serial; 
  property p_data_msb2lsb; 
      bit[7:0] v_data, v_collected;
      bit[2:0] i;
      @(posedge clk)($rose(sync), v_data=data, i=0) |-> // serial output is from lsb to msb 
          (1, v_collected[i]=serial, i=i+1'b1)[*8] ##1 v_collected==v_data; 
  endproperty 
 
  property p_data_lsb2msb; 
      bit[7:0] v_data, v_collected;
      bit[2:0] i;
      @(posedge clk)($rose(sync), v_data=data, i=7) |-> // serial output is from msb to lsb 
          (1, v_collected[i]=serial, i=i-1'b1)[*8] ##1 v_collected==v_data; 
  endproperty 
 
  ap_data_msb2lsb: assert property(p_data_msb2lsb); 
  a_data_lsb2msb:  assert property(_data_lsb2msb);

In this case, there is one thread for the successful attempt. The $rose insures one successful attempt, and one thread. You have multiple threads in a successful attempt if you have in the antecedent the ORing of sequences, like


a ##[1:4] b |-> c
a ##1 b[*1:4] |-> c
Here ypou would need a first_match() lile
first_match(a ##[1:4] b) |-> c
first_match(a ##1 b[*1:4]) |-> c

Each local variable for each atteempt, when the assertion is first sampled and started, is independent of other previously threads started at previous attempts.
Local variables are “local” to the property.
Ben SystemVerilog.us