In reply to ben@SystemVerilog.us:
Is this the correct SVA based on the problem statement?
we store a value in cycle1 and then in
cycle2,3,4,5 we have one of b or c matching the a value in cycle1 and we also ensured ‘a’ value in cycles 2-5 is not matching it’s value in cycle1
we use [*4] as we are maintaining the check for 4 cycles from 2-5. Based on the problem statement it looks like a hard constraint to maintain the check for 4 consecutive cycles and is not optional. If it was optional then using ##[m:n] was appropriate.
Please correct me if I am wrong.
property p_a4bc;
int v;
@(posedge clk) (a inside {[0:31]}, v = a) |=> ((v == b || v==c) and (a != v))[*4];
//cycle1 //cycle2,3,4,5
endproperty
ap_p_a4bc: assert property(p_a4bc);