[RFC] Clarify the meaning of Past and friends when there is no lexically enclosing scope

[cestrauss]

I would like to propose an alternative to the solution being discussed on #526. In order to not derail that discussion, and since it's somewhat opposite to it, I opened this RFC.

To recapitulate, in #526 (comment), @whitequark said:

Semantically, Past generates a register chain clocked by the domain of the lexically containing expression. I.e. m.d.<domain> += (... Past(...) ...) clocks the FFs implicit in the Past expression with <domain>'s clock.

In #526 (comment), I pointed out:

This model seems somewhat broken by statements like with m.If(Past(...)):, where there is no lexically containing expression.

The model being discussed in #526 is:

I think the best course of action is to ditch the current behavior where the domain is magically lifted from the lexically containing statement, make it default to sync, issue a deprecation warning during the 0.4 cycle when a call to Past is detected where the behavior would otherwise silently change.

Also,

I think we could perhaps define Rose(sig, domain="comb") to mean "rose asynchronously". It seems reasonably intuitive and would be mapped to the global clock without tying us to the way Yosys calls/implements it.

This RFC takes the point of view that the current model can be fixed, with some clarifications.
Basically, it's:

1. Semantically, Past generates a register chain clocked by the domain of the lexically containing expression. I.e. m.d.<domain> += (... Past(...) ...) clocks the FFs implicit in the Past expression with <domain>'s clock.
2. In case there is no enclosing lexical scope, use the domain parameter, e.g. with m.If(Past(..., domain=<domain>)):
   2.1. In case the domain is not specified, assume sync.
3. If the there is a domain mismatch, assert a CDC violation (see Require signals crossing clock domains to be explicitly marked #6).
4. Asynchronous signals can be sampled when the enclosing domain is "comb", or by explicitly passing domain="comb".

As for "magically lifting the domain from the lexically containing statement", I would argue that it is consistent with the way assignments already work in nMigen.

Upsides:

1. Avoids repetition:m.d.<domain> += Assert(Past(...)) instead of m.d.<domain> += Assert(Past(..., domain=<domain>))
2. Consistent with the way Assignments work in nMigen: m.d.<domain> += [ a.eq(b), Assert(Past(c)) ]
3. Avoid CDC, like m.d.<domain1> += Assert(Past(...,domain=<domain2>))

Downsides:

1. Non-uniform behavior, depending on the presence or absence of a lexical scope.
2. Potential to create CDC due to domains being implicit..

[cestrauss]

Actually, Upside n. 1 above should read:

1. Avoids some typing: m.d.<domain> += m.d.comb += Assert(Past(...)) instead of m.d.comb += Assert(Past(...,domain=<domain>))
   There is no repetition involved.

[RobertBaruch]

Personally, I agree with whitequark@'s mental model that Past is something that samples a signal in a given domain, not necessarily the signal driver's domain. Consider:

x = Signal(8)
m.d.clk1 += x.eq(x+1)

So we can have:

m.d.comb += Assert((Past(x, domain="clk1") + 1)[:8] == x)

That is, no matter what formal verification step I'm on, and no matter how that relates to clk1, I assert that x is equal to the past value of x, relative to clk1, plus 1.

The proposed syntax would be:

m.d.clk1 += Assert((Past(x) + 1)[:8] == x)

To me, this has similar syntax to:

m.d.clk1 += x.eq(x+1)

Now, I can always refactor:

next_x = Signal(8)
m.d.comb += next_x.eq(x+1)
m.d.clk1 += x.eq(next_x)

Now consider again the proposed syntax for Past:

m.d.clk1 += Assert((Past(x) + 1)[:8] == x)

In a similar way, I can also refactor:

compare_x = Signal(8)
m.d.comb += compare_x.eq(Past(x) + 1)
m.d.clk1 += Assert(compare_x == x)

But this is now wrong, because the syntax proposes that Past by default uses the sync domain, and that would fail here. Thus, my refactor is inexplicably incorrect, in that it works for everything except Past and friends. This is too much of a cognitive load, and in my opinion, error-prone.

[whitequark]

I concur. To add to (or perhaps rephrase) what @RobertBaruch said, I think that it is important that any subexpression can be replaced with either (a) Python variable containing that subexpression, or (b) fresh Signal of the same shape that is combinatorially assigned that subexpression.

[RobertBaruch]

I propose this RFC be closed, since it has fatal issues, or the original proposer should modify the proposal to eliminate the problems.

[cestrauss]

Sure. Thanks for the insights and feedback.

I admit I don't really have a use case for multi-clock formal verification, and will respectfully defer to the opinion of those that do.