使用 Chisel 进行形式化验证

Question

是否可以用Chisel3 HDL语言做形式化验证？如果是，是否有开源软件可以做到这一点？我知道我们可以用 Yosys 做 verilog 形式验证，但是用 chisel ?

Answer 1

SpaceCowboy 问了同样的问题。 jkoening回应说：不是现在，但也许会完成。

Answer 2

可以使用 Yosys-smtbmc 和描述的一些小技巧 here 在生成的 Verilog 中“注入”正式属性。

Answer 3

现在有一个名为chisel-formal的凿子包。

import chisel3.formal._

这扩展了具有名为 Formal 特征的模块。

class MyModule extends Module with Formal {
//...
      past(io.Mwrite, 1) (pMwrite => {
        when(io.Mwrite === true.B) {
          assert(pMwrite === false.B)
        }
      })
      cover(countreg === 10.U)
//...
}

允许使用 assert()、assume()、cover()、past() 等函数。

github repository.

上给出了完整的指南

Answer 4

正式验证现在集成在 chiseltest 官方测试库下。

使用 Chisel 进行形式化验证

Formal verification with Chisel

hdl

chisel

formal-verification