> For the complete documentation index, see [llms.txt](https://hongcez.gitbook.io/ilang-doc/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://hongcez.gitbook.io/ilang-doc/verification/target.md).

# 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                                 |