CODEWITHSUNDEEP
hdlchiselformal-verification
FabienM
FabienM

Reputation: 3751

Formal verification with Chisel

Is it possible to do formal verification with Chisel3 HDL language? If yes, is there an open-source software to do that ? I know that we can do verilog formal verification with Yosys, but with chisel ?

Upvotes: 4

Views: 1166

Answers (4)

FabienM
FabienM

Reputation: 3751

formal verification is now integrated under chiseltest official test library.

Upvotes: 1

FabienM
FabienM

Reputation: 3751

SpaceCowboy asked the same question here. And jkoening responded it: not now but maybe it will be done.

Upvotes: 2

FabienM
FabienM

Reputation: 3751

There is a chisel package named chisel-formal now.

import chisel3.formal._

This extends Module with trait named 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)
//...
}

That allow to use assert(), assume(), cover(), past(), ... functions.

Full howto is given on github repository.

Upvotes: 1

FabienM
FabienM

Reputation: 3751

It's possible to use Yosys-smtbmc with some little hacks described here to «inject» formal properties in Verilog generated.

Upvotes: 1

Related Questions