ILAng
  • Introduction
  • Getting Started
    • Installing ILAng
    • ILAng with CMake
    • ILAng with Python
    • ILAng in Docker
  • Modeling
    • ILA Model
    • Architectural States
      • Expressions
      • Uninterpreted function
    • Instructions
    • Hierarchical ILA
    • Conclusion
  • Synthesis
    • Writing Templates
    • Interfacing Simulators
    • Synthesis Results
    • Conclusion
  • Verification
    • Refinement Relation
    • Verification Target
    • Examples
    • Notes
  • Development
    • Release Notes
Powered by GitBook
On this page

Was this helpful?

Verification

PreviousConclusionNextRefinement Relation

Last updated 4 years ago

Was this helpful?

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.