If this is directly adding components to the builder in the constructor, and doesn't actually generateComponent as a BaseModule, maybe this should be more of a helper function rather than a BaseModule class that is instantiated? It seems like all we really need here is a public API to push a DefFormalTest, which can pass the name and parameters to FIRRTL. So maybe this could be more like:

object FormalTest {
  def apply(...) = {
    ...
  }
}

Hmmm yeah, that is a good point. I'll give that a shot!

Thanks for the suggestion! That cleaned things up quite a bit 🙂. Not entirely sure where to get the source location from now, and the FIRRTL-side Component needs a def id: BaseModule field, but I can make both work by just using the test harness module for that. 👍

Cool, that does look cleaner to me. If you want to materialize a SourceInfo at the callsite, I think you can add an implicit argument to your apply method, like:

def apply(...)(implicit sourceInfo: SourceInfo)

Ah nice, I was wondering if that would just work, or if the plugin was hardwired to only touch certain constructs. I've added that and threaded it through to the FIRRTL emission. Works like a charm! Thanks for the pointer 🙂

nit: maybe add a check for module Foo_2 so we know that is indeed the module name? Could maybe use the capture / substitution functionality as well, so we could do something like CHECK: module [[NAME:Foo.+]] and later CHECK: formal Foo of [[NAME]]?

Ah yeah, nice catch. Forgot that this actually runs through FileCheck with all the bells and whistles.

Done 👍

It's fine that in this PR we're just testing for the basic FIRRTL emission, but how are Chisel users really intended to use this?

I'd expect this to combine nicely with some of the work that @tmckay-sifive has been doing on defining unit tests and inline tests. There could be an API like formalTest { ... } that you get for your Testable or HasTest (don't remember what the proposed trait was exactly), which would mark the generate test harness as a formal test. We may also want to allow the user to define some of the parameters on the test, or at least supplement whatever Chisel does internally with their own stuff. There might also be cases where the user really wants to manually mark modules as formal tests through this API, if they need multiple test runs on the same harness with different parameters.

TL;DR, I'd imagine something like this as a the lowest barrier of entry for formally testing modules:

class MyModule extends RawModule with Testable {
  val a = IO(Input(UInt(8.W)))
  val b = IO(Input(UInt(8.W)))
  val z = IO(Output(UInt(8.W)))

  // ... module body ...

  formalTest "Complete" { dut =>
    AssertProperty(dut.a + dut.b === dut.z)
  }
  formalTest "NeutralA" { dut =>
    AssumeProperty(dut.a === 0.U)
    AssertProperty(dut.b === dut.z)
  }
  formalTest "NeutralB" { dut =>
    AssumeProperty(dut.b === 0.U)
    AssertProperty(dut.a === dut.z)
  }
}

I'm wondering if we really want FormalTest and the Parameters classes to be part of the Chisel public API vs. a more sugary API like your sketch above. In any case, not gonna sandbag here, we should just make sure to massage the API before we really start advertising this to users