In reply to BhaRath@Intel:
You still have some ambiguity in the English definition of the requirements, something that when translating the English into SVA clearly brings out. BTW, this is one of the nice things of SVA, it forces the user to clarify the requirements.
Specifically, you were ambiguous as to when the "then" means, SAME cycle or the NEXT cycle.
I made some assumptions for you, but you need to fix it according to your real requirements.
I also changed the name of clkreq to req.
bit clk, req, valid, force_on, force_on_ack, ack;
default clocking @(posedge clk);
initial forever #10 clk=!clk;
// 1.when req asserted I should check for valid that needs to be get asserted within 500clocks,
// then ack should get asserted IN THE NEXT CYCLE.
ap_req_valid: assert property(@ (posedge clk) $rose(req) |->
first_match(##[1:500] valid) ##1 ack);
// first_match() is needed here
// If force_on asserted then valid must be asserted IN THE NEXT CYCLE(?)
// then (##0 or ##1 ?)force_on_ack must be asserted followed IN THE NEXT CYCLE by force_on deassert,
// valid deassert, force_on_ack deassert.
ap_force_on: assert property(@ (posedge clk) $rose(force_on) |->
##1 force_on_ack ##1 $fell(force_on) ##0 !valid ##0 !force_on_ack);
// ##0 or ##1 spec is poorly defined
/* In second case when force_on asserted it will check for valid (NExt or same cycle?) ,
If valid already asserted due to clkreq it should go ahead
and check for force_on_ack assertion followed
we need to check for force_on deassertion and force_on_ack deassertion. */
ap_force_on_valid: assert property(@ (posedge clk) $rose(force_on) ##1 valid |->
##1 force_on_ack ##1 $fell(force_on) ##0 !force_on_ack);
For training, consulting, services: contact http://cvcblr.com/home
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
- SVA Alternative for Complex Assertions
- SVA in a UVM Class-based Environment
- Understanding the SVA Engine,