Chisel/Firrtl Verilog 后端工作证明

Question

是否有一些内置的测试或工具用于对 chisel 或 firrtl 设计与生成的 verilog 进行形式验证？verilog 后端建立在哪些概念上？里面有什么bug吗？

Answer 1

Chisel 和 FIRRTL 中没有内置的形式验证支持。编译器或后端没有工作证明。与任何传统编译器一样，虽然我们尽最大努力捕捉并修复它们，但肯定存在错误。

我们目前正在使用Yosys在我们对 FIRRTL 代码库所做的任何更改之间对 FIRRTL 电路的几个实例执行 LEC。我想扩展形式验证的使用，以确保编译器中的各种转换不会改变它们操作的电路的语义。我们还在试验模型检查后端，以改进与形式验证工具的集成。