In reply to Amit Kumar Mishra:
Comments:
- 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
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy