PIR Dialect

This dialect provides operations and types that fully encode SystemVerilog Assertions (SVA), in a manner that provides interoperation with Yosys’s internal SVA support.

Rationale ¶

Temporal logic is highly used across hardware verification to properly specify hardware designs. This can be found in many forms but the most common is SystemVerilog Assertions (SVA), which is a sub-language in SystemVerilog that allows for properties and sequences, i.e. predicates that require more than one cycle to evaluate. While this language exists and is mimicked in many front-ends, it’s back-end support is often limited to either commercial tools or adhoc support for a minimal subset in open-source tools.

This is where Property IR (PIR) comes in. The goal of PIR is to support formal verification flows, while decoupling front-end tasks (parsing, name resolution, etc.) from checker circuit synthesis and optimization. This is achieved by providing a unified representation for assertions, automata, and circuits. This means that PIR acts as a proper intermediate representation for manipulating and lowering SVA properties and sequences end-to-end. Unlike other dialects like verif or ltl, pir aims to fully encode and support all of SVA, as defined in the IEEE specification. Not only that, but PIR is designed and developed to share infrastructure and interoperate between CIRCT and Yosys. This allows CIRCT to gain access to the much more developed SVA support in Yosys while also allowing Yosys to gain access to all of CIRCT’s front-ends and core optimizations. As such this dialect acts both as a an interface for interoperating with Yosys’ SVA tooling, and as a full Abtract Syntax Tree for encoding SVA.

The property IR flow looks as follows:

  |------------------|
  | CIRCT Frontends  |
  |------------------|    |------------|
            |-----------> | CIRCT PIR  |
                          |------------|     |------------|
                                + ---------> | Yosys PIR  |
                          |------------|     |------------|        
                          | CIRCT Core |           |
                          |------------|           v
                                ^            |----------------------------| ---¬
                                |            | Yosys PIR automaton model  | <--|
                                |            |----------------------------| 
                                |                  |
                                |                  v
                                |            |----------------------------|
                                |------------| Yosys PIR Checker circuit  | 
                                             |----------------------------|       

Structure of PIR Property ¶

The general structure of a PIR block is a a pir.cell, which represents a property being asserted, assumed, cover, etc. which can have inputs that represent signals which it inherits from outside of the cell (by default it is isolated), and a top-level pir.assert_property, pir.assume_property, pir.coover_property, or pir.restrict_property.

Unlike in other interpretations of SVA, PIR follows a strict typing isolation where there is no inherit hierarchy between the types. For example in ltl, !ltl.property > !ltl.sequence > i1 so a boolean is a sequence which itself is a property. In pir, explicit casts or clocking operations are needed to move between types, e.g. !pir.sequence must be explicitly clocked to become a !pir.clocked_sequence, same for !pir.property and !pir.clocked_property, and of course i1 to any clocked expression. This reduces the amount of analyses required, and potential inference, to retrieve information as a !pir.clocked_property will always be explicitly tied to a clock somewhere. This same reasoning is why all assertlike operations only accept !pir.clocked_property as their inputs.

Here’s an example of how an SVA property gets encoded in PIR: Given a SystemVerilog property to assert:

prop_ assert property (a ##1 b |-> always(c))

this becomes the following textual property IR (s-expressions):

(documnent
  (declare-input a)
  (declare-input b)
  (declare-input c)
  (declare prop 
    (clk-prop-overlapped-implication
      (clk-seq-concat
        (clk-seq-bool a)
        (clk-seq-bool b)
      )
      (clk-prop-always
        (clk-prop-bool c)
      )
    )
  )
  (assert-property prop)
)

which is equivalent to the following pir dialect:

pir.cell @prop {} {
  %a, %b, %c = pir.input : i1, i1, i1
  %clk_s_a = pir.bool_to_clocked_seq %a
  %clk_s_b = pir.bool_to_clocked_seq %b
  %clk_p_c = pir.bool_to_clocked_prop %c

  %aconcatb = pir.concat %clk_s_a, %clk_s_b 
  %always_c = pir.always %clk_p_c
  %prop = pir.overlapped_implication %aconcatb, %always_c 

  pir.assert_property %prop : !pir.clocked_property
}

This is a simple example but shows the general structure of a PIR property. Assert-like operations function as terminators for a cell’s region, meaning that each property should exist within its own cell. Note that by default, type conversions will tie a property or sequence to the global clock, that is, the clock defined by the steps taken by a model checker. This is what distinguishes “clocking operations” with “type conversion operations”. A neat addition is that the type signature in the pretty printed mlir assembly can be omitted in most cases since all of the operations only accept a single type of operand.
The general structure is close enough to actual SVA to make a much cleaner interface than ltl, which should be used as a core dialect and not an interfacing dialect.

Enums ¶

Types ¶

ClockedPropertyType ¶

Clocked Property IR Property

Syntax: !pir.clocked_property

Represents a clocked property (in the SVA sense). This means that it is bound to an explicit clock. These can be rewritten as simple properties by encoding the clock as an explicit state that depends on the global clock, and having updates for the clocked property wait on the that state holding to be sampled.

ClockedSequenceType ¶

Clocked Sequence IR Sequence

Syntax: !pir.clocked_sequence

Represents a clocked sequence (in the SVA sense). This means that it is bound to an explicit clock. These can be rewritten as simple sequences by encoding the clock as an explicit state that depends on the global clock, and having updates for the clocked sequence wait on the that state holding to be sampled.

PropertyType ¶

Simple Property IR Property

Syntax: !pir.property

Represents a property (in the SVA sense) that is simple. This means that is only bound to the global clock, i.e. the one whose ticks represent the steps of the model checker used to prove this property. This should not be explicitly bound to any local clock. Additionally simple properties must not contain any subsequences that admit empty matches.

SequenceType ¶

Simple Property IR Sequence

Syntax: !pir.sequence

Represents a sequence (in the SVA sense) that is simple. This means that is only bound to the global clock, i.e. the one whose ticks represent the steps of the model checker used to prove this property. This should not be explicitly bound to any local clock.

Operations ¶

pir.assert_property (circt::pir::AssertPropertyOp) ¶

Assert that a Property IR property holds.

Syntax:

operation ::= `pir.assert_property` $property ($scope^)? (`disable` `iff` $disable^)? (`on` $enable^)? attr-dict `:` type($property)

Concurrent assertion that checks if the current property holds. This only accepts clocked properties, thus all other types must be explicitly casted to a clocked property, using an appropriate type conversion operation, before they can be asserted.

Traits: AttrSizedOperandSegments

Attributes: ¶

Operands: ¶

pir.assume_property (circt::pir::AssumePropertyOp) ¶

Assumes that a Property IR property holds.

Syntax:

operation ::= `pir.assume_property` $property ($scope^)? (`disable` `iff` $disable^)? (`on` $enable^)? attr-dict `:` type($property)

Concurrent assumption that checks if the current property holds. This only accepts clocked properties, thus all other types must be explicitly casted to a clocked property, using an appropriate type conversion operation, before they can be assumed. Concurrent assumptions are treated alongside assertions without directly impacting their timing. As such if an assumption turns out to not hold, then ongoing assertions that depend on it will be disabled as the assumed property terminates.

Traits: AttrSizedOperandSegments

Attributes: ¶

Operands: ¶

pir.bool_to_clocked_prop (circt::pir::BoolToClockedPropOp) ¶

Convert a Boolean expression to a clocked property of length 1.

Syntax:

operation ::= `pir.bool_to_clocked_prop` $input attr-dict

Converts a Boolean expression directly to a sequence property. Note that sequence properties must not admit empty matches.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: ¶

Results: ¶

pir.bool_to_clocked_seq (circt::pir::BoolToClockedSeqOp) ¶

Convert a Boolean expression to a clocked sequence of length 1.

Syntax:

operation ::= `pir.bool_to_clocked_seq` $input attr-dict

Converts a Boolean expression to a clocked sequence of length 1. In SystemVerilog, there exists no equivalent operator because this happens implicitly by using a Boolean expression in a sequence context. This uses the global clock.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: ¶

Results: ¶

pir.cell (circt::pir::CellOp) ¶

PIR Wrapper Cell for Properties and Sequences.

Syntax:

operation ::= `pir.cell` $sym_name $parameters attr-dict-with-keyword $body

Wrapper cell which encapsulates all of the logic related to a specific property or sequence. This allows PIR properties to be both well contained and exist within any other dialect. When interoperating with Yosys, the contents of a cell will be the only information shared with Yosys infrastructure.

Traits: IsolatedFromAbove, NoRegionArguments, NoTerminator, SingleBlock, SymbolName, SymbolVisibility

Interfaces: RegionKindInterface, Symbol

Attributes: ¶

pir.clocked (circt::pir::ClockedOp) ¶

Specify the clock of a clocked operation.

Syntax:

operation ::= `pir.clocked` $clock `,` $input attr-dict `:` qualified(type($clock)) `,` qualified(type($input))

Specifies the clock for a given clocked sequence or clocked property. Note that these must be converted into a “clocked” type before being given a specific clock.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: ¶

Results: ¶

pir.clocked_seq_to_clocked_prop (circt::pir::ClockedSeqToClockedPropOp) ¶

Converts a clocked sequence to sequence property.

Syntax:

operation ::= `pir.clocked_seq_to_clocked_prop` $input attr-dict

Converts a clocked sequence to sequence property using the same clock.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: ¶

Results: ¶

pir.cover_property (circt::pir::CoverPropertyOp) ¶

Cover-point that tracks how often a property holds.

Syntax:

operation ::= `pir.cover_property` $property ($scope^)? (`disable` `iff` $disable^)? (`on` $enable^)? attr-dict `:` type($property)

Tracks how often a concurrent property holds. Will yeald a coverage report in the end. Mostly makes sense in the context of finite traces, e.g. simulation.

Traits: AttrSizedOperandSegments

Attributes: ¶

Operands: ¶

pir.gclk_future (circt::pir::GlobalClockFutureOp) ¶

Samples the value of the input at the next gobal time step.

Syntax:

operation ::= `pir.gclk_future` $input attr-dict

Samples the value of the input at the next gobal time step. This allows us e.g. to model any clock in terms of the global clock. Note that the three other global clock sampling methods can also be modeled using future sampling as follows:

%res = pir.glck_sample posedge %clk_v, %clk_d : i1 

// is equivalent to:

%0 = comb.and bin %clk_v, %clk_d : i1
%true = hw.constant true
%1 = comb.xor bin %0, %true : i1
%2 = pir.gclk_future %0 : i1
%res = comb.and bin %2, %1 : i1

// -----

%res = pir.glck_sample negedge %clk_v, %clk_d : i1 

// is equivalent to:

%true = hw.constant true
%n_clk_v = comb.xor bin %clk_v, %true : i1
%0 = comb.and bin %n_clk_v, %clk_d : i1
%1 = comb.xor bin %0, %true : i1
%2 = pir.gclk_future %0 : i1
%res = comb.and bin %2, %1 : i1

// -----

%res = pir.glck_sample edge %clk_v, %clk_d : i1 

// is equivalent to:

%f0 = gclk_future %clk_v : i1
%f1 = gclk_future %clk_d : i1
%0 = comb.xor bin %clk_v, %f0 : i1
%1 = comb.xow bin %clk_d, %1 : i1
%res = comb.or bin %0, %1 : i1

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: ¶

Results: ¶

pir.gclk_sample (circt::pir::GlobalClockSampleOp) ¶

Samples the input with respect to the global clock.

Syntax:

operation ::= `pir.gclk_sample` $edge $clockValue (`,` $clockDefined^)? attr-dict

Samples a given input signal with respect to the global clock on a given clock edge. This is useful when encoding other clocks through their relation to the global clock.

Additionally, the two arguments of this operation are used to represent clocks that might have undefined traces, i.e. moments where the clocks evaluate to either x or z. These arguments are used as follows:

operand[0] | operand[1] | result ¶

    0    |     1      |    0
    1    |     1      |    1
    0    |     0      |    z
    1    |     0      |    x

Operand[0] is referred to as “clock_value” as it carries the value of the clock, while operand[1] is referred to as “clock_defined” as it specifies whether the clock is currently in an undefined state.

Clock_defined can be omitted, in which case it is interpreted as a constant 1.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes: ¶

Operands: ¶

Results: ¶

pir.input (circt::pir::InputOp) ¶

Defines the inputs to a PIR Cell.

Syntax:

operation ::= `pir.input` `` custom<ImplicitSSANames>($names) attr-dict `:` type($results)

Defines the inputs to a PIR Cell as a single variadic symbolic value. This can of course also be used to model non-determinism or ANY_SEQ macros from YOSYS produced SystemVerilog into CIRCT, e.g.

pir.cell @prop1 {
  %a, %b, %c = pir.input : i1, i8, i8
}

In the example above, the inputs a, b, and c can then be used to reference signals from the surrounding design in a manner that allows the logic of the property to remain isolated from the logic of the design under verification (DUV).

Traits: SameVariadicResultSize

Interfaces: OpAsmOpInterface

Attributes: ¶

Results: ¶

pir.restrict (circt::pir::RestrictOp) ¶

Restricts the input space checked for a given property.

Syntax:

operation ::= `pir.restrict` $property ($scope^)? (`disable` `iff` $disable^)? (`on` $enable^)? attr-dict `:` type($property)

Similarly to Assumptions, restrictions allow for a property’s input space to be constrained. They differ mainly in simulation semantics, where an assumption must be checked before it is applied, a restriction is just applied regardless of its validity. Restrict is identical to assume in the context of formal verification.

Traits: AttrSizedOperandSegments

Attributes: ¶

Operands: ¶

pir.seq_to_clocked_seq (circt::pir::SeqToClockedSeqOp) ¶

Convert a simple sequence into a clocked sequence.

Syntax:

operation ::= `pir.seq_to_clocked_seq` $input attr-dict

Convert a simple sequence into a clocked sequence that uses the global clock. Then it can be used as a parameter for assertions. Note that it is not possible to change the clock that is used by the resulting clocked sequence.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: ¶

Results: ¶