'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:
| Attribute | MLIR Type | Description |
|---|---|---|
inverted | ::mlir::DenseBoolArrayAttr | i1 dense array attribute |
Operands:
| Operand | Description |
|---|---|
inputs | variadic of any type |
Results:
| Result | Description |
|---|---|
result | any 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:
| Operand | Description |
|---|---|
inputs | variadic of any type |
Results:
| Result | Description |
|---|---|
result | any 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:
| Attribute | MLIR Type | Description |
|---|---|---|
inverted | ::mlir::DenseBoolArrayAttr | i1 dense array attribute |
Operands:
| Operand | Description |
|---|---|
x | any type |
y | any type |
z | any type |
Results:
| Result | Description |
|---|---|
result | any 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:
| Attribute | MLIR Type | Description |
|---|---|---|
inverted | ::mlir::DenseBoolArrayAttr | i1 dense array attribute |
Operands:
| Operand | Description |
|---|---|
inputs | variadic of any type |
Results:
| Result | Description |
|---|---|
result | any type |
Attributes
NLDMTableAttr
Resolved 2D NLDM lookup table
Syntax:
#synth.nldm_table<
::mlir::DenseF64ArrayAttr, # index1
::mlir::DenseF64ArrayAttr, # index2
::mlir::DenseF64ArrayAttr # values
>
Parameters:
| Parameter | C++ type | Description |
|---|---|---|
| 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:
| Parameter | C++ type | Description |
|---|---|---|
| pin | ::mlir::StringAttr | |
| relatedPin | ::mlir::StringAttr | |
| timingSense | ::mlir::StringAttr | |
| cellRise | NLDMTableAttr | |
| cellFall | NLDMTableAttr | |
| riseTransition | NLDMTableAttr | |
| fallTransition | NLDMTableAttr |