module some_asn;
bit a, b, clk;
bit[15:0] x=3, y=5; // // X and Y can be varying per simulation to simulation
// 1) Signal B must remain constant during the entire time A signal is asserted
ap_ab: assert property(@(posedge clk) a |-> b);
// 2) A asserts,
// B if asserts it should assert within X cycles of A
// and should remain asserted as long a A asserts
property p_axb;
bit[15:0] v_x;
($rose(a), v_x=x) |=>
first_match((1, v_x=v_x-1'b1)[*1:$] ##1 (b && v_x >=0)) |->
(b && a)[*1:$] ##1 !a;
endproperty
ap_axb:assert property(@(posedge clk) p_axb);
// ***** NOTE *****
// If ‘b’ is never true, a simulator will keep on evaluating the sequence
// inside the first_match() once $rose(a) is true.
// A solution
property p_axb2;
bit[15:0] v_x;
($rose(a), v_x=x) |=>
first_match(
((1, v_x=v_x-1'b1)[*1:$] ##1 (b && v_x >=0)) or
(v_x < 0 [->1])
) |->
(b && a)[*1:$] ##1 !a;
endproperty
ap_axb2:assert property(@(posedge clk) p_axb2);
// 3) if asserts A should stay asserted for a min of X cyles and stay upto a max of Y cycles
property p_axy;
bit[15:0] v_x, v_y;
($rose(a), v_x=x, v_y=y) |=>
first_match((a, v_x=v_x-1'b1, v_y=v_y-1'b1)[*1:$] ##1 v_x ==0) |->
(a, v_y=v_y-1'b1) [*1:$] ##1 !a && v_y >=0 ;
endproperty
ap_axy:assert property(@(posedge clk) p_axy);
endmodule
Ben Cohen systemverilog.us