'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 (`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 |
verif.assume
(circt::verif::AssumeOp) ¶
Assume that a property holds.
Syntax:
operation ::= `verif.assume` $property (`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 |
verif.cover
(circt::verif::CoverOp) ¶
Ensure that a property can hold.
Syntax:
operation ::= `verif.cover` $property (`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 |
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.yield
(circt::verif::YieldOp) ¶
Yields values from a region
Syntax:
operation ::= `verif.yield` ($inputs^ `:` type($inputs))? attr-dict
Traits: HasParent<verif::LogicEquivalenceCheckingOp>
, Terminator
Operands: ¶
Operand | Description |
---|---|
inputs | variadic of any type |