CIRCT

Circuit IR Compilers and Tools

'synth' Dialect

Synthesis dialect for logic synthesis operations

The Synth dialect provides operations and types for logic synthesis, including meta operations for synthesis decisions, logic representations like AIG, and synthesis pipeline infrastructure.

Operations

synth.aig.and_inv (::circt::synth::aig::AndInverterOp)

AIG dialect AND operation

Syntax:

operation ::= `synth.aig.and_inv` custom<VariadicInvertibleOperands>($inputs, type($result), $inverted, attr-dict)

The synth.aig.and_inv operation represents an And-Inverter in the AIG dialect. Unlike comb.and, operands can be inverted respectively.

Example:

  %r1 = synth.aig.and_inv %a, %b: i3
  %r2 = synth.aig.and_inv not %a, %b, not %c : i3
  %r3 = synth.aig.and_inv not %a : i3

Traditionally, an And-Node in AIG has two operands. However, synth.aig.and_inv extends this concept by allowing variadic operands and non-i1 integer types. Although the final stage of the synthesis pipeline requires lowering everything to i1-binary operands, it’s more efficient to progressively lower the variadic multibit operations.

Variadic operands have demonstrated their utility in low-level optimizations within the comb dialect. Furthermore, in synthesis, it’s common practice to re-balance the logic path. Variadic operands enable the compiler to select more efficient solutions without the need to traverse binary trees multiple times.

The ability to represent multibit operations during synthesis is crucial for scalability. This approach enables a form of vectorization, allowing for batch processing of logic synthesis when multibit operations are constructed in a similar manner.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

AttributeMLIR TypeDescription
inverted::mlir::DenseBoolArrayAttri1 dense array attribute

Operands:

OperandDescription
inputsvariadic of any type

Results:

ResultDescription
resultany type

synth.choice (::circt::synth::ChoiceOp)

Synth choice operation

Syntax:

operation ::= `synth.choice` $inputs attr-dict `:` type($result)

The synth.choice operation represents a set of structurally equivalent choices, corresponding to the choice nodes introduced in “Reducing Structural Bias in Technology Mapping” (ICCAD 2005, S. Chatterjee et al.).

A compiler may assume all operands are equivalent and replace the operation with any one of them at any point in the pipeline.

Example:

  %r1 = synth.choice %a, %b : i1
  %r2 = synth.choice %a, %b, %c : i16

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

OperandDescription
inputsvariadic of any type

Results:

ResultDescription
resultany type

synth.dot (::circt::synth::DotOp)

Ordered 3-input DOT gate with invertible inputs

The synth.dot operation represents the ordered three-input Boolean function x xor (z or (x and y)), applied after optional per-input inversion.

Unlike common AND, OR, XOR, and majority gates, synth.dot is not permutation-invariant: its operands play distinct roles in the Boolean expression. Dot gates are known to be a promising intermediate representation for area optimization, as discussed in “Three-Input Gates for Logic Synthesis” (Dewmini Sudara Marakkalage et al., TCAD 2021).

Example:

  %r0 = synth.dot %x, %y, %z : i1
  %r1 = synth.dot not %x, %y, not %z : i8

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

AttributeMLIR TypeDescription
inverted::mlir::DenseBoolArrayAttri1 dense array attribute

Operands:

OperandDescription
xany type
yany type
zany type

Results:

ResultDescription
resultany type

synth.xor_inv (::circt::synth::XorInverterOp)

XOR gate with invertible variadic inputs

Syntax:

operation ::= `synth.xor_inv` custom<VariadicInvertibleOperands>($inputs, type($result), $inverted, attr-dict)

The synth.xor_inv operation represents a parity node whose operands may be individually inverted before the XOR is evaluated.

Example:

  %r0 = synth.xor_inv %a, %b : i1
  %r1 = synth.xor_inv not %a, %b, %c : i8
  %r2 = synth.xor_inv not %a : i1

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

AttributeMLIR TypeDescription
inverted::mlir::DenseBoolArrayAttri1 dense array attribute

Operands:

OperandDescription
inputsvariadic of any type

Results:

ResultDescription
resultany type

Attributes

NLDMTableAttr

Resolved 2D NLDM lookup table

Syntax:

#synth.nldm_table<
  ::mlir::DenseF64ArrayAttr,   # index1
  ::mlir::DenseF64ArrayAttr,   # index2
  ::mlir::DenseF64ArrayAttr   # values
>

Parameters:

ParameterC++ typeDescription
index1::mlir::DenseF64ArrayAttr
index2::mlir::DenseF64ArrayAttr
values::mlir::DenseF64ArrayAttr

NLDMTimingArcAttr

NLDM timing arc with delay and transition lookup tables

Syntax:

#synth.nldm_timing_arc<
  ::mlir::StringAttr,   # pin
  ::mlir::StringAttr,   # relatedPin
  ::mlir::StringAttr,   # timingSense
  NLDMTableAttr,   # cellRise
  NLDMTableAttr,   # cellFall
  NLDMTableAttr,   # riseTransition
  NLDMTableAttr   # fallTransition
>

Parameters:

ParameterC++ typeDescription
pin::mlir::StringAttr
relatedPin::mlir::StringAttr
timingSense::mlir::StringAttr
cellRiseNLDMTableAttr
cellFallNLDMTableAttr
riseTransitionNLDMTableAttr
fallTransitionNLDMTableAttr

'synth' Dialect Docs