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
  • Defining instructions
  • Decode function
  • State update functions

Was this helpful?

  1. Modeling

Instructions

Defining instructions

To define an instruction of the ILA model m:

auto instr = m.NewInstr("RD/WR_ADDR");

Decode function

The decode function takes in the opcode and return a Boolean type output, indicating whether an instruction is issued. It can be set to an Boolean type expression:

instr.SetDecode(InAddr == 0xFF02);

State update functions

Each instruction contains the state update functions of every state variables (unchanged if not specified). The update function can be set to an expression of the same type:

instr.SetUpdate(Addr, ilang::Ite(Cmd == 1, InData, Addr));
instr.SetUpdate(OutData, ilang::Ite(Cmd == 0, Addr, 0x0));
PreviousUninterpreted functionNextHierarchical ILA

Last updated 6 years ago

Was this helpful?