This is the ILA model database, archiving the ILA models and the verification scripts.

IMDb_Archive

Content

Accelerators

• AES: ILA model of the AES (Advanced Encryption Standard) accelerator.
• SHA: ILA model of the SHA (Secure Hash Algorithm) accelerator.
• FLEXNLP: ILA model of the FlexASR accelerator (all rights reserved - Harvard University).
• HLS-CNN: This is the ILA model of HLSCNN accelerator (all right reserved - Harvard University)
• VTA: ILA model of the Versatile Tensor Accelerator (VTA)
• GB: ILA model of the Gaussian Blurr Accelerator (GB)
• RBM: ILA model of the Restricted Boltzman Machine Accelerator (RBM)
• NVDLA: ILA model of the NVDLA Accelerator

Communication

• LMAC: LeWiz Communications Ethernet MAC.
• AXI: OH! Implementation, it also includes the protocol verification
• Off-chip: BaseJump Implementation

Cores

• [RISC-V]
• Pico: The PicoRISCV processor, simple core without pipeline
• Piccolo: The Piccolo processor with pipepines.
• Rocket: Rocket Processor
• PTX: ILA model of the Nvidia GPU PTX ISA.
• Nibber: ILA verification of a SIMD Processor
• 8051: ILA model of the Intel 8051 micro-processor

Others

• FIFO-BMC demonstrates the bounded model checking (BMC) capability of ILAng using a FIFO example.
• Cache Coherence: OpenPiton Implementation, we also verifies cache coherence protocol under this repo.
• Memory Controller: ILA model of the Garnet Memory Controller

Contribute

1. Please ensure all commited files follow the MIT License requirements.
2. Please properly categorize the design and provide scripts for setting up/reproducing the case study in scripts/ci.
3. Please test and make sure your model works (at least) under the below environment:

Environment:

• Ubuntu 18.04 LTS (Bionic)
• gcc 7.4.0
• Python 2.7
• boost 1.65.1
• z3 4.4.1
• bison 3.0.4
• flex 2.6.0
• ILAng (0.9.1 or above)

A docker image with the above configuration can be pulled by:

docker pull byhuang/ilang:IMDb-ci