This is the ILA model database, archiving the ILA models and the verification scripts.
- 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
- LMAC: LeWiz Communications Ethernet MAC.
- AXI: OH! Implementation, it also includes the protocol verification
- Off-chip: BaseJump Implementation
- [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
- 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
- Please ensure all commited files follow the MIT License requirements.
- Please properly categorize the design and provide scripts for setting up/reproducing the case study in
scripts/ci
. - 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