Chisel/Firrtl Verilog 后端工作证明

Question

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

Answer 1

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

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

Answer 2

从 FIRRTL v1.4 和 Chisel v3.4 开始，将基本支持验证原语。

如果您导入 chisel3.experimental.verification，您将得到 assert、assume 和 cover，它们会在 Verilog 中生成相应的结构。

import chisel3.experimental.{verification => v}

class Foo extends Module {
  val predicate: Bool
  v.assert(predicate)
}

请注意，这是一个相当 low-level 的界面。我目前正在开发一个帮助程序库，以使 Chisel 中的形式验证更容易上手：https://github.com/tdb-alcorn/chisel-formal

Chisel/Firrtl Verilog backend proof of work