Синтаксис SVA: разница между ##1 a |-> b и a |-> $past(b)

Question

В чем разница между этими двумя выражениями:

##1 a |-> b 

против

a |-> $past(b)

В первом будет значение b из текущего цикла будет использоваться или из следующего цикла?

Answer 1

Поскольку вы используете перекрывающий оператор импликации в обоих случаях, цикл, в котором LHS(антецедент) становится истинным, является тем же циклом, который начинается RHS(последующим). Итак, в первом утверждении, оба a а также b должно быть верно в том же цикле. ##1 просто задерживает всю операцию на один цикл.

Возможно, вы думаете о разнице между перекрывающимися и непересекающимися. Для этих простых свойств следующее эквивалентно:

a |-> b;
a |=> $past(b);