Hi, I am writing asn assertion for following requirement.
REQ: When, for the first time, (AWREADY is high and AWVALID is high and LINE_COUNT is 1), store the value of AXI_ADDR to addr0. After some clock cycles, when, for the first time, (AWREADY is high and AWVALID is high and LINE_COUNT is 2), store the value of AXI_ADDR to addr1. The difference between addr1 and addr0 should always be equal to the value = 40’h5000 that is programmed in another register (REG_STRIDE).
a |-> ##[0:$] b |-> c;
1) Here you have 2 antecedents;
>>>> "a" is antecedent for the property ##[0:$] b |-> c;
>>>> ##[0:$] b is the antecedent for the property c
2) For the property (##[0:$] b |-> c) to succeed, it is necessary that
all threads of antecedent (##[0:$] b) be tested, and that all of those threads
succeed vacuously or nonvacuoulsy. In essence, that property (##[0:$] b |-> c)
cannot succeed (because of the 0:$), it can only fail.
3) Two options for you:
Instead of (a |-> ##[0:$] b |-> c) // BAD STYLE, cannot succeed
write in in one of the following forms:
a |-> first_match(##[0:$] b) |-> c; // property can succeed or fail, option 1
a |-> first_match(##[0:$] b) ##0 c; // property can succeed or fail, option 2
I prefer option 2/
Below is my recommendation for you.
property REGMODE_STRIDE;
logic [39:0] addr0;
logic [39:0] addr1;
logic [39:0] addr2;
@(posedge tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.I_SENSOR_RX_REGBANK.CLK)
((tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.I_SENSOR_RX_REGBANK.SRX_LINE_COUNT[0] &&
tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.SRX_AXI_AWVALID &&
tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.SRX_AXI_AWREADY),
addr0 = tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.SRX_AXI_AWADDR[39:0]) |->
first_match(## [0:$] ((tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.I_SENSOR_RX_REGBANK.SRX_LINE_COUNT[1] &&
tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.SRX_AXI_AWVALID &&
tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.SRX_AXI_AWREADY),
addr1 = tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx.SRX_AXI_AWADDR[39:0])) ##0
((addr1 - addr0) == 40'h5000);
endproperty
Thanks for your reply. When I run your suggested code, though I get pass occurrences (4 times), I still get the violations (486).
“assert_macros.sv”, 187: .REGMODE_CHECK8: started at 57943712000fs failed at 58022120000fs
Offending ‘repeat or delay’
“assert_macros.sv”, 187: .REGMODE_CHECK8: started at 57792242000fs failed at 58022120000fs
Offending ‘repeat or delay’
“assert_macros.sv”, 187: .REGMODE_CHECK8: started at 57729872000fs failed at 58022120000fs
Actually my objective is to check the addr1 - addr0 = 40’h5000 only for the first time when Line Count becomes 1->2 combined with first rising edge of AWVALID and AWREADY. I don’t need to check throughout. Also, it can’t be given in number of fixed clock cycles as CLOCK freq varies b/w 550 MHz and 600 MHz at which operation is happening. Please suggest. Thanks.
Line Count becomes 1->2: Your code uses one bit only RX_LINE_COUNT[0], LINE_COUNT[1]
But LINE_COUNT[1] includes the value 2 and 3, not what you may want.
Your code is hard to read because of the paths. How about using the `define to make the code more readable?
" first rising edge of AWVALID and AWREADY" add this
`define path tb_sensor_rx_top.i_tb_sensor_rx.i_sensor_rx
/* Actually my objective is to check the addr1 - addr0 = 40'h5000 only for the first time
when Line Count becomes 1->2 combined with first rising edge of AWVALID and AWREADY.
I don't need to check throughout. Also, it can't be given in number of fixed
clock cycles as CLOCK freq varies b/w 550 MHz and 600 MHz at which operation is happening. */
property REGMODE_STRIDE;
logic [39:0] addr0;
logic [39:0] addr1;
logic [39:0] addr2;
@(posedge path_k.CLK)
((`path.I_SENSOR_RX_REGBANK.SRX_LINE_COUNT[1:0]==2'b01 && // <-----
`path.SRX_AXI_AWVALID && `path.SRX_AXI_AWREADY),
addr0 = path.SRX_AXI_AWADDR[39:0]) |-> first_match( ##[0:$]
(`path.I_SENSOR_RX_REGBANK.SRX_LINE_COUNT[1:0]==2'b10 && // <----
$rose(`path.SRX_AXI_AWVALID && `path.SRX_AXI_AWREADY)), // <----
addr1 = `path.SRX_AXI_AWADDR[39:0]) ##0
((addr1 - addr0) == 40'h5000);
endproperty
So LINE_COUNT is a 32 bit variable but I figured out that I don’t have to consider all of that.
For LINE_COUNT[0] = 1 the value of Line count is 1. when LINE_COUNT[1] = 1 the value is 2.
In between these 2 events (line count getting 1 → 2) there are many instances when AWREADY and AWVALID become high.
When LINE COUNT is 1 and at the first occurrence of AWREADY and AWVALID both getting high, there will be some address value in the AWADDR bus. I have to poll/read that value and store.
After some clock cycles, when LINE COUNT is 2 and at the first occurrence of AWREADY and AWVALID both getting high, there SHOULD be some different address value in the AWADDR bus, as per the specs. I have to poll/read that value and store in a different variable. This is what I have to check. The difference in the value between two stored addresses happens due to a user PROGRAMMED value in a register in the DUT.
The DUT works on random clock frequency so it is difficult to tell exact numbers of clock cycles between LINE COUNT 1 → 2.
In reply to Amit Kumar Mishra:
“when LINE COUNT is 2 and at the first occurrence of AWREADY and AWVALID both getting high”
Sounds like you need to tune the assertion to the requirements. What you seem to be saying is that count==2 and then some cycles later rdy&&vod rises. The way it is Witten count ==2 and the valids are on the same cycle.
Do what you need to do with the address range, 1, 2, 1:0.
I commented on the structure.
BTW, à good way to debug an assertion is to
reverse engineer the assertion to the requirements that it expresses,
write the requirements in English, separately from the assertion,
check the waveforms to understand the failures.
do à design review of the assertions and requirements with colleagues.
So far, you should have a better understanding of the assertion structure, the need for the first_match, the use of [->1], and the clocking scheme.
Tune the assertion to your needs.
Ben systemverilog.us