[FIRRTL][InferWidths] When there is no unique minimal solution for width constraints, what should be the width?

[wky17]

When I write a FIRRTL program like this:

circuit FormalSimple :
  module FormalSimple :
    input clock : Clock
    input reset1 : UInt<1>
    output io : UInt<10>

    wire a1 : UInt
    wire a2 : UInt

    a1 <= shr(mul(a2, a2), 3)
    a2 <= shr(mul(a1, a1), 3)

    io <= a1

widths constraints for implicit widths in the circuit should be:

x1 >= 2x2 -3
x2 >= 2x1 -3

and the solution can be (2,1) or (1,2), which is confused to find out which solution should be assigned to a1,a2.

In fact for this case, firtool gives an error like this:

FormalSimple.fir:7:5: error: 'firrtl.wire' op is constrained to be wider than itself
    wire a1 : UInt
    ^
FormalSimple.fir:7:5: note: see current operation: %0 = "firrtl.wire"() {annotations = [], name = "a1", nameKind = #firrtl<name_kind droppable_name>} : () -> !firrtl.uint
FormalSimple.fir:11:15: note: constrained width W >= 2W here:
    a2 <= shr(mul(a1, a1), 3)
              ^
FormalSimple.fir:11:11: note: constrained width W >= 2W-3 here:
    a2 <= shr(mul(a1, a1), 3)
          ^
FormalSimple.fir:11:11: note: constrained width W >= 2W here:
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
    a2 <= shr(mul(a1, a1), 3)
       ^
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
FormalSimple.fir:8:5: note: constrained width W >= 2W here:
    wire a2 : UInt
    ^
FormalSimple.fir:11:15: note: constrained width W >= 2W here:
    a2 <= shr(mul(a1, a1), 3)
              ^
FormalSimple.fir:11:11: note: constrained width W >= 2W-3 here:
    a2 <= shr(mul(a1, a1), 3)
          ^
FormalSimple.fir:11:11: note: constrained width W >= 2W here:
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
    a2 <= shr(mul(a1, a1), 3)
       ^
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
FormalSimple.fir:11:8: note: constrained width W >= 2W here:
FormalSimple.fir:8:5: note: constrained width W >= 2W here:
    wire a2 : UInt
    ^
FormalSimple.fir:10:15: note: constrained width W >= 4W here:
    a1 <= shr(mul(a2, a2), 3)
              ^
FormalSimple.fir:10:11: note: constrained width W >= 4W-3 here:
    a1 <= shr(mul(a2, a2), 3)
          ^
FormalSimple.fir:10:11: note: constrained width W >= 4W here:
FormalSimple.fir:10:8: note: constrained width W >= 4W here:
    a1 <= shr(mul(a2, a2), 3)
       ^
FormalSimple.fir:10:8: note: constrained width W >= 4W here:
FormalSimple.fir:10:8: note: constrained width W >= 4W here:
FormalSimple.fir:10:8: note: constrained width W >= 4W here:

The error means this program is illegal For FIRRTL or there is some problem in CIRCT compiler? What should be the solution and the widths?

[seldridge]

The error is saying that there isn't enough information to choose a width. In this case, as you identify, this is a system of linear inequalities and there are multiple solutions that are possible here. (A FIRRTL compiler won't choose one possible solution.) Either the width of a1 or the width of a2 would need to be specified by the author of the FIRRTL snippet so that a compiler can infer a width.

It's thereby illegal FIRRTL.

While the width inference algorithm is internally expressed as a (very simple) set of constraints that are solved, it is intended to be (and practically after #6917) purely feedforward.

[wky17]

okay, if it is a case of illegal program when there is no unique solution for constraint solver, is there a specification for all compilation passes that defines illegal cases?

[dnjansen]

I am not sure what is the exact problem here. If the constraints are

    x1 >= 2*x2 - 3
    x2 >= 2*x1 - 3

and implicitly also

    x1 >= 1
    x2 >= 1

Then I think (x1,x2) = (1,1) is a solution. Why does the constraint solver not find this solution?

[seldridge]

Minor correction: the implicit constraint is really x1 >= 0 and x2 >= 0 because zero-width is allowed. So, you could argue that the optimal choice, from a PPA cost perspective, is to choose (0, 0) as this allows for removal of hardware.

The simplistic reason why it doesn't find the (0, 0) solution is that this is that this is not how the Scala-based FIRRTL Compiler (SFC) infer widths constraint solver was originally written. During the migration from the the SFC to CIRCT, this algorithm was ported as-is in order to enable Chisel users to migrate without changes to width inference. Given that CIRCT is fully online and the SFC is deprecated, this is no longer a good reason!

That said, this algorithm is generally trying to be feedforward. Known widths are used to determine unknown widths based on the width propagation rules of primitive operations. This generally matches how designers are using uninferred widths (in the limited uses where they are using uninferred widths). The example here is different from this use case in that the request is about choosing a minimum width given only unknown widths. To help narrow the discussion, the original reported circuit can be reduced to the following with all primitive operations removed:

  module Foo :
    input clock : Clock
    output io : UInt<10>

    reg a1 : UInt, clock
    reg a2 : UInt, clock

    a1 <= a2
    a2 <= a1

    io <= a1

Here, the inequalities are a1 >= a2 and a2 >= a1. It's perhaps reasonable to say that improvements to the constraint solver would be able to solve this, by choosing (0, 0). However, in almost all situations, this is user error.

So, I can see this going in two directions:

1. This is a bug and the constraint solver should be beefed up here.
2. This is intentional and unknown widths must be constrained by known widths.

(2) may be better and is more aligned with changes we've been wanting to make to width inference to make it simpler. The current constraint solver is insanely expensive for what it is doing. It builds up a complete shadow IR of constraints and then solves this. Most designers have empirically shied away using unknown widths because they're unpredictable. In the designs that we have, width inference is both slow, a memory hog, and not actually inferring that many widths because these are so rarely used. There have then been discussions about making width inference an incredibly simple feedforward, iterative algorithm that avoids framing this as a constraint problem. I anticipate that this algorithm also won't work for the example above, though that likely aligns with how designers are using Chisel and unknown widths.

[dnjansen]

TL;DR: I recommend to simplify width inference to handle only acyclic dependencies.

We are also thinking about an implementation of the width inference algorithm. If the width dependency graph is acyclic—one might interpret “simple feedforward” as this—it is sufficient to infer widths by calculating them in the topological order of the graph. For us, that would be the most convenient solution, and it might be sufficient for the (few) uses where unspecified widths are used in practice.

However, if one allows cycles like the ones in these examples, a more complex algorithm is needed. A legitimate use of width-inference cycles in designs might be a counter register in a reusable module, with something like counter <= mux(trigger, tail(1)(counter + UInt(1)), counter), but such a direct cycle (constraint “width(counter) ≥ width(counter)”) is easily recognized and can be dropped.

The original example of wky17 still seems to exhibit a bug in the width inference constraint solver. It contains a combinatorial cycle, which should generate an error message, but not this one. But (wky17 has told me) even if one replaces the wires by registers, the same error message is produced. If one “beefs up the constraint solver”, a construct similar to wky17’s can be used to give a maximum width constraint¹—something that I would rather not have. Currently, there is a kind of monotonicity in width inference: if some width is ok (i.e. avoids data loss), then any larger width is allowed as well, only that it uses more silicon. However, that would no longer hold if one can formulate maximum width constraints.

Footnotes

1. The constraints x1 ≥ 2∙x2 – 3 and x2 ≥ 2∙x1 – 3 imply x1 ≤ 3 and x2 ≤ 3. ↩

[wky17]

This is an example of GCD:

circuit GCD :
  module GCD : 
    input clk : Clock
    input reset : UInt<1>
    output io : {flip a : UInt<16>, flip b : UInt<16>, flip e : UInt<1>, z : UInt<16>, v : UInt<1>}
    
    io is invalid
    reg x : UInt, clk
    reg y : UInt, clk
    node T_7 = gt(x, y)
    when T_7 :
      node T_8 = sub(x, y)
      node T_9 = tail(T_8, 1)
      x <= T_9
      skip
    node T_10 = gt(x, y)
    node T_12 = eq(T_10, UInt<1>("h00"))
    when T_12 :
      node T_13 = sub(y, x)
      node T_14 = tail(T_13, 1)
      y <= T_14
      skip
    when io.e :
      x <= io.a
      y <= io.b
      skip
    io.z <= x
    node T_16 = eq(y, UInt<1>("h00"))
    io.v <= T_16

We can see that there is a dependency from y to x: y -> T_8 -> T_9 -> x and x to y: x -> T_13 -> T_14 -> y, which means x and y depends on each other. But this program can be solved by CIRCT.
I think it's kind of similar to the case:

  module Foo :
    input clock : Clock
    output io : UInt<10>

    reg a1 : UInt, clock
    reg a2 : UInt, clock

    a1 <= a2
    a2 <= a1

    io <= a1

Then why there is no error in GCD program? Does it means that CIRCT just ignore cycles and solve with explicit widths?

[dnjansen]

We tried a bit and found out that in circuit Foo there is no constraint on the widths of a1 and a2 at all. In particular, they are not constrained to have a width of at least 0. Adding some statement to ensure that constraint (e.g. a1 <= UInt<0>(0)) makes the error go away. I consider this a bug: the constraint solver does not automatically add constraints “width(a1) ≥ 0”. (Or at least, if this behaviour was intended to signal components that do not depend on any external input at all, the error message should be more informative.)

However, a similar trick does not work in the initial example FormalSimple, even after changing the wires to registers. I think there may be another bug, but we haven’t yet found the minimal difference to make the error message go away. I guess that the constraint solver has as a precondition: If there is some constraint “width(a1) ≥ expression(width(a1))”, then “λw.w – expression(w)” should be a isotonic function in w.

In trying, we also found some other behaviour contrary to specification: “width(shr(...)) ≥ 1” even on type UInt, while the manual specifies that for UInt, it should be “width(shr(...)) ≥ 0”.

[seldridge]

Then why there is no error in GCD program? Does it means that CIRCT just ignore cycles and solve with explicit widths?

This is working because there is a constraint from a known width, specifically x <= io.a. However! I did notice that this is insufficient to work in all situations if there are additional constraints on x that make it more like the first FormalSimple example. Something seems wrong here.

I do want to state that both of you are applying far more rigor to this problem than has been applied previously. Thanks for digging into this!

We tried a bit and found out that in circuit Foo there is no constraint on the widths of a1 and a2 at all. In particular, they are not constrained to have a width of at least 0. Adding some statement to ensure that constraint (e.g. a1 <= UInt<0>(0)) makes the error go away. I consider this a bug: the constraint solver does not automatically add constraints “width(a1) ≥ 0”. (Or at least, if this behaviour was intended to signal components that do not depend on any external input at all, the error message should be more informative.)

Yes, this sounds like a bug.

If you do add the constraint, does the circuit optimize itself to nothing, i.e., just io <= UInt<10>(0)?

However, a similar trick does not work in the initial example FormalSimple, even after changing the wires to registers. I think there may be another bug, but we haven’t yet found the minimal difference to make the error message go away. I guess that the constraint solver has as a precondition: If there is some constraint “width(a1) ≥ expression(width(a1))”, then “λw.w – expression(w)” should be a isotonic function in w.

I'm not sure what to do with this. I would be happy with a saner user error. E.g., "reg a is not driven by a known width". This type of error message contradicts what you were able to show with the Foo example, however, where that is then solvable.

In trying, we also found some other behaviour contrary to specification: “width(shr(...)) ≥ 1” even on type UInt, while the manual specifies that for UInt, it should be “width(shr(...)) ≥ 0”.

Is this a CIRCT version issue or a bug where this was missed when making this spec change in CIRCT? This was only changed recently such that SInt saturates at 1-bit and UInt saturates at 0-bit. See:

circt/lib/Dialect/FIRRTL/Transforms/InferWidths.cpp

Line 1575 in d9e35fa

// UInt saturates at 0 bits, SInt at 1 bit

@darthscsi: Do you have any thoughts on how you had been thinking about a new algorithm for width inference?