Verification Target

The verification target can be generated by creating the IlaVerilogRefinementChecker object.

The arguments of the constructors are:

1. The ILA object

2. A list of paths to search for Verilog include files

3. A list of Verilog design files

4. The Verilog top module

5. The variable mapping file (first part of refinement map)

6. The instruction start/ready conditions (second part of refinement map)

7. The output path of the verification targets

8. The choice of backend, which can be either ModelCheckerSelection::JASPERGOLD or ModelCheckerSelection::PONO

9. (Optional) Verilog generator configuration

Some of the useful options are listed below (see include/ilang/rtl_verify.h for a full list):

Option	Meaning	Possible values
ForceInstCheckReset	Whether to start from an arbitrary state	true/false
PonoEngine	Engines for Pono	"ind", "bmc", "ic3ia", "ic3sa", ...
PonoOtherOptions	Additional options for Pono	e.g., " -v 1 " sets verbose level to be 1.
YosysSmtArrayForRegFile	Whether to use SMT arrays for Verilog arrays	true/false