This is the ILA model database, archiving the ILA models and the verification scripts.
- AES is a documented tutorial for ILA-based behavioral equivalence checking.
- FIFO-BMC demonstrates the bounded model checking (BMC) capability of ILAng using a FIFO example.
- LMAC: LeWiz Communications Ethernet MAC.
- 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