是否有一些内置测试或工具用于对 chisel 或 firrtl 设计与生成的 verilog 进行形式验证？ verilog 后端是基于哪些概念构建的？有没有什么bug？
最佳答案
Chisel 和 FIRRTL 中没有内置的形式验证支持。编译器或后端没有工作量证明。与任何传统编译器一样，尽管我们尽力捕获并修复它们，但肯定存在错误。
我们目前正在使用Yosys在我们对 FIRRTL 代码库进行的任何更改之间对 FIRRTL 电路的几个实例执行 LEC。我想扩展形式验证的使用，以确保编译器中的各种转换不会改变它们所操作的电路的语义。我们还在尝试模型检查后端，以改进与形式验证工具的集成。
关于Chisel/Firrtl Verilog 后端工作证明，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/49800826/