You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The FIRRTL spec defines a `formal` construct to indicate that a module
should be executed as a formal test. Currently, there is no way to emit
this construct from Chisel.
This PR adds a user-facing `FormalTest` class that can be used to mark
a module as to be executed as a formal test. This would commonly be used
inside a test harness module to mark the surrounding module as a test.
For example:
class TestHarness extends RawModule {
FormalTest(this)
}
The formal test can be given an optional name and a map of parameters.
The parameters are distinct from blackbox modules in that they do not
map to Verilog parameters, but instead allow for any recursive nesting
of integers, doubles, strings, arrays, and maps, as prescribed by the
FIRRTL spec. Multiple formal test markers may be added to a single
module, which may be useful if a test should be run with different sets
of user-defined parameters.
This PR also adds the necessary IR nodes to the FIRRTL and Chisel FIRRTL
IRs.
0 commit comments