'verif' Dialect
This dialect provides a collection of operations to express various verification concerns, such as assertions and interacting with a piece of hardware for the sake of verifying its proper functioning.
Operations ¶
verif.assert
(circt::verif::AssertOp) ¶
Assert that a property holds.
Syntax:
operation ::= `verif.assert` $property (`if` $enable^)? (`label` $label^)? attr-dict `:` type($property)
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
label | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
property | 1-bit signless integer or LTL sequence type or LTL property type |
enable | 1-bit signless integer |
verif.assume
(circt::verif::AssumeOp) ¶
Assume that a property holds.
Syntax:
operation ::= `verif.assume` $property (`if` $enable^)? (`label` $label^)? attr-dict `:` type($property)
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
label | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
property | 1-bit signless integer or LTL sequence type or LTL property type |
enable | 1-bit signless integer |
verif.bmc
(circt::verif::BoundedModelCheckingOp) ¶
Perform a bounded model check
Syntax:
operation ::= `verif.bmc` `bound` $bound `num_regs` $num_regs attr-dict-with-keyword `init` $init `loop` $loop `circuit`
$circuit
This operation represents a bounded model checking problem explicitly in
the IR. The bound
attribute indicates how many times the circuit
region
should be executed, and num_regs
indicates the number of registers in the
design that have been externalised and appended to the region’s
inputs/outputs (these values are fed from each circuit
region execution
to the next, as they represent register state, rather than being
overwritten with fresh variables like other inputs). The circuit
region
contains the circuit (alongside the verif
property checking operations)
to be checked.
The init
region contains the logic to initialize the clock signals, and
will be executed once before any other region - it cannot take any
arguments, and should return as many !seq.clock
values as the circuit
region has !seq.clock
arguments, followed by any initial arguments of
‘state’ arguments to be fed to the loop
region (see below).
The loop
region contains the logic to advance the clock signals, and will
be executed after each execution of the circuit
region. It should take as
arguments as many !seq.clock
values as the circuit
region has, and
these can be followed by additional ‘state’ arguments to represent e.g.
which clock should be toggled next. The types yielded should be the same,
as this region yields the updated clock and state values (this should also
match the types yielded by the init
region).
Traits: IsolatedFromAbove
, SingleBlockImplicitTerminator<verif::YieldOp>
, SingleBlock
Interfaces: InferTypeOpInterface
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
bound | ::mlir::IntegerAttr | 32-bit signless integer attribute |
num_regs | ::mlir::IntegerAttr | 32-bit signless integer attribute |
Results: ¶
Result | Description |
---|---|
result | 1-bit signless integer |
verif.clocked_assert
(circt::verif::ClockedAssertOp) ¶
Assert that a property holds, checked on a given clock’s ticks and enabled if a given condition holds. Only supports a single clock and a single disable.
Syntax:
operation ::= `verif.clocked_assert` $property (`if` $enable^)? `,` $edge $clock
(`label` $label^)? attr-dict `:` type($property)
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
edge | circt::verif::ClockEdgeAttr | clock edge |
label | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
property | 1-bit signless integer or LTL sequence type or LTL property type |
clock | 1-bit signless integer |
enable | 1-bit signless integer |
verif.clocked_assume
(circt::verif::ClockedAssumeOp) ¶
Assume that a property holds, checked on a given clock’s ticks and enabled if a given condition holds. Only supports a single clock and a single disable.
Syntax:
operation ::= `verif.clocked_assume` $property (`if` $enable^)? `,` $edge $clock
(`label` $label^)? attr-dict `:` type($property)
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
edge | circt::verif::ClockEdgeAttr | clock edge |
label | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
property | 1-bit signless integer or LTL sequence type or LTL property type |
clock | 1-bit signless integer |
enable | 1-bit signless integer |
verif.clocked_cover
(circt::verif::ClockedCoverOp) ¶
Cover on the holding of a property, checked on a given clock’s ticks and enabled if a given condition holds. Only supports a single clock and a single disable.
Syntax:
operation ::= `verif.clocked_cover` $property (`if` $enable^)? `,` $edge $clock
(`label` $label^)? attr-dict `:` type($property)
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
edge | circt::verif::ClockEdgeAttr | clock edge |
label | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
property | 1-bit signless integer or LTL sequence type or LTL property type |
clock | 1-bit signless integer |
enable | 1-bit signless integer |
verif.concrete_input
(circt::verif::ConcreteInputOp) ¶
Declare a concrete input for formal verification
Syntax:
operation ::= `verif.concrete_input` $init `,` $update attr-dict `:` type($result)
This operation declares a concrete input that can then be used in the
reasoning surrounding symbolic inputs, allowing for a form of concolic
reasoning to take place in a verif.formal
block. Concrete inputs are
defined by an initial value and an update SSA value. This is equivalent
to a register with the parent verif.formal
’s implicit clock, which is
initialized with the init value and obtains a new value every implicit
clock tick from the update value.
Traits: HasParent<verif::FormalOp>
Interfaces: InferTypeOpInterface
Operands: ¶
Operand | Description |
---|---|
init | any type |
update | any type |
Results: ¶
Result | Description |
---|---|
result | any type |
verif.cover
(circt::verif::CoverOp) ¶
Ensure that a property can hold.
Syntax:
operation ::= `verif.cover` $property (`if` $enable^)? (`label` $label^)? attr-dict `:` type($property)
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
label | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
property | 1-bit signless integer or LTL sequence type or LTL property type |
enable | 1-bit signless integer |
verif.formal
(circt::verif::FormalOp) ¶
Defines a formal verification test
Syntax:
operation ::= `verif.formal` $sym_name `(``k` `=` $k `)` attr-dict-with-keyword
$test_region
This operation defines a formal verification test. This should be written
by declaring symbolic values that are then connected to a hardware instance.
These symbols can then be used in additional assertions that are defined
outside of the instantiated hw.module
but inside of this region.
Assertions/Assumptions defined within the instantiated module will also be
used for verification. The region can then be converted into btor2,
SystemVerilog, or used for verification directly in circt-bmc. The operations
in this region are ignored during regular SystemVerilog emission. This allows
for verification specific logic to be isolated from the design in a way that
is similar to layers.
The attribute k
defines the upper bound of cycles to check for this test
w.r.t. the implicit clock defined by this operation within its region.
Traits: HasParent<mlir::ModuleOp>
, IsolatedFromAbove
, NoTerminator
Interfaces: RegionKindInterface
, Symbol
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
sym_name | ::mlir::StringAttr | string attribute |
k | ::mlir::IntegerAttr | arbitrary integer attribute |
verif.format_verilog_string
(circt::verif::FormatVerilogStringOp) ¶
Creates a formatted string.
Syntax:
operation ::= `verif.format_verilog_string` $formatString `(` $substitutions `)` `:` type($substitutions) attr-dict
Creates a formatted string suitable for printing via the verif.print
op.
The formatting syntax is expected to be identical to verilog string
formatting to keep things simple for emission.
If we in the future would like to be less tied to verilog formatting,
please ask your friendly neighbourhood compiler engineer to e.g. implement
a FormatStringOp
which itself may lower to a FormatVerilogStringOp
.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
formatString | ::mlir::StringAttr | string attribute |
Operands: ¶
Operand | Description |
---|---|
substitutions | variadic of any type |
Results: ¶
Result | Description |
---|---|
str | a HW string |
verif.has_been_reset
(circt::verif::HasBeenResetOp) ¶
Check that a proper reset has been seen.
Syntax:
operation ::= `verif.has_been_reset` $clock `,` custom<KeywordBool>($async, "\"async\"", "\"sync\"")
$reset attr-dict
The result of verif.has_been_reset
reads as 0 immediately after simulation
startup and after each power-cycle in a power-aware simulation. The result
remains 0 before and during reset and only switches to 1 after the reset is
deasserted again.
This is a useful utility to disable the evaluation of assertions and other verification constructs in the IR before the circuit being tested has been properly reset. Verification failures due to uninitialized or randomized initial state can thus be prevented.
Using the result of verif.has_been_reset
to enable verification is more
powerful and proper than just disabling verification during reset. The
latter does not properly handle the period of time between simulation
startup or power-cycling and the start of reset. verif.has_been_reset
is
guaranteed to produce a 0 value in that period, as well as during the reset.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
async | ::mlir::BoolAttr | bool attribute |
Operands: ¶
Operand | Description |
---|---|
clock | 1-bit signless integer |
reset | 1-bit signless integer |
Results: ¶
Result | Description |
---|---|
result | 1-bit signless integer |
verif.lec
(circt::verif::LogicEquivalenceCheckingOp) ¶
Represents a logical equivalence checking problem
Syntax:
operation ::= `verif.lec` attr-dict `first` $firstCircuit `second` $secondCircuit
This operation represents a logic equivalence checking problem explicitly in the IR. There are several possiblities to perform logical equivalence checking. For example, equivalence checking of combinational circuits can be done by constructing a miter circuit and testing whether the result is satisfiable (can be non-zero for some input), or two canonical BDDs could be constructed and compared for identity, etc.
The number and types of the inputs and outputs of the two circuits (and thus also the block arguments and yielded values of both regions) have to match. Otherwise, the two should be considered trivially non-equivalent.
Traits: IsolatedFromAbove
, SingleBlockImplicitTerminator<verif::YieldOp>
, SingleBlock
Interfaces: InferTypeOpInterface
Results: ¶
Result | Description |
---|---|
areEquivalent | 1-bit signless integer |
verif.print
(circt::verif::PrintOp) ¶
Prints a message.
Syntax:
operation ::= `verif.print` $string attr-dict
Operands: ¶
Operand | Description |
---|---|
string | a HW string |
verif.symbolic_input
(circt::verif::SymbolicInputOp) ¶
Declare a symbolic input for formal verification
Syntax:
operation ::= `verif.symbolic_input` attr-dict `:` type($result)
This operation declares a symbolic input that can then be used to reason
about hw.instance
inputs in a symbolic manner in assertions and
assumptions. The result type must be explicitly marked. The resulting value
is a new non-deterministic value for every clock cycle of the implicit clock
defined by the parent verif.formal
.
Traits: HasParent<verif::FormalOp>
Results: ¶
Result | Description |
---|---|
result | any type |
verif.yield
(circt::verif::YieldOp) ¶
Yields values from a region
Syntax:
operation ::= `verif.yield` ($inputs^ `:` type($inputs))? attr-dict
Traits: HasParent<verif::LogicEquivalenceCheckingOp, verif::BoundedModelCheckingOp>
, Terminator
Operands: ¶
Operand | Description |
---|---|
inputs | variadic of any type |