Add assert IR op and tie to DSLX fail!

[dkillebrew-g]

fail! should become a Verilog assertion (that fails when evaluated, i.e. the assertion is always false), so that when DSLX is converted to Verilog, the programmer's desired semantics are carried into Verilog simulations.

[meheff]

Hijacking this issue for more general support for fail throughout XLS.

IR level: add a fail_if op with following form: fail_if(token, cond, message="...")

Interpreter/JIT: Add support for raising error at runtime.

Codegen: Initally lower to SystemVerilog assert: assert(condition) else $error(message) Functionality can be extended to include pluggable options for how to generate project-specific assert forms (e.g., macros).

[dkillebrew-g]

add a fail_if op

I think Chris and I discussed fail_when and fail_unless extensions to fail. Please check with @cdleary

[meheff]

The IR will only have one variant and not its negation. DSLX frontend may have multiple forms (fail, fail_when, fail_unless, etc) which then map to the single IR operation. Filed https://github.com/google/xls/issues/290 for the DSLX issue.

[dkillebrew-g]

Ah, I see.

[meheff]

One more change of direction for this issue. After some discussion I think we want three forms of error/assert/fail related ops in xls: assert (raises error during interpretation/simulation), assume (declares assumption the optimizer can take advantage of), and fatal (generates some hardware for error handling). This issue is about addding assert ot the XLS IR and lowering it to SV assert.

[meheff]

Assigning to leary as he is working on the DSLX frontend part.

[cdleary]

Status update here with some design notes.

Last week I was adding tokens to the frontend (as a type-keyword, type in the type system, something we know how to IR emit, etc): https://github.com/google/xls/commit/dbd4eaf76152f71075f26c9a0d9ba2a4467abd74 https://github.com/google/xls/commit/32927a0b3216e25e7259e7b3c43af8a05324ae54 https://github.com/google/xls/commit/b240b4c83b325e3ec951df29053a56eafe859d26

The conceptual basis for the work started there was "it's nice to be able to have constructs at the language level that map fairly 1:1 with the constructs that are available in the IR". In some sense the DSL is a syntax that's got a bunch of conveniences vs typing in IR text directly, as the latter is more verbose and certainly missing some useful "meta facilities" like parametric instantiation, and desugarings, i.e. for function-based loop bodies, that kind of thing. That work on token plumbing will likely continue to be useful for things like send/recv where we want to explicitly sequence the threading of the "network I/O ops" via token-based dependencies.

However, for assertions, folks on the team noted that if we could automatically thread token control to the assertions it'd be convenient and probably more like what you'd expect (since you're not so concerned with sequencing of assertions like you are with send/recv). We're effectively choosing which parts of an effect system to keep under the covers (assertion effects) and which parts to expose (send/recv sequencing effects) when everything is sea of nodes with effect sequencing tokens to tie them into the dataflow computation described "at the bottom" (the XLS IR level). Assuming procs have a superset of function capabilities where they can also do send/recv I/O, but assertions can be done in otherwise pure functions as an asynchronous "sideband" side effect that doesn't need any precise behaviors with respect to the program's properties (like an asynchronous fatal), there are at least a few considerations there:

• We may need to tie in the implicit token threading with any explicit token threading (if the need arises for that in non-procs for some other sort of effect) down the road -- side effects must always be tied into the dataflow computation in our current model, vs needing explicit effect tracking (this was a nice simplifying design decision in XLA HLO we're trying to learn from by carrying forward)
• If there's a scenario where retaining the predicates for use in assertions may have some cost, we may want to be able to eliminate them via some tooling request like a flag (e.g. imagine lower layer tooling can't DCE the assertion support code entirely, that is, the code that ends up computing the assertion's predicate -- we may want to ensure it's eliminated by doing it ourselves at the XLS IR level)

DSL implementation wise and user-experience wise, the way we tend to elide / avoid effecting things occurring is via a notion of "control structures" in the program description. Ultimately what looks like guarding control to human users are actually just implicit dataflow predicates; e.g. in an everything-eagerly-evaluated world match is really a selector that computes all its arms and uses a predicate to do the selection. Selection predicates are conceptually used for preventing "unwanted side effects" from propagating, e.g. "I didn't select that match arm but if I had it would have triggered an assertion -- the fact predicate p that selects it was untrue means I quash (an assertion I would have otherwise made if it were selected)".

Consider:

fn f(x: u32) -> u32 {
  match x {
    u32:42 | u32:64 => x + u32:1,
    _ => fail!(x)
  }
}

In Verilog we really want the wildcard arm to lower to something near:

assert(x == 42 || x == 64) else $fatal("Assertion failure via fail! @ test.x:4:10");

(Which support landed for in https://github.com/google/xls/commit/b7e3c7772b1a36c6bb599413b286b538b82ebb30 via XLS IR). But obviously in that control path there's nothing that explicitly says it's guarded by that condition. We need a way to take a program point in IR conversion (the place where we encounter the fail! builtin) and ask what its implicit guard predicate is, and use that condition for the XLS IR assertion.

Control-esque AST constructs for conversion include: Match, Ternary, For, and Invocation. We'll likely want a pre-pass to identify which functions want a token for sequencing assert effects (which probably amounts to a very simple effect inference) so that we can inject the token parameter into those functions at IR conversion time.

[cdleary]

TL;DR is (I realized) when we try to say "well assertion failures are asynchronous concurrent failures" we'll get arbitrary failures reported first (at the IR interpretation or codegen level), which may look counter-intuitive to the user from the apparent program flow. It's something to consider since users are likely to want to test that exactly one "first encountered" failure is reported; e.g. from the Verilog simulation. Right now it'd be possible to test "one of the related assertion failures definitely triggers". (Anything we push under the hood we're more responsible for than if users token-thread the sequencing themselves, where it's, as a result, more clear what concurrency they've oped into -- some of this comes from trying to push sequencing under the hood of the DSL's IR conversion for the first time.)

Note how we thread tokens for "peer" fail! that are present within a conceptual scope; as described they would be unordered due to the "asynchronous, predicate based" nature of how we intend to implement these assertions; e.g. in

fn f(x: u32) -> u32 {
  let _ = fail!(x);
  fail!(x+u32:1)
}

You wouldn't know which fail! would trigger because a token would thread from the function entry to both fail!s concurrently. Even if there was an apparent data dependency:

fn f(x: u32) -> u32 {
  let y = fail!(x+u32:1);
  fail!(y)
}

Compiler is within its rights to avoid the apparent data dep by cloning/substitution:

fn f(x: u32) -> u32 {
  fail!(x+u32:1);
  fail!(x+u32:1)
}

In which case we're clearly back to the "no defined order between concurrent operations" property of the first example. As with testing/expectation of concurrent side effects in any environment, you'd need expectation code to note any of the fail! triggering could be possible.

A related note, a match's arms /will/ have logically disjoint conditions, but the "astonishment" there would come from the fact that one failure that dominates another still may not be reported first:

fn f(x: u32) -> u32 {
  fail!(x);  // dominates
  match x {
    u32:42 => fail!(x);
    _ => x
  }
}

Consider when this is invoked with the value 42: two failures would be "active" in that invocation (their predicates could cause the assertion to fire) but the one that dominates is not necessarily the one that's reported because in the proposal above we'd make them all concurrent.

If we want to more strictly sequentialize it (which would likely be the less astonishing behavior per principle of least astonishment :-) some options are a) we could thread a token down the various control paths (in which case we've effectively created a CFG out of tokens, which seems non ideal just in terms of complexity but probably fine, just use AfterAll for joins at merge points in the apparent control flow) or b) collect all the "assertion should fire" predicate bits and use the moral equivalent of a one-hot-select to strictly order their reporting in the assertion failure, or equivalently c) add in a "not any of the previously observed assertions have fired" in the assertion predicate, but that's likely to look gnarly in the generated Verilog.

Since we're trying to enable these automatically-generated-assertions-via-fail! for some soon-upcoming DV activity I think maybe the "one of N assertions will definitely report" will be ok for a first cut, and we can rework our tests for more explicit sequentialization-of-fired-assertion testing once we have soak on the basic "they fire if the condition is wrong" which is the important MVP. :-)

[cdleary]

Just a note that the way it's being done, every function that transitively contains a fail! takes a token and "is activated predicate" as a first arg. We'll give the "is activated predicate" some special name with a leading double underscore, like perhaps __activated and the backend part of the compiler flow (say opt onwards) can tie it to true for the entry function, and codegen will end up dropping the token param.

So effectively, transitively having a fail! implicitly changes your calling convention (which seems to make sense).

[cdleary]

Just a small design note on the required function signature transform here; imagine we have entry([tok, bool], T...) -> [tok], U where the braces indicate what we're implicitly inserting -- we can bump the parameters arity by 2, but we have to tuple the output since the DSL is single-valued return. So if entry calls subroutine([tok, bool], P...) -> [tok], Q then entry has to, in its IR conversion, unpack the resulting (tok, Q) typed tuple and use the tok (from subroutine) in the AfterAll that joins all the assert control, and use the Q typed value as the result value for the invocation.

[cdleary]

Realized two more things to consider:

• Zero-trip-count-loops with fail! inside: we can mitigate this by asking "is the range zero" as part of the predicate when emitting unoptimized IR. Might be good to eventually constant fold that one into the IR evaluator to avoid the predicates being more "crufty"/complex in the common case where the trip count is not zero, but we'll want to expose an EvaluateToConstant() like we had in XLA so the IR converter can attempt to constant fold arbitrary things that have been enqueued into the IR package/function. For now we can just make the dynamic predicate always.
• CountedFor loop transform: we can't just add the token as a loop invariant argument to the (anonymous, desugared) body function, so we have to tack it on to the accumulator. Instead of desugaring a body function of the form f(ivar, accum, invariant_args...) -> accum I believe we can desugar to f(token, ivar, accum, invariant_args...) -> (token, accum)

[cdleary]

Should be done now, thanks to @RobSpringer for getting us through the tough part at the end (flipping the flag to true by default and all the accommodations needed for that in existing code / tests / systems).