In reply to bhajanpreetsinght:
@(posedge clk) $rose(c) |-> ((a||c) throughout(c==1)) until (c==0)
which also can be rewritten as
@(posedge clk) $rose(c) |-> ((a||c) && (c==1)) until (c==0)
it can be further rewritten as
@(posedge clk) rose(c) |-> ((a||c) && (c==1))[*0:] ##1 (c==0)
I suggest that you try various tests with different assertions; this will help in your
understanding of these operators. Also, read my paper Reflections on Users’ Experiences with SVA, part 2
Addresses the usage of these four relationship operators: throughout, until, intersect, implies
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog