In reply to rohitk:
// I need to write an assertion to catch response of a request if request is asserted after certain control signal.
// There are two control signals "start" and "eop", for every start there is an eop at the end of the process.
ap_start2eop: assert property(@(posedge clk) $rose(start) |-> strong (##[1:$] $rose(eop)));
// [Ben] Wirte short assertions when you see them fit.
// If "request" is asserted after start and before eop, the "response" shall come only after "eop" and not before.
// I have come up with an assertion which works also, but I am not convinced that this is the best way to achieve this,
// can someone help me how do I make it better. Following is assertion I am using right now:
property check_rsp;
@(posedge clk)
$rose(start) |=> req[->1] |-> strong(
first_match(!ack [*0:$] ##1 $rose(eop) ##1 $fell(eop)) ##[0:10] (ack == 1) );
endproperty
// [Ben] WIth $rose(start) |-> req[->1] you state that req CAN OCCUR in the SAME cycle as start.
// I think you want to say that req can occur any cycle AFTER start, thus you need to write
// $rose(start) |=> req[->1]
// [Ben] If ack NEVER occurs, but eop does, the assertion the way yo have will not fail because of the !ack [*0:$]
// (!ack [*0:$] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) is same as
// (!ack [*0 ] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) or
// (!ack [*1] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) or
// ..
// (!ack [*n] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) // n==infinity
// THUS, you need the first_match()
// [Ben] On the "strong", you may want to qualify that for the whole consequent
// [Ben] Avoid writing unnecessary parenheses, like ($rose(start)), $rose(start) is sufficient
ap_check_rsp: assert property(check_rsp)
$display("assertion passed");
else
$display("assertion failed");
// [Ben] Add labels.
// FOr assertions that are not reused and that do not have local variables, avoid writing a separate property declaration.
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 0-9705394-2-8
- 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