What are different types of temporal Operators in SystemVerilog

SystemVerilog
,
1

Hi All,

While searching for SV Interview questions I came across a question

“What are different types of temporal Operators in SystemVerilog“

I understand that concurrent assertions are temporal in nature (i.e which consumes time).

Does this mean that all operators used in concurrent assertions classify as temporal operators ?

Eg: |→ (overlapping implication) , |=> (non-overlapping implication) , Clock delay ## , Clocking event @(posedge clk).

Are all of these considered as temporal operators ?

On searching for “temporal operators“ in LRM I observe the following

F.3.4.3.8 Derived unbounded temporal operators
— (always p) (p until 0).
— (s_eventually p) (not (always(not p)).
— (p s_until q) ((p until q) and s_eventually q).
— (p until_with q) ((p until (p and q)).
— (p s_until_with q) ((p s_until (p and q)).

F.3.4.3.9 Derived bounded temporal operators
— (s_nexttime p) (not nexttime not p).
— (nexttime[0] p) (1 |-> p).
............................
2

The answer to this question depends on the context.

In the context of a SystemVerilog concurrent assertion, it refers to a sequence or property operator that operates over multiple clock cycles. This would exclude all boolean and arithmetic operators.

In formal linear temporal logic (LTL), it represents an operator that specifies a condition with a past and a future condition. So always, nexttime, until are temporal operators, but implication and ##delay are not.

In dynamic simulation, event controls (#delay, ~@(), wait() could be considered temporal operators.

3

Hi Dave,

A few questions

In the context of a SystemVerilog concurrent assertion, it refers to a sequence or property operator that operates over multiple clock cycles. This would exclude all boolean and arithmetic operators.

Would this mean that both implication operators , clock delay ##delay are temporal operators ?

assert property( seq_exp1 |→ ##2 seq_exp2 );  // |-> ##2 operates over multiple clocks

In formal linear temporal logic (LTL), it represents an operator that specifies a condition with a past in a future condition.

I believe you meant “with a pass in a future condition“

So always, nexttime, until are temporal operators, but implication and ##delay are not.

Could you please elaborate on the last part ? Why is it that ##delay isn’t considered temporal ?

4

I meant to say “with past and a future condition”

I wouldn’t get too bogged down in the technical terms. Instead, focus on understanding the functionality and meaning of these operators.