cxxrtl: Implement $assert checks

[povik]

This is the result of piecing something together for my downstream needs. I am curious to hear how it fits into @whitequark's plans with CXXRTL.

Related: #2431

[whitequark]

CXXRTL_ASSERT is for internal constraint violations. User assertions need to be collected similar to $display cells into a buffer that can be read via the C API.

(The $display cell needs changes too, but the current situation there is very useful. Here I do not think it is appropriate to merge.)

[povik]

Sure, and what do you think of adding the extra check() step?

[whitequark]

Not a fan either. The pure eval/commit based simulation model is quite elegant and I don't think having $assert should change it any more than having $display does.

[povik]

Well, but do you see a way to reasonably implement the user assertions checks within the eval/commit model when there are feedback arcs? As I see it the assertions should only be checked once the circuit converges.

[whitequark]

As I see it the assertions should only be checked once the circuit converges.

Why is the same not true about $display? They are both side effects.

[povik]

I assume you mean $print which can be conditioned on clock edges, $assert cannot. If it cannot be guaranteed to be checked once the circuit converges (in the CXXRTL sense) then I don't think there's any sane way to use the assertion cells at all. There are no guarantees.

[whitequark]

I assume you mean $print which can be conditioned on clock edges, $assert cannot.

Oh. I for some reason thought $assert can be. In that case the solution is $assert_v2 which can be, not changing CXXRTL.

[povik]

I will raise that at the next Yosys dev meeting.

[whitequark]

Thanks! Note that I am also making an effort towards implementing CXXRTL 2. It will have a different evaluation model not based on a eval/commit loop the way CXXRTL 1 is. So check would not work there.

(Once CXXRTL 2 lands, the plan is to fully deprecate CXXRTL 1.)

[povik]

I assume you mean $print which can be conditioned on clock edges, $assert cannot.

Oh. I for some reason thought $assert can be. In that case the solution is $assert_v2 which can be, not changing CXXRTL.

So we have discussed this on today’s dev JF. The consensus was that we are fine with having assertion cells with the semantics being that the cell inputs are only sampled once the circuit converges, so that there’s no need for a new version of an assertion cell. What would be the argument against that? Why shouldn’t CXXRTL, even in version 2, bend to that requirement?

[whitequark]

Why shouldn’t CXXRTL, even in version 2, bend to that requirement?

Does "because I lead the design of CXXRTL and I veto that choice" work for you?

[povik]

Uh, not really, I was interested in a technical argument. So that I understand why the “once the circuit converges” sampling semantics is broken so that it warrants a new cell, which I understand is your position.

[whitequark]

Uh, not really, I was interested in a technical argument.

Well, you were requesting someone else "bends" to your instructions, which isn't a technical argument either.

[povik]

I don’t think I was. I am really only trying to find out why the definition of the assertion cell as it is now is something unreasonable, so that CXXRTL 2 will have hard time “bending” to it. Though maybe I assumed wrong what you meant when you say the check step from this PR wouldn’t work there.

[whitequark]

Ah yeah. Let me elaborate on that.

The CXXRTL simulation model is fundamentally resting on the pillars of its two actions: eval and commit. This isn't an artifact of the current implementation but is something that is both of theoretical importance (it is how CXXRTL avoids races) and it is also exported in every API (the C++ API, the C API, etc). Adding a new action, if it was ever done, would have to be reflected everywhere, and it is a breaking change to the C API (for example it would mean assertions do not work when Amaranth is driving the simulation through cxxsim). While the step function exists, it is just a convenience (for which reason the unsigned int steps; is entirely wrong; #3995) and calling eval/commit directly is a correct use of the API, which step itself should respect.

If you are adding support for a new cell, even in CXXRTL 1, it needs to fit into the eval/commit unless you have a very good motivation, starting with the fundamentals of the CXXRTL simulation model, that this is impossible or profoundly undesirable. $print was adapted to it for this reason. CXXRTL is not "the Yosys simulator" even if it ended up living in the Yosys repository for convenience (it goes to great lengths to be Yosys-independent as much as possible) and the mere fact that a Yosys cell has an interface not permitting that is an insufficient motivation. If Yosys is unwilling to add a new cell then a transformation shall be added in CXXRTL to adapt the existing Yosys cell to the interface it should have had (probably by looking at the clock domain of the EN input or something like that).

In addition to that, I'm not actually sure the notion of "whenever comb signals settle" is especially well defined, particularly when an external simulator harness is involved rather than just repeated calls to the step function, and my comments re: CXXRTL 2 (which is in flux but thus far seems slated to have a more event-driven design) refer to that.

[povik]

OK, so the gist of the matter seems to be that the simulation model that exposes evaluation of combinational cells to transitionary glitch states is so ingrained into the design, and maybe what's more important into the interface of CXXRTL, that the cost of implementing the "converged sampling" semantics directly is too high to bear.

On a more general level, $assert is being peculiar and gets by with being peculiar because it's not meant for physical implementation. Otherwise those semantics would be basically impossible. But then it's a hindrance for a simulator where the simulator exploits what's true of a physical cell, because that works on bulk of the design and there are gains to be made this way. Making $assert not special so that it can be treated on equal terms with other cells would be the argument for $assert_v2, right? There would be a clocked version of the cell, which would cover good chunk of occurrences of HDL assertions, and could be readily supported in CXXRTL, and I assume there would need to be an unclocked version with the semantics of the old cell, just because some HDL constructs cannot be lowered any other way, at least not directly. This latter point I am not that sure of, it's a guess. There could be a pass to transform the unclocked cell into the clocked cell where possible with some analysis of the design, similar to what you suggest might be a CXXRTL-level transformation if we are without $assert_v2.

If Yosys is unwilling to add a new cell then a transformation shall be added in CXXRTL to adapt the existing Yosys cell to the interface it should have had (probably by looking at the clock domain of the EN input or something like that).

Thinking out loud: if you have an always @(posedge clk) if (...) assert (...); construct in Verilog, that's lowered to an $assert with both EN and A being fed by flip-flops, so that could be the typical pattern to support. The question with nonobvious answer to me is how far the transformation should go in dealing with other patterns so that the end result isn't brittle, even if we opt to only support some specified subset of kinds of HDL assertions.

[whitequark]

OK, so the gist of the matter seems to be that the simulation model that exposes evaluation of combinational cells to transitionary glitch states is so ingrained into the design, and maybe what's more important into the interface of CXXRTL, that the cost of implementing the "converged sampling" semantics directly is too high to bear.

This is an accurate summary, thank you.

On a more general level, $assert is being peculiar and gets by with being peculiar because it's not meant for physical implementation. Otherwise those semantics would be basically impossible. But then it's a hindrance for a simulator where the simulator exploits what's true of a physical cell, because that works on bulk of the design and there are gains to be made this way.

I actually want physical implementation of $assert to be possible as a part of the product we're shipping at @ChipFlow, so that's something we'll have to look into either way.

CXXRTL itself, as you've realized already, is a synthesis target at its heart, not a simulation target, hence all these difficulties.

Once again thank you for an accurate summary.

Making $assert not special so that it can be treated on equal terms with other cells would be the argument for $assert_v2, right?

Yes.

There would be a clocked version of the cell, which would cover good chunk of occurrences of HDL assertions, and could be readily supported in CXXRTL, and I assume there would need to be an unclocked version with the semantics of the old cell, just because some HDL constructs cannot be lowered any other way, at least not directly.

Yes. In case of the $print cell and anything else where the designer can be "doing something's weird" (latches that depend on delta cycles for example) CXXRTL's answer is that it's undefined and if you happen to like the results, great, if you don't, you need to rewrite the input netlist to conform to the synthesis rules of the target, as always. The $assert* cell(s) can be treated that way too, and this is what I would ordinarily expect.

There could be a pass to transform the unclocked cell into the clocked cell where possible with some analysis of the design, similar to what you suggest might be a CXXRTL-level transformation if we are without $assert_v2.

Yep, sounds good to me.

Thinking out loud: if you have an always @(posedge clk) if (...) assert (...); construct in Verilog, that's lowered to an $assert with both EN and A being fed by flip-flops, so that could be the typical pattern to support. The question with nonobvious answer to me is how far the transformation should go in dealing with other patterns so that the end result isn't brittle, even if we opt to only support some specified subset of kinds of HDL assertions.

As far as I recall (it's been a while since I looked) for $print the decision is done in the frontend. Seems like it would be easiest to do it in the frontend for $assert too--maybe add an attribute or something.

[whitequark]

Is obsoleted by #4128.