In reply to Bhaskar44:
Assertion fails at 5ns itself…At 5ns the CtrllerCmd changes from 3’bX to 3’b000, however I don’t understand why the assertion is triggering and failing ?
At the first posedge of clk, CtrllerCmd ==3’bX in the Prepone region, thus, your assertion fails since your property has no implication operator and is a sequence. With 3’bX that sequence fails in the first attempt.
Could I get some advice on correcting this assertion ?
I am trying to write an assertion for: When the CtrllerCmd becomes/is 3’b100, the time between the CtrllerCmd = 3’b001 should be 56 clock cycles!
The assertion I have written is:
property p2;
@ (posedge clk) (CtrllerCmd == 3'b100) ##56 (CtrllerCmd == 3'b001)
endproperty
a2: assert property (p2) else $info ("PreCharge to Activate Violation");
// When the CtrllerCmd becomes/is 3'b100, the time between the CtrllerCmd = 3'b001 should be 56 clock cycles!
ap56: assert property(@ (posedge clk) (CtrllerCmd == 3'b100) |-> ##56 (CtrllerCmd == 3'b001)) else $info ("PreCharge to Activate Violation");
// You may want to use the UVM severity levels
string tID="my module name";
ap56: assert property(@ (posedge clk) (CtrllerCmd == 3'b100) |-> ##56 (CtrllerCmd == 3'b001))
else `uvm_info(tID,$sformatf("%m : PreCharge to Activate Violation, CtrllerCmd=%b", CtrllerCmd), UVM_FULL);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- 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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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