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

# Verification

This Chapter explains how to use the verification functionality of ILAng to generate verification target to work with existing model checkers. Currently we support Cadence JasperGold, CoSA, Pono (previously named CoSA2). For other Verilog model checker, we can generate a standalone Verilog with embedded assumptions and assertions using the SVA format.

For verification, you will need (1) an ILA model (2) the Verilog module (3) the refinement relation to map ILA and Verilog, this is shown in the following figure.

![](/files/-ML8miLlEE6dBZw5B45S)