[SV] [FIRRTL] Add intrinsics for sampled value functions

[unlsycn]

In Chisel we are seeking for intrinsics for sampled value functions like $rose and $stable to use with LTL and I think it should be lowered to the sv dialect in CIRCT.

I noticed that there are existing mappings of these functions to seq and comb in the LTL documents which seem to be used for arc and maybe they should be lowered to these Ops of sv in the future.

Specific functions to be added contains:

• $sampled
• $rose
• $fell
• $stable
• $changed
• $past

I'm not that familiar with CIRCT hence please let me know if there are any misconceptions.

[sequencer]

I think these functions relate to the SVA but not a part of LTL, these are not defined in LTL However we need to use it for Sequence construction to design AIP. A similar intrinsic is isX, which sounds like a sample to current cycle, but the sampled value functions need to observe previous cycle, aka $sampled x or $past x 1 and most of these behavior can be mocked by $past, e.g. $sampled x == $past x 1 $rose x == (not ($past x 1)) && x $fell x == ($past x 1) && (not x) $stable x == ($past x 1) nor x $changed x == ($past x 1) xor x

So if doing these implementation, I think a simple solution is defining $sampled intrinsic, matching the canonical AST and convert them to the sampled functions in the SVA.

I personally would like to introduce this API to chisel.ltl to reduce the user understanding burden, WDYT? @fabianschuiki, @jackkoenig, @seldridge

[fabianschuiki]

Summarizing some side-channel discussion with @sequencer: Looks like $sampled is different from the other $past-based expressions and we can probably just ignore it.

We can express all other functions based on $past as pointed out by @sequencer, so the only thing CIRCT needs is a concept of $past. The LTL emitter could then pattern match the different $past invocations and substitute a more compact $rose or other function instead.

It looks like $past behaves like a register, providing an older value relative to a clock (implicit or explicit). We could check in the LTL sequence emitter if a value is defined by a seq.compreg or seq.firreg with the same clock as the sequence, and if it is, emit a $past(<reginput>) instead.

[sequencer]

Thanks @fabianschuiki's suggestion! @unlsycn please try to implement the these ops in Chisel with the emulation of RegNext directly with Chisel, it can still live in chisel.ltl package, but remember to guard the Reg construction in the corresponding Verification Layer, after we get it merged, that won't block our progress on the AXI/CHI AIP developing, and you can start to contributing CIRCT for doing the pattern matching as @fabianschuiki proposed to get a better SystemVerilog Assertion with these ops.

[fabianschuiki]

I'm happy to help if you run into trouble with the pattern matching during SystemVerilog assertion emission!

[jackkoenig]

It looks like $past behaves like a register, providing an older value relative to a clock (implicit or explicit)

please try to implement the these ops in Chisel with the emulation of RegNext directly with Chisel

What is the behavior of $past at time 0? Do we need any special consideration for that when emulating it with RegNext or is the implicit guarding of all SVA with "disable before reset" sufficient?

[fabianschuiki]

Good point! IEEE 1800-2017 § 16.9.3 "Sampled value functions says":

$past ( expression1 [, [number_of_ticks ] [, [expression2 ] [, [clocking_event]]] ] ) [...] number_of_ticks shall be 1 or greater and shall be an elaboration-time constant expression. If number_of_ticks is not specified, then it defaults to 1. [...] If there do not exist k strictly prior time steps in which the event ev iff expression2 occurred, then the value returned from the $past function is the default sampled value of expression1 (see 16.5.1).

Seems like $past always returns a value strictly in the past, and if there haven't been enough clock ticks in between, it returns the default value for the type of the expression you're sampling (basically 0 for two-valued types and X for four-valued types). This would match the behavior of a register that is neither reset nor randomized.

[ekiwi]

I just wanted to chime in real quick and point to the "safe-past" construct that I implemented in the original firrtl compiler. Essentially, my pass would look at the fan in of each assertion and take notice of the largest nesting of past-registers. Then it would automatically delay the assertion by that many cycles. Details are in my WOSET paper: https://woset-workshop.github.io/WOSET2021.html#article-3

Here is the old implementation: https://github.com/ucb-bar/chiseltest/blob/main/src/main/scala/chiseltest/formal/past.scala