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