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?

  1. Modeling

ILA Model

Defining ILA models

To start defining an ILA model, the first thing is to create an Ila object at the top-most level.

auto m = ilang::Ila("model_name");

The object hierarchy is structured based on the ILA formal model:

ILA
+-  Architectural states
|   +-  Inputs variables (leaf nodes of type Boolean or bit-vector)
|   +-  State variables (leaf nodes of type Boolean, bit-vector, or memory)
|
+-  Instructions
|   +-  Decode function: expression (bit-vector)
|   +-  State update functions: expression (same type as the state)
|
+-  Valid function: expression (Boolean)
|
+-  Fetch function: expression (bit-vector)
|
+-  Initial conditions: expression (Boolean)
|
+-  Child ILAs

Note: expressions are the AST tree where input and state variables are the leaf nodes.

PreviousModelingNextArchitectural States

Last updated 6 years ago

Was this helpful?