stateful declarations shouldn't be allowed in conditions (was: what happens when you read from inactive enum variants)

[programmerjake]

I noticed that firrtl lets you read from inactive enum variants using code like:

FIRRTL version 3.2.0
circuit test:
    module test:
        input clk: Clock
        input a: UInt<1>
        input b: UInt<1>
        output o: UInt<1>
        connect o, UInt<1>(0)
        wire w: {|Some: UInt<1>, None|}
        connect w, {|Some: UInt<1>, None|}(None)
        when a:
            connect w, {|Some: UInt<1>, None|}(Some, b)
        match w:
            None:
                skip
            Some(v):
                reg r: UInt<1>, clk
                connect r, v
                connect o, r

note how if a is false, it still writes v to r, which you can then read in the next clock cycle.

this makes me think that putting stateful logic elements in a conditional block is a misfeature because state changes still occur even when the conditional block is not active.

[seldridge]

For registers, this should do what you want. I.e., r should only be updated to v when w is a Some. (Maybe I'm misunderstanding.)

That example should simulate the same with the register inside or outside the match (just like with a when block).

You do bring up a good point about other circuit components, specifically wires and instances. If reg r is instead wire r, then there is a question about what value it takes when w is a None. There's two interpretations of how this could be handled:

1. The conservative approach of this is an unconditional connection. Conditionality is only evaluated for conditions deeper than the declaration.
2. A more relaxed approach of r is invalidated when w is a None and a FIRRTL compiler can choose any value for r when w is a None.

CIRCT will take interpretation (1) for reasons that this is what the Scala-based FIRRTL Compiler did. However, I don't actually think that there is a reason why it can't be invalidated other than there is legacy Chisel code that is relying on this behavior. The problematic case is where a user has instantiated a module under a when and they wrote assertions in the module. Interpretation (2) will likely break these assertions.

I've toyed with a radical change to the FIRRTL spec which would disallow any statement under a conditional statement other than connects. This avoids all of the ambiguity here.

[programmerjake]

For registers, this should do what you want. I.e., r should only be updated to v when w is a Some.

afaict that's not right. The spec describes how connects depend only on the conditions in between the destination declaration and the connect:

firrtl-spec/spec.md

Lines 1908 to 1912 in f3b0034

	For connections (see [@sec:connections]), appearing inside of a conditional block affects whether or not the connect executes.
	The sink of a connect operator will correspond to a circuit component declared earlier in the module.
	We consider the conditions associated to the blocks of all conditional blocks which contain the connect statement, but which do *not* contain the declaration of the circuit component.
	We call this set of conditions the **interleaving conditions** of the connect.
	Whenever we determine the last connect semantics (see [@sec:last-connect-semantics]) for that component, if each of the interleaving conditions is true, then that connect is executed.

for the code:

FIRRTL version 3.2.0
circuit test:
    module test:
        input clk: Clock
        input a: UInt<1>
        input b: UInt<1>
        output o: UInt<1>
        connect o, UInt<1>(0)
        when a:
            reg r: UInt<1>, clk
            connect r, b
            connect o, r

the firrtl-expand-whens pass makes the change:

// -----// IR Dump Before ExpandWhens (firrtl-expand-whens) //----- //
firrtl.module @test(in %clk: !firrtl.clock, in %a: !firrtl.uint<1>, in %b: !firrtl.uint<1>, out %o: !firrtl.uint<1>) attributes {convention = #firrtl<convention scalarized>} {
  %c0_ui1 = firrtl.constant 0 : !firrtl.uint<1>
  firrtl.matchingconnect %o, %c0_ui1 : !firrtl.uint<1>
  firrtl.when %a : !firrtl.uint<1> {
    %r = firrtl.reg interesting_name %clk : !firrtl.clock, !firrtl.uint<1>
    firrtl.matchingconnect %r, %b : !firrtl.uint<1>
    firrtl.matchingconnect %o, %r : !firrtl.uint<1>
  }
}

// -----// IR Dump After ExpandWhens (firrtl-expand-whens) //----- //
firrtl.module @test(in %clk: !firrtl.clock, in %a: !firrtl.uint<1>, in %b: !firrtl.uint<1>, out %o: !firrtl.uint<1>) attributes {convention = #firrtl<convention scalarized>} {
  %c0_ui1 = firrtl.constant 0 : !firrtl.uint<1>
  %r = firrtl.reg interesting_name %clk : !firrtl.clock, !firrtl.uint<1>
  firrtl.matchingconnect %r, %b : !firrtl.uint<1>
  %0 = firrtl.mux(%a, %r, %c0_ui1) : (!firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
  firrtl.connect %o, %0 : !firrtl.uint<1>
}

[programmerjake]

CIRCT will take interpretation (1) for reasons that this is what the Scala-based FIRRTL Compiler did. However, I don't actually think that there is a reason why it can't be invalidated other than there is legacy Chisel code that is relying on this behavior. The problematic case is where a user has instantiated a module under a when and they wrote assertions in the module. Interpretation (2) will likely break these assertions.

For wires, and any other stateless constructs, it shouldn't matter what value wires take when the conditionals their declaration is in are not active, since you can't read them then. For any stateful constructs it does matter.

I've toyed with a radical change to the FIRRTL spec which would disallow any statement under a conditional statement other than connects. This avoids all of the ambiguity here.

Imo some stuff should still be allowed under conditionals:

• generally expected stuff:
  • connect
  • invalidate
  • when
  • match
  • node
• wire -- since you can't read its value when the condition is false
• statements that have attached conditions (lowering just combines the conditionals with the attached conditions:
  • skip
  • stop
  • printf
  • assert/assume/cover
• intrinsics, but only for those intrinsics that specifically allow being in a condition