CODEWITHSUNDEEP
chisel
SpaceCowboy max
SpaceCowboy max

Reputation: 137

Chisel/Firrtl Verilog backend proof of work

Is there some built in test or tools for formal verification of chisel or firrtl design vs generated verilog? On which concepts verilog backend is build? Is there any bugs in it?

Upvotes: 5

Views: 893

Answers (2)

alcorn
alcorn

Reputation: 1368

As of FIRRTL v1.4 and Chisel v3.4, there will be basic support for verification primitives.

If you import chisel3.experimental.verification you'll get assert, assume and cover, which generate their corresponding constructs in Verilog.

import chisel3.experimental.{verification => v}

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

Note that this is a fairly low-level interface. I'm currently working on a helper library to make formal verification in Chisel more approachable: https://github.com/tdb-alcorn/chisel-formal

Upvotes: 2

Jack Koenig
Jack Koenig

Reputation: 6064

There is no built-in formal verification support in Chisel and FIRRTL. There is no proof of work for the compiler or backend. As with any traditional compiler, there are certainly bugs although we do our best to catch and fix them.

We are currently using Yosys to perform LEC on a few instances of FIRRTL circuits between any changes we make to the FIRRTL code base. I would like to expand the use of formal verification to ensure that various transformations in the compiler do not change the semantics of the circuits upon which they operate. We are also experimenting with model checking backends to improve integration with formal verification tools.

Upvotes: 5

Related Questions