In reply to rkg_:
After every successful antecedent, a new thread is fired, and that thread is independent of any other previously fired thread. That can cause errors if you want to check the packets independently. Below is a simulatable example where I used the block.
/*property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |=>
(1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
This assertion is failing even after lock is asserted ( just after 6 posedge of sampled_monclk after lock assertion ).
Do we need to put some extra logic so that one lock is asserted it should not check until the next packet will come ? */
module top;
timeunit 1ns; timeprecision 100ps;
`include "uvm_macros.svh" import uvm_pkg::*;
bit clk, a, b, c, reset_n, block;
initial forever #10 clk = !clk;
function void set_block(bit x);
block=x;
endfunction
ap_a2b2c: assert property(@ (posedge clk)
$rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));
ap_a2b2cBLOCK: assert property(@ (posedge clk)
($rose(a) && block==0, set_block(1)) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]))
set_block(0); else set_block(0) ;
initial begin
repeat (200) begin
@(posedge clk);
if (!randomize(a, b, c) with {
a dist {1'b1 := 1, 1'b0 := 3};
b dist {1'b1 := 1, 1'b0 := 4};
c dist {1'b1 := 1, 1'b0 := 4};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule