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 Quote:
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
