This is tool developed at Princeton that targets generating architecture-level models(ISA) for hardware directly from its RTL code. The user only needs to provide information for how to use this hardware(see tutorials below), then an architecture-level model (in the format of LLVM IR) can be automatically generated. Techniques used in this project includes model checking, symbolic execution, program optimization, etc. Several softwares are also used: LLVM, JasperGold, Z3. The generated models can be used for several applications. For example, if used for functional simulation, the simulation speed is 4~20 times faster compared with RTL simulation using Verilator. We are now actively working on other interesting applications. Stay tuned!
There have been two papers published related to this tool: DATE'22, ICCAD'21
This repository contains code for automatically generate architecture-level(ISA) models from RTL There are mainly two steps:
- Determine architecture-level registers in RTL
- Generate the register update function (instruction semantics) for each instruction from RTL
Two algorithms for step 1 is provided, in directory "write_taint" and "live_analysis". You can find a tutorial for how to use the live_analysis algorithm here
Another tutorial for step 2 is here
There is a docker image here If you want to install locally, please follow the steps below in the order.
Google glog, version: v0.5.0-rc2-2-g8d40d75
boost, should be compatible with the latest version
cd ./src/live_analysis; mkdir build; cd build; cmake ..; make
Should be able to see libTaintGenLib.a and taint_gen in the build folder
The build process of func_extract depends on the libTaintGenLib.a generated in the last step.
z3, version: 4.8.8
llvm, the link is for the specific commit we used: 22f00f61dd5483a9fdaed3b7592d392c23b3646a
cd ./src/func_extract; mkdir build; cd build; cmake ..; make
should be able to see: cmp func_extract libFuncExtractLib.a sim_gen tb_gen test_gen
If you have any problems, please submit an issue, or contact Yu Zeng: [email protected]