Chisel/Firrtl Verilog 后端工作证明答案

【问题标题】：Chisel/Firrtl Verilog backend proof of workChisel/Firrtl Verilog 后端工作证明
【发布时间】：2018-04-12 15:46:48
【问题描述】：

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

【问题讨论】：

标签： chisel

【解决方案1】：

从 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)
}

请注意，这是一个相当低级的接口。我目前正在开发一个帮助程序库，以使 Chisel 中的形式验证更加平易近人：https://github.com/tdb-alcorn/chisel-formal

【讨论】：

【解决方案2】：

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

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

【讨论】：