Chisel/Firrtl Verilog 后端工作证明

Question

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

Answer 1

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

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