If there were no enable signal, inputReady ##N outputValid would do the job. But, how should I exclude the cycles when enable is deasserted? Is there a short solution?

1

There are 1 best solutions below

1
Sierra On

If you want to include only the portion when enable is asserted, you can just use a repetition operation. For example, if N == 4:

inputReady ##0 enable [*4] ##1 enable && outputValid;
// or
inputReady ##0 enable [*5] ##0 outputValid;
// or
inputReady && enable ##1 enable [*3] ##1 enable && outputValid;

The repetition is equivalent to N-1 delays:

enable ##1 enable ##1 enable ##1 enable

If you're building an assertion to check if-this-then-that, you could use the simple form:

inputReady |-> enable [*5] ##0 outputValid;

These are all equivalent:

inputReady |-> enable [*4] ##1 enable && outputValid;
inputReady && enable |=> enable [*4] ##0 outputValid;
inputReady && enable |=> enable ##1 enable ##1 enable ##1 enable && outputValid;