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


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://hongcez.gitbook.io/ilang-doc/verification/target.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.