Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
cestrauss opened this issue Nov 8, 2020 · 5 comments
Closed

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

cestrauss opened this issue Nov 8, 2020 · 5 comments
Labels
design

Comments

@cestrauss
Copy link

cestrauss commented Nov 8, 2020 •
edited

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
Copy link
Author

cestrauss commented Nov 8, 2020 •
edited

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
Copy link
Contributor

RobertBaruch commented Nov 8, 2020 •
edited

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
Copy link
Member

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
Copy link
Contributor

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

@cestrauss
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
design
Milestone
No milestone
Development

No branches or pull requests
3 participants
@whitequark @RobertBaruch @cestrauss