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.

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

Export Past, Rose, Fell, etc from nmigen.hdl.ast #356

Closed
awygle opened this issue Apr 15, 2020 · 15 comments
Closed

Export Past, Rose, Fell, etc from nmigen.hdl.ast #356

awygle opened this issue Apr 15, 2020 · 15 comments
Labels

Comments

@awygle
Copy link
Contributor

awygle commented Apr 15, 2020

Nothing about Past, Rose, Fell, etc is formal-specific but currently these utility functions are only exported (well, glob-exported or whatever Python calls this) from nmigen.asserts. It would be convenient if they were available directly from nmigen.hdl.ast.

@whitequark
Copy link
Member

whitequark commented Apr 15, 2020

They are glob-exported from nmigen.hdl.ast. That's where they're defined!

@whitequark
Copy link
Member

Do you mean "expose them from the prelude"?

@awygle
Copy link
Contributor Author

awygle commented Apr 15, 2020

I guess that's what I mean. They're not in the all list, I have to specifically go get them.

I'm bad at Python import rules...

@whitequark
Copy link
Member

Ok, so, that was actually intentional, because I didn't consider that they would be useful in normal code. (In SVA you can't use them in synthesis--in Yosys implementation of SVA you can, just like in nMigen.) And if they aren't useful in synthesis, then putting them in the prelude would have just polluted the namespace.

Do I understand it correctly that you found them useful? In things like edge detectors or FSMs, I assume? I'm essentially on board with adding them to the prelude already, but I'd still like to see the use cases you have to understand how broad their usefulness is.

@awygle
Copy link
Contributor Author

awygle commented Apr 15, 2020

Edge detectors exactly. It's not difficult to write one manually, of course, but why bother when Rose communicates the intent more clearly?

Also in my current state machine prototyping work I'm using Past to check "came-from" for on_entry triggers associated with transitions, which may or may not turn out to be The Right Way but it's something I'm doing. That's what prompted me to file this, although I've thought about doing so before.

@whitequark
Copy link
Member

Let's do this. Would you prepare a PR? When moving them to the prelude, you should add wrappers to nmigen.asserts to indicate that this module is deprecated. Then we can remove it once 0.3 is released.

@awygle
Copy link
Contributor Author

awygle commented Apr 15, 2020

Sounds good, will do.

@whitequark
Copy link
Member

It's not difficult to write one manually, of course, but why bother when Rose communicates the intent more clearly?

It also creates a more compact netlist (you get exactly one chain of registers per signal no matter how many of these operators you use).

However, there is a caveat. All of these implicitly created registers are reset_less. Do you foresee this being a problem? For example I'm not sure if this is the right thing for FSMs.

@whitequark
Copy link
Member

Actually, I think that caveat is important enough we should pause and think if this is really the right path. I'm worried about introducing a feature that will turn out to be a footgun.

The main argument in favor of Past, etc, being language features (beyond the assertion sub-language) is that they take their clock domain from the context they're used in, which is handy, and means you don't need to write sampling registers by hand. But that same convenience and concisenes could be a drawback.

@awygle
Copy link
Contributor Author

awygle commented Apr 15, 2020

Good question. My intuition would be that e.g. Rose would always output 0 immediately after a reset, which wouldn't necessarily be true if the generated registers are reset_less. I agree with pausing here for further thought.

Is there a reason they must be reset-less in the formal use case?

@whitequark
Copy link
Member

Is there a reason they must be reset-less in the formal use case?

I remember that I made them reset-less deliberately while writing testbenches for AsyncFIFO. I think that before I did so, I had an issue where the reset-ful nature of those implicit registers was hiding a bug in the reset logic by virtue of, well, resetting the testbench with the design.

@awygle
Copy link
Contributor Author

awygle commented Apr 15, 2020

Hm. I wonder if we could just add the reset_less parameter to the Rose et al objects(?). It does make sense that in formal mode, you'd want Fell if reset caused a signal to fall, for example.

Another thought is to add something like EdgeDetector(edge="pos", reset_less=False) to ast and export an alias from asserts which is Rose = EdgeDetector(edge="pos", reset_less=True) (and the corresponding for Fell).

EDIT: on further thought the above probably doesn't literally work, but perhaps something in that spirit would.

@whitequark
Copy link
Member

whitequark commented Apr 15, 2020

Hm. I wonder if we could just add the reset_less parameter to the Rose et al objects(?). It does make sense that in formal mode, you'd want Fell if reset caused a signal to fall, for example.

We could of course do that, but it seems like it would impact ergonomics either in the formal case, the synthesis case, or both, since I think the defaults for these are different.

Another thought is to add something like EdgeDetector(edge="pos", reset_less=False) to ast

Sure, we could do it in principle, but it seems like special-casing some fairly boring functionality in a way that is too specific. I thought it's OK to special-case for SVA because, well, I'm not about to invent a whole new verification sub-language and SVA seems really well-designed, so we might as well do whatever is needed to import SVA constructs wholesale. But if we're generalizing them, it seems like an issue.

@awygle
Copy link
Contributor Author

awygle commented Apr 15, 2020

We could always just not do this at all. It's really not that big of a deal to write my own edge detectors.

@whitequark
Copy link
Member

whitequark commented Apr 16, 2020

Let's not do this for now, and reconsider it if someone makes a good case for the usefulness of these operations in the prelude, and puts in work to determine the exact semantics. I think these operations is something that would be nice to have in principle, but more work is necessary to make sure we won't regret adding them.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Development

No branches or pull requests

2 participants