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
Publish this compiler plugin locally.
# in this project
sbt publishLocalAdd 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 compileStainless 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"' compileThis 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.
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.
DAC 2024: Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once
Efficient verification of ALUs has always been a challenge. Traditionally, they are verified at a low level, leading to state space explosion for larger bit widths. We symbolically can verify ALUs for all bit widths at once. Chisel is a hardware description language embedded in Scala. Our key idea is to transform arithmetic Chisel designs into Scala software programs that simulate their behavior, then apply Stainless, a deductive formal verification tool for Scala. We validate the effectiveness by verifying dividers and multipliers in two open-source RISC-V processors, and conclude that our approach requires less manual guidance than others.