Unverified Commit 18a444da authored by Fabian Schuiki's avatar Fabian Schuiki Committed by GitHub
Browse files

Add basic linear temporal logic assertions (#3337)

Add a wrapper API around a handful of new CIRCT compiler intrinsics that
allow for FIRRTL inputs to express linear temporal logic expressions and
assert, assume, and cover operations on them. The CIRCT compiler emits
these as SVAs.

Since there are no opaque user-defined types in FIRRTL yet, the
intrinsics all use `UInt<1>` as the type for sequences and properties.
This change exposes a safe Chisel API with `Sequence` and `Property`
wrappers around the internal `UInt<1>` types.

As FIRRTL and the CIRCT compiler evolve, we'll be able to use more
strongly-typed intrinsics and later probably dedicated FIRRTL IR nodes
for this. I also expect the `circt.verif.assert` intrinsics to be
collapsed with the other assertion mechanisms in FIRRTL to provide one
uniform IR node. That's future work though. This commit just gets the
ball rolling.
parent 9ff9cac0
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment