[minor] Formal Test definitions and test harnesses

[dobios]

This PR proposes a new formal construct that allows for test harness modules to be marked as formal tests to be run using bounded model checking with a given bound. This is a first step towards enabling inline formal tests and already has support in CIRCT through the btor2 and circt-bmc backends. It also has the following approved PR that adds support for the new op in CIRCT (llvm/circt#7374)

Example:

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

[mwachs5]

from an administrative standpoint, if this is "just" adding a new feature (vs breaking old ones) it can be minor