Chicala

Chicala is a Chisel to Scala Translator. It uses a Scala compiler plugin to translate Chisel hardware design code to Scala simulation code. This translation alows us to use software verification technology on the Scala code to varify the Chisel hardware design, and use Chisel level information to improve the verification, such as parameter and structure information.

We verified arithmetic Chisel designs through this translation using Stainless. Parameter information allows us to prove all different bit widths at once, and structure information provides convenience for the proof. For more details, see our paper in DAC24:
Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once

Usage

Publish this compiler plugin locally.

# in this project
sbt publishLocal

Add the compiler plugin to your Chisel program. In your build.sbt add:

addCompilerPlugin("cn.ac.ios.tis" %% "chicala" % "0.1.0-SNAPSHOT")

Compile your Chisel program. The translated Scala code for Stainless will be put in <your-chisel-project-dir>/test_run_dir/chiselToScala.

# in your chisel project
sbt compile

Stainless version Scala codes are not able to run simulations due to some type conversion issues. We also support generating simulation-capable Scala codes by adding a scalacOptions or compiling your Chisel project by:

# in your chisel project
sbt 'set scalacOptions+="-P:chicala:simulation:true"' compile

This tool is developed based on Chisel3.5.6 and only supports limited keywords and structures.

Dependency libraries for translated code can be found in divider-stainless/stain/src/main/scala/verify/libraryUInt for Stainless and chicala-soundness/src/main/scala/librarySimUInt for simulation.

Examples

Run make test to see how this tool translates hardware designs in ./testcase.

For verification with Stainless, see our proof project.

For simulation, see the project where we compare the simulation results of our Scala code and ChiselTest.