CIRCT

Circuit IR Compilers and Tools

'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: 

AttributeMLIR TypeDescription
label::mlir::StringAttrstring attribute

Operands: 

OperandDescription
property1-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: 

AttributeMLIR TypeDescription
label::mlir::StringAttrstring attribute

Operands: 

OperandDescription
property1-bit signless integer or LTL sequence type or LTL property type

verif.clocked_assert (circt::verif::ClockedAssertOp) 

Assert that a property holds, checked on a given clock’s ticks and disabled if a given condition holds. Only supports a single clock and a single disable.

Syntax:

operation ::= `verif.clocked_assert` $property `disable` $disable `clock` $edge $clock
              (`label` $label^)? attr-dict `:` type($property)

Attributes: 

AttributeMLIR TypeDescription
edgecirct::verif::ClockEdgeAttrclock edge
label::mlir::StringAttrstring attribute

Operands: 

OperandDescription
property1-bit signless integer or LTL sequence type or LTL property type
disable1-bit signless integer
clock1-bit signless integer

verif.clocked_assume (circt::verif::ClockedAssumeOp) 

Assume that a property holds, checked on a given clock’s ticks and disabled if a given condition holds. Only supports a single clock and a single disable.

Syntax:

operation ::= `verif.clocked_assume` $property `disable` $disable `clock` $edge $clock
              (`label` $label^)? attr-dict `:` type($property)

Attributes: 

AttributeMLIR TypeDescription
edgecirct::verif::ClockEdgeAttrclock edge
label::mlir::StringAttrstring attribute

Operands: 

OperandDescription
property1-bit signless integer or LTL sequence type or LTL property type
disable1-bit signless integer
clock1-bit signless integer

verif.clocked_cover (circt::verif::ClockedCoverOp) 

Cover on the holding of a property, checked on a given clock’s ticks and disabled if a given condition holds. Only supports a single clock and a single disable.

Syntax:

operation ::= `verif.clocked_cover` $property `disable` $disable `clock` $edge $clock
              (`label` $label^)? attr-dict `:` type($property)

Attributes: 

AttributeMLIR TypeDescription
edgecirct::verif::ClockEdgeAttrclock edge
label::mlir::StringAttrstring attribute

Operands: 

OperandDescription
property1-bit signless integer or LTL sequence type or LTL property type
disable1-bit signless integer
clock1-bit signless integer

verif.cover (circt::verif::CoverOp) 

Ensure that a property can hold.

Syntax:

operation ::= `verif.cover` $property (`label` $label^)? attr-dict `:` type($property)

Attributes: 

AttributeMLIR TypeDescription
label::mlir::StringAttrstring attribute

Operands: 

OperandDescription
property1-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: 

AttributeMLIR TypeDescription
formatString::mlir::StringAttrstring attribute

Operands: 

OperandDescription
substitutionsvariadic of any type

Results: 

ResultDescription
stra 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: 

AttributeMLIR TypeDescription
async::mlir::BoolAttrbool attribute

Operands: 

OperandDescription
clock1-bit signless integer
reset1-bit signless integer

Results: 

ResultDescription
result1-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: 

ResultDescription
areEquivalent1-bit signless integer

verif.print (circt::verif::PrintOp) 

Prints a message.

Syntax:

operation ::= `verif.print` $string attr-dict

Operands: 

OperandDescription
stringa 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: 

OperandDescription
inputsvariadic of any type