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

Operands:

Results:

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:

Results:

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

Ordered 3-input DOT gate with invertible inputs

Syntax:

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

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, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Operands:

Results:

synth.gamble (::circt::synth::GambleOp)

3-input Gamble gate with invertible inputs

Syntax:

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

The synth.gamble operation computes the gamble function of its three inputs, where each operand can be optionally inverted. The gamble function returns 1 when all inputs are 1 or all inputs are 0, and 0 otherwise. For three inputs, it is equivalent to:

(a & b & c) | (~a & ~b & ~c)

Example:

    %r0 = synth.gamble %a, %b, %c : i1
    %r1 = synth.gamble not %a, %b, not %c : i1

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Operands:

Results:

synth.majority (::circt::synth::MajorityOp)

Majority gate with invertible inputs

Syntax:

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

The synth.majority operation computes the majority function of its inputs, where each operand can be optionally inverted.

The majority function returns 1 when more than half of the inputs are 1, and 0 otherwise. For three inputs, it’s equivalent to: (a & b) | (a & c) | (b & c).

Example:

    %r0 = synth.majority %a, %b, %c : i1
    %r1 = synth.majority not %a, %b, not %c : i1

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Operands:

Results:

synth.mux_inv (::circt::synth::MuxInverterOp)

MUX gate with invertible inputs

Syntax:

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

The synth.mux_inv operation represents a 3-input multiplexer node whose operands can be individually inverted before evaluation. The operation chooses between two values based on a condition: given operands (cond, trueValue, falseValue), it calculates cond ? trueValue : falseValue, which is equivalent to:

(cond & trueValue) | (~cond & falseValue)

Example:

  %r0 = synth.mux_inv %a, %b, %c : i8
  %r1 = synth.mux_inv not %a, %b, not %c : i8

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Operands:

Results:

synth.onehot (::circt::synth::OneHotOp)

3-input Onehot gate with invertible inputs

Syntax:

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

The `synth.onehot` operation computes the one-hot function of its three
inputs, where each operand can be optionally inverted. The one-hot function
returns 1 when exactly one of the inputs is 1, and 0 otherwise. For three
inputs, it is equivalent to:

`(a & ~b & ~c) | (~a & b & ~c) | (~a & ~b & c)`

Example:

      %r0 = synth.onehot %a, %b, %c : i1
      %r1 = synth.onehot not %a, %b, not %c : i1

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: BooleanLogicOpInterface, ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Operands:

Results:

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:

Operands:

Results:

Attributes

LinearTimingArcAttr

A single simplified linear timing arc

Syntax:

#synth.linear_timing_arc<
  ::mlir::StringAttr,   # pin
  ::mlir::StringAttr,   # relatedPin
  int64_t,   # intrinsic
  int64_t,   # sensitivity
  PolarityAttr   # polarity
>

Parameters:

MappingCostAttr

Simplified timing and area cost for tech mapping

Syntax:

#synth.mapping_cost<
  ::mlir::FloatAttr,   # area
  ::mlir::ArrayAttr,   # arcs
  ::mlir::DictionaryAttr   # inputCaps
>

Parameters:

NLDMTableAttr

Resolved 2D NLDM lookup table

Syntax:

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

Parameters:

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:

PolarityAttr

Timing arc polarity

Syntax:

#synth.polarity<
  PolarityKind   # value
>

Parameters:

Enums

PolarityKind

Timing arc polarity

Cases:

'synth' Dialect Docs

• 'synth' Dialect
• Synth Longest Path Analysis