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

Do you mean "expose them from the prelude"?

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...

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.

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.

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.

Sounds good, will do.

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.

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.

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?

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.

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.

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.

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

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.