Open wky17 opened 4 months ago
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 https://github.com/llvm/circt/pull/6917) purely feedforward.
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?
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?
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:
(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.
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[^1]—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.
[^1]: The constraints x1 ≥ 2∙x2 – 3 and x2 ≥ 2∙x1 – 3 imply x1 ≤ 3 and x2 ≤ 3.
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?
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”.
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: https://github.com/llvm/circt/blob/d9e35fa8a91be8ba274b59e4616b3b1987dae679/lib/Dialect/FIRRTL/Transforms/InferWidths.cpp#L1575
@darthscsi: Do you have any thoughts on how you had been thinking about a new algorithm for width inference?
When I write a FIRRTL program like this:
widths constraints for implicit widths in the circuit should be:
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:
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?