[FIRRTL] Add Inline Formal Test ops

[dobios]

The goal of this PR is to add a new set of inline formal test ops to FIRRTL:

FIRRTL version 4.0.0

circuit Foo:
  public module Foo:
    input data : UInt<32>
    input c : UInt<1>
    output out : UInt<32>
    ;; Foo body

  module FooTest:
      ;; example test
      inst foo of Foo
      ;; symbolic input -- maps to input in btor2
      input s_foo_c : UInt<1>
      input s_foo_data : UInt<32> 
      ;; feed the symbolic inputs to the instance
      connect foo.c, s_foo_c 
      connect foo.data, s_foo_data
      ;; example assertion that uses the symbolic inputs and outputs
      intrinsic(circt_verif_assert, intrinsic(
        circt_ltl_implication : UInt<1>, s_foo_c, eq(foo.out, s_foo_data))
      )

  formal testFormal of FooTest, bound = 20
  
  

These new ops will then be lowered to the existing verif.formal op in a future PR.

[uenoku]

Awesome! Parser and Op definitions generally look great. It would be also necessary to modify firrtl-spec. Regarding FIRRTL dialect representation there are several things to consider since FormalOp is a first operation which is not FModuleOp but could contain mots of FIRRTL ops:

1. InstanceGraph -- FormalOp has an instance op so we would need to create an edge from FormalOp to the referenced module. Probably need to implement ModuleOpInterface.
2. FModuleOp pass -- LowerIntrinsics, ExpandWhen etc. are currently FModuleOp pass so we need to find a way to run them on FormalOp

[mmaloney-sf]

@uenoku commented:

It would be also necessary to modify firrtl-spec.

Feel free to reach out to me if you want to offload the FIRRTL spec work to me.

[uenoku]

The new design looks fantastic! Thank you for iterating on this! The implementation looks great to me except for few nits regarding ReferableDeclOp.

[uenoku]

I think it needs Symbol as well.

[uenoku]

LGTM, can you check whether we should first change FIRRTL-spec or merge the PR?

[dobios]

Firrtl spec is updated, so I guess we're good to go!