Chisel/Firrtl Verilog backend proof of work

Question

Is there some built in test or tools for formal verification of chisel or firrtl design vs generated verilog? On which concepts verilog backend is build? Is there any bugs in it?

Answer 1

There is no built-in formal verification support in Chisel and FIRRTL. There is no proof of work for the compiler or backend. As with any traditional compiler, there are certainly bugs although we do our best to catch and fix them.

We are currently using Yosys to perform LEC on a few instances of FIRRTL circuits between any changes we make to the FIRRTL code base. I would like to expand the use of formal verification to ensure that various transformations in the compiler do not change the semantics of the circuits upon which they operate. We are also experimenting with model checking backends to improve integration with formal verification tools.