[FIRRTL] Disallow Top-level Abstract Reset

[seldridge]

The following circuit should be an error. Assumedly, this should be a verification hook added to either a FIRRTL circuit or to a module that is conditioned on it being the top module.

circuit Foo:
  module Foo:
    input a_d: UInt<1>
    output a_q: UInt<1>
    input r: Reset
    input c: Clock

    reg x: UInt<1>, c with:
      reset => (r, UInt<1>(0))

    x <= a_d
    a_q <= x

When running with the Scala FIRRTL Compiler, this errors quickly:

firrtl -i chiselTests/Reset.fir                     
# Exception in thread "main" firrtl.passes.CheckHighFormLike$ResetInputException: : [module Foo] Abstract Reset not allowed as top-level input: r

When compiling with CIRCT, this happily goes all the way to Verilog and generates a synchronous reset flip flop.

[lattner]

Is this something that the chisel API should catch, or is this a user error that we want to enforce at the FIRRTL level?

The difference is really important. If this is an invariant of the IR that Chisel should check, then this should be a verifier check. If this is a logical bug that we want to diagnose in a nice way, then we should write a "type checking" pass that checks these assumptions and reports them in a "user exposed" way. There are direct analogies to Swift's SIL passes which are dataflow passes that enforce dataflow properties (like designated initialization errors).

This question applies to https://github.com/llvm/circt/issues/564 as well.

If these are semantic user problems that we should catch then I think we need a pass that is run early in the pipeline to catch and report these, and we should spend a lot of time wordsmithing the diagnostics etc.

[lattner]

(no, I'm not impressed by Exception in thread "main" in some compiler internals :-) )

[lattner]

DI is a now huge pass in Swift, but there are simpler things akin to this.

[seldridge]

I think this is really an invariant of the IR and a Chisel-level check. Basically, it's nonsensical to have a top-level abstract reset port for the reason that reset type inference will default to synchronous if no other information is available. Therefore, if there's not at least one input to the global algorithm (a top level port), then you can run into problems where you do local inference on a sub-circuit, the abstract reset goes to synchronous, but then that's legally instantiated in an asynchronous region (which is a type error). The algorithm is sketched out here.

Conversely, the reset inference pass should provide really good diagnostics and would be the latter variant of pass you mention.

What do you think?

@jackkoenig: Does this make sense to you?

@lattner wrote:

(no, I'm not impressed by Exception in thread "main" in some compiler internals :-) )

😬 😬 😬

[jackkoenig]

I think this is really an invariant of the IR and a Chisel-level check. Basically, it's nonsensical to have a top-level abstract reset port for the reason that reset type inference will default to synchronous if no other information is available. Therefore, if there's not at least one input to the global algorithm (a top level port), then you can run into problems where you do local inference on a sub-circuit, the abstract reset goes to synchronous, but then that's legally instantiated in an asynchronous region (which is a type error). The algorithm is sketched out here.

Conversely, the reset inference pass should provide really good diagnostics and would be the latter variant of pass you mention.

@jackkoenig: Does this make sense to you?

It makes sense to me with the stated goal being matching the behavior of SFC. An issue I've always struggled with w.r.t. SFC's reset inference is how to make such operations support incremental compilation. If we hoisted abstract reset to be a type parameter in CIRCT, could it perhaps leverage standard MLIR/LLVM incremental compilation flow? I have no idea how that works though, it seems to me that specializing generic methods/modules might be tricky in incremental compilation as well.

In any case, for matching SFC's behavior I agree with everything you've said.

(no, I'm not impressed by Exception in thread "main" in some compiler internals :-) )

Are you suggesting there shouldn't be ~80 useless characters before you get to the error message? Oh, the humanity!

[seldridge]

This should probably be rolled into the existing InferResets/CheckResets pass. Currently we're doing some weird inference that results in the following circuit compiling when it should not:

circuit Foo:
  module Foo:
    input a: Reset
    output b: AsyncReset

    b <= a

With CIRCT, this produces:

firrtl.circuit "Foo"   {
  firrtl.module @Foo(in %a: !firrtl.asyncreset, out %b: !firrtl.asyncreset) {
    firrtl.connect %b, %a : !firrtl.asyncreset, !firrtl.asyncreset
  }
}

With the SFC, this errors:

Exception in thread "main" firrtl.passes.CheckHighFormLike$ResetInputException: : [module Foo] Abstract Reset not allowed as top-level input: a

[jackkoenig]

This should probably be rolled into the existing InferResets/CheckResets pass. Currently we're doing some weird inference that results in the following circuit compiling when it should not:

So I'm not sure I'd call that a "weird" inference; it's actually what I'd prefer to do in SFC as well. Reset inference runs forwards and backwards so I see no reason why we shouldn't just start allowing this. The reason SFC errors is because we check for this separately and before we run the inference pass. If we didn't error, SFC's inference pass would do the same thing you're doing here.

[seldridge]

Ah, good call.

Accepting more circuits (and doing the right thing) makes sense to me.

I had filed this when I was generating examples that would try to show two reset nets merging that shouldn't and thought it might be an issue. I realized after the fact that it probably wasn't.

The correct check here should be if any resets are not inferred after InferResets runs, then error.