凿子/Firrtl Verilog后端工作证明

Question

是否有一些内置的测试或工具，用于对凿子或firrtl设计与生成的verilog进行正式验证？verilog后端构建在哪些概念上？里面有虫子吗？

Answer 1

在Chisel和FIRRTL中没有内置的正式验证支持。编译器或后端没有工作证明。与任何传统的编译器一样，虽然我们尽力捕捉并修复它们，但仍然存在bug。

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

Answer 2

从FIRRTLv1.4和Chiselv3.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