Home

Welcome to the ILA-Modeling-Verification wiki!

---

Writing ILAs using the Python API

We will give a brief tutorial on how to write an ILA model using the Python API, with the AES example described in the arXiv paper. The below figure shows the (partially described) model of the AES ILA.

1. Create an ILA model.

  import ila 
  m = ila.Abstraction('aes')

2. Specify the set of architectural states. There are three types of state variables supported in the Python API, i.e., Boolean (bit), bit-vector (reg), and array (mem).

  AesState = m.reg('AesState', 2) % model the AesState as a 2-bit bit-vector 
  Addr = m.reg('Addr', 16)        % model the Addr as a 16-bit bit-vector 
  Length = m.reg('Length', 16)    % model the Length as a 16-bit bit-vector 
  OutData = m.reg('OutData', 8)   % model the OutData as a 8-bit bit-vector

3. Specify the set of input variables.

  InAddr = m.inp('InAddr', 16)
  InData = m.inp('InData', 8)
  Cmd = m.inp('Cmd')

4. Define the valid and fetch function.

  m.valid = (Cmd != 0) & (InAddr >= 0xFF00) & (InAddr <= 0xFF10)
  m.fetch = ila.concat([Cmd, InAddr, InData])

5. Now let's start defining the instructions. We will take the RD/WR_ADDR instruction as the example.

  % decode function
  decode_0 = (InAddr == 0xFF02) 
  % next state functions (of two state variables)
  next_addr_0 = ila.ite(Cmd == 1, InData, Addr)
  next_out_data_0 = ila.ite(Cmd == 0, Addr, 0)

6. After all instructions are specified, set the decode functions and (cumulated) next state functions to the ILA model.

  m.decode_exprs = [decode_0, decode_1, ...] % specify the list of decode functions
  m.set_next(Addr, next_addr_all)            % the next state function of Addr
  m.set_next(OutData, next_out_data_all)     % the next state function of OutData

This is a simplified tutorial, a complete ILA model of the AES accelerator can be found in AES-ILA.