Got this question: What is the best way to write an SVA to check a valid signal remains asserted for exactly one cycle? Implication |=> or delay ## operator?
[Ben]
cond |-> sig ##1 !sig;
// if the condition is the $rose(valid) then
$rose(valid) |-> ##1 ! $valid; // $rose means that valid ==1
// NOTE
// Instead of "|-> ##1" you can use "|=>", but keep in mind that they not the samething.
// |-> is followed by a property. The ##1 is followed by a sequence
// |=> is equivalent to ##1 |->
// I generally prefer the |-> ##1 because it reads as "implies that at next cycle ..."
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.