Better Representation of Assignments (maybe Value Summaries)

[Nikil-Shyamsunder]

Right now we use ITEs, which are straightforward for sequential merges but become very annoying when we do parallel merges (we need to tear down the ITE into what I think are value summaries, and then reconstruct an ITE after moving concretes up front).

Find a better encoding, perhaps kevins idea of Action::Assign(guard, value, dont_care_guard) as a value summary

[Nikil-Shyamsunder]

Assignment Summary IR RFC

Based on our discussion, here's the revised RFC for representing assignments in
the IR.

---

An Assign action has the following fields:

• DontCare: ExprRef // the guard for the DontCare
• Concretes: Vec<(ExprRef, ExprRef)> // (guard, expression)

The DontCare expression is just a guard for an implicit DontCare assignment.
We check the DontCare guard before checking the Concretes, and if the
DontCare guard fires we don't evaluate the Concretes.

The Concretes vector is an ordered list of boolean-evaluating guards and
bitvector expressions which should evaluate to concrete values with a left to
right preference. That is, for a vector [(p, a), (q, b), (r, c)] we assign:

• a if p
• b if (not p and q)
• c if (not p and not q and r)
• InternalAssertFalse if (not p and not q and not r)

More generally, because DontCare is checked before any concrete branch, the
effective guard for a concrete value also includes not DontCare. For example:

Assign {
  DontCare: g,
  Concretes: [(p, a), (q, b), (r, c)]
}

assigns:

• DontCare if g
• a if (not g and p)
• b if (not g and not p and q)
• c if (not g and not p and not q and r)
• InternalAssertFalse if (not g and not p and not q and not r)

For convenience, define the effective concrete coverage of an assignment as
the condition under which some concrete branch is selected. For the example
above:

effective_concretes =
  not g and (p or q or r)

This is different from the raw concrete guard coverage p or q or r, because a
raw concrete guard may be true even when DontCare has already been selected.

The individual effective concrete guards are still useful for conflict checking,
because they identify which concrete value is selected:

a selected if (not g and p)
b selected if (not g and not p and q)
c selected if (not g and not p and not q and r)

---

Assign Action Invariant

Assignments should always have an action guard of 1.

That is, assignment path conditions live inside the Assign summary itself:

Action {
  guard: 1,
  op: Assign(symbol, {
    DontCare: ...,
    Concretes: ...
  })
}

If edge contraction or lowering needs to move an assignment across a guarded
edge, it should push that edge guard into the assignment summary:

DontCare := edge_guard and DontCare
Concretes := [(edge_guard and guard, value), ...]

Non-assignment actions still use Action.guard normally. For assignments,
Action.guard != 1 is an IR invariant violation.

---

Sequential Merge Rules

Suppose we have Node A with:

Assign A := {
  DontCare: ga,
  Concretes: [(p1, e1), (p2, e2), ..., (pn, en)]
}

for DUT.in.

We want to sequentially merge Node B in, with:

Assign B := {
  DontCare: gb,
  Concretes: [(q1, v1), (q2, v2), ..., (qm, vm)]
}

for DUT.in.

Sequential merge should preserve source-order assignment semantics: the new
assignment has priority over the existing assignment. Create the merged
assignment:

Assign C := {
  DontCare: gb \/ (!effective_concretes_B /\ ga),
  Concretes: [(q1, v1), ..., (qm, vm), (p1, e1), ..., (pn, en)]
}

In essence, we force an ordering between the existing DontCare guard ga
and the new concrete assignments by negating the effective concrete coverage of
Node B. We don't need to force an ordering for the new DontCare, since it has
top priority in the assignment summary, and we don't need to force an ordering
for the new concrete assignments, since they go earlier in the vector.

This guarantees the ordering:

DontCare_B > Concretes_B > DontCare_A > Concretes_A

---

Parallel Merge Rules

Suppose we have Node A with:

Assign A := {
  DontCare: ga,
  Concretes: [(p1, e1), (p2, e2), ..., (pn, en)]
}

for DUT.in.

We want to parallel merge Node B in, with:

Assign B := {
  DontCare: gb,
  Concretes: [(q1, v1), (q2, v2), ..., (qm, vm)]
}

for DUT.in.

Create the merged assignment:

Assign C := {
  DontCare:
    (!effective_concretes_B /\ ga)
    \/
    (!effective_concretes_A /\ gb),
  Concretes: [(p1, e1), ..., (pn, en), (q1, v1), ..., (qm, vm)]
}

In essence, we are doing the same thing as in the sequential merge, where we
negate the DontCare guard gb with all the effective concrete guards from
Node A, except we do the exact same thing in reverse where we negate ga with
all the effective concrete guards from Node B. This forces a preference order
where Concretes from the other node (i.e. the other transaction) are preferred
to DontCare.

The Concrete vectors are just merged.

The important detail is that the negated coverage must be effective concrete
coverage, not just the OR of the raw concrete guards. A raw concrete guard can
be true even if an earlier DontCare or earlier concrete branch prevents that
concrete value from being selected.

For example:

Assign A := {
  DontCare: s,
  Concretes: [(q, 3)]
}

The concrete value 3 is selected under (not s and q), not under just q.
So when another parallel assignment's DontCare is suppressed by A's concrete
coverage, it should be suppressed by (not s and q), not by q.

---

Parallel Conflict Rules

Parallel concrete assignments conflict only when their effective concrete
guards overlap and their concrete values differ.

For example, if:

Assign A := {
  DontCare: s,
  Concretes: [(q, 3)]
}

Assign B := {
  DontCare: false,
  Concretes: [(r, 4)]
}

then the concrete conflict guard is:

not s and q and r

not:

q and r

If two overlapping effective concrete branches assign the same expression, that
is legal. If they assign different expressions, we synthesize
InternalAssertFalse under the overlap guard.

---

With this representation, going to ITEs for codegen is going to be very easy.
But why not just stick with ITEs in the IR itself, since that's essentially what
we're building implicitly through the preferred assignment partial ordering of
DontCare > Concretes[0] > Concretes[1] > ...?

Why represent DontCares separately?

• Since DontCares are special and there are a lot of reasons why we want to go
  looking for a DontCare and check if our assignment evaluated to it (waveform
  outputs, for example), it's useful to have the DontCare assignment guard be
  its own thing instead of being hidden amongst the concrete assignments.
• Since DontCares get moved around in a parallel merge (need to prefer
  Concrete's from other transactions over them), it's easier to keep them
  separate than have to move things around in a vector, or deconstruct and
  reconstruct an ITE.

Why represent Concretes in a Vector not an ITE?

• ITEs make it harder to extract every individual guard (e.g. q1, q2, q3, ..., qn) and AND/OR them together as we need to do sometimes to force orderings
  compared to just having the guards directly in a sequential vector.
• With ITEs, we need to write down an explicit default value if all the guards
  q1, ..., qn fail. Right now, we don't want to list an explicit value because
  we're going to InternalAssertFalse that we should never reach that value
  anyways.

[sampsyo]

This is quite clear, @Nikil-Shyamsunder! I thought carefully about your actual formulas here, and they seem right given the semantics you've outlined. I also agree with the following general observation: because DontCare is such a privileged value (it is the only thing that is allowed to be overwritten by a parallel assignment), it makes sense that the data structure would need to distinguish it. Letting it get "lost" in a deep ITE nest seems like a recipe for unpleasantness.

Here are two minor comments:

• You've proposed that the action guard for assignments must be 1 is an IR invariant. That makes sense, because assignments already have a way to guard. But if you find it useful, this could also be a normalization step as opposed to an invariant. (That is, you could allow the action guard to become non-1 sometimes, but when it's time to merge, you normalize so the action guard becomes 1 before proceeding.)
• About conflicts: is the plan to always discharge this check when merging? Or is there some way to record the conflict condition so it can be checked later? If we want to avoid needing to discharge this proof burden every time we merge, it seem like the data structure may need yet another field for the conflict state?? Or is there maybe a way to encode the conflict state in the Concretes array?

[Nikil-Shyamsunder]

Thanks! Regarding the two comments

• I haven't found a reason to have non-1 guards yet, but if it comes up I will keep this in mind as a way to do that nicely.
• Yup, we discharge what we can while merging but if we can't we use this InternalAssertFalse thing. This is a first-class action in the IR, which we can panic on in the interpreter if we can't statically discharge it, or lower into the RTL and maybe prove later on in RTL that "the InternalAssertFalse port never goes to high" or something. I believe this is what you mean by encoding a conflict state.