[FIRRTL] Accept list of parameters for formal construct

[fabianschuiki]

Adjust the syntax for the FIRRTL formal construct such that it no longer expects a single bound = <N> parameter, but accepts a list of user-defined integer, string, array, or dictionary parameters. The syntax now looks like

formal someTest of SomeModule:
  a_int = 42
  b_string = "hello"
  c_array = [42, "hello", [9001], {foo = 1337}]
  d_map = {a = 42, b = "hello", c = [9001], d = {foo = 1337}}

instead of the previous

formal someTest of SomeModule, bound = 42

The previous syntax is still supported until the corresponding change to the FIRRTL spec lands. Since it is not yet entirely clear what the list of necessary or well-understood parameters for formal tests is, the presence of bounds is no longer enforced. The rationale here being that this might turn out to be just a default setting in the formal test runner, which the user may not want to explicitly state. Once we have a clearer picture of which parameters are necessary, we can extend the parser to enforce parameters to be of specific types, and for specific parameters to be always defined.

This is the first time we allow for arrays and dictionaries to be specified as parameters. To avoid code duplication, this commit extends the parseParameter function with an allowAggregates option that enables parsing of [...] arrays and {...} dictionaries. The function now returns an untyped attribute, and places which want to turn this into a ParamDeclAttr now cast the result to a TypedAttr themselves. Parsing of the values is split out into a separate parseParameterValue function, which allows for the parsing of nested arrays and dictionaries. A similar adjustment exists in the emitter.

This commit is the first step towards lowering formal constructs in FIRRTL inputs to verif.formal core dialect ops, and running them with circt-test. The ability to specify parameters will help us build out the testing infrastructure without requiring spec changes for every single parameter adjustment.

[uenoku]

Does Chisel emit the old bound = N currently? It's unfortunate that we have to keep old style as well 😿

[fabianschuiki]

It's only until the thing is in the spec. I'll drop this again afterwards. Chisel doesn't emit anything as of today 😁

[dobios]

I like this approach and how it makes the construct more expressive!
Wouldn't we want to standardize the set of attributes that are expected and have it clearly be defined what their value is when they are omitted (e.g. the bound)? I feel like this should be shown somewhere either in the firrtl spec or in some documentation somewhere. Like there should be a clear list of what the expected attributes can be and what they mean which it seems that this change doesn't introduce (yet).

I feel like the line

No parameters with well-known semantics are defined yet.

Is more confusing than helpful ^^"

[dobios]

Otherwise looks good to me, this seems like a good addition and specs can always be updated later.