This section covers how to construct the ILA formal model through ILAng's programming interface. You will learn how to define each component of the ILA model.
{% hint style="info" %} This guide only shows a selected list of features. The complete set of all supported API with detailed description can be found here. {% endhint %}
As described in TODAES18, the ILA formal model has several valuable attributes for modeling and verification. It is modular, with functionality expressed as a set of instructions. It enables meaningful abstraction through architectural state that is persistent across instructions. It provides for portability through a more durable interface with the interacting processors. It is hierarchical, providing for multiple levels of abstraction for modeling complex instructions as a software program through sub- and micro-instructions.
The below image shows the instruction set for the AES cryptographic accelerator from OpenCores.org. The design behavior can be represented using these 8 instructions, e.g., RD/WR_ADDR, START_ENCRYPT, GET_STATUS, etc. Instead of all micro-architectural states/registers, only the architectural states are included in the ILA model.
The ILA model can be hierarchical, in that it can contains child-ILAs to represent complex operations. It is often easier to describe the architectural state update function as a sequence of steps, i.e., an algorithm. The below image shows the child-ILA of the AES design and also the child-program for the START_ENCRYPT instruction.
