if i do this my assertion starts evaluating but is never triggered even if i have start == 1 on posedge CLK.
my intention here is when i see start on posedge of CLK after 4 posedge of CLKOUT i should see start_out set and also that addr_out and ap_id_out should be same as what i had when start was 1 on posedge of CLK.
so i am trying to save addr_l and apid_l when assertion triggers. how do i save those variable and use them later in same assertion?
@(posedge CLK) disable iff(~resetb)…
Thus, resetb is a reset signal that goes from 0 to 1.
Assertion is disabled when resetb==0.
@(posedge CLK) disable iff(~resetb) ((start === 1'b1),addr_l=reg_addr,apid_l=ap_id) ##1 @(posedge CLK_OUT) (~resetb) [*4]|=>...
//If (~resetb==0) the assertion is disabled, thus never fires.
// Since you are trying to test the after effect of a reset, you need to delete the disable. Thus,
property req_to_out_chk;
logic [19:0] addr_l;
logic [11:0] apid_l;
@(posedge CLK) ((start === 1'b1),addr_l=reg_addr,apid_l=ap_id) ##1 @(posedge CLK_OUT) (~resetb) [*4]
|=>( (start_out == 1) && (addr_out == addr_l) && (ap_id_out == apid_l) );
endproperty
// BTW, arethe clocks working at startup?
@ben. thanks for the update. i figured that and reran it is working now. what i wasnt sure is my approach to saving the variable on first clock and then using them to compare on different clock. and since my clk is faster than clk_out i will have more than one instance of assertion triggered (4 in this case) will that create an issue with storing local variable. but i tested it out looks like it will work.
i had to make minor adjustment to implement to match spec
In reply to shahparth08:
The different clocks with local variables is OK. However, there are rules about local variables, particularly with the AND OR operators. They are defined in 1800’2017, however, I expanded on these in my SVA book with examples and diagrams. I am making those pages available to here: http://systemverilog.us/fv/local%20variable_and_or.pdf