CIRCT Release Notes: firtool-1.143.0

FIRRTL Dialect

String Properties

This release adds comprehensive support for string concatenation in FIRRTL
properties:

New firrtl.string.concat operation (15f44a9, 32d7d87, ae00359):
Concatenate multiple string property values with full support in parsing,
emission, and lowering to OM. This enables building complex string properties
from multiple components.

Example:
```
%result = firrtl.string.concat %prefix, %name, %suffix
```
The operation lowers cleanly through LowerClasses to OM's om.string.concat
(2f9b5c9) and includes evaluator support (34e5533) for runtime string
concatenation.

Domain System Overhaul

The domain system has undergone a major redesign to align with FIRRTL's
class-based property system:

Domains are now similar to classes (#9871): Domain types now include
symbol references and field name/type tuples, making them structurally similar
to FIRRTL classes. This unification simplifies the type system and enables
better tooling support.
Field value support (#9902): DomainCreateOp now accepts variadic field
values as operands, allowing domains to be instantiated with specific field
values directly. This eliminates the need for separate assignment operations.

Example:
```
%domain = firrtl.domain.create @ClockDomain(%clk, %reset)
```
New DomainSubfieldOp (#9910): Extract field values from domain
instances using firrtl.domain.subfield, similar to how object fields are
accessed.
Improved domain inference (#9958): The InferDomains pass now properly
handles DomainCreateOp and DomainCreateAnonOp, preventing spurious domain
inference on modules containing these operations. Error messages for domain
unification conflicts are now more user-friendly.
Simplified storage (#9896): Domain information is now stored exclusively
in types rather than duplicated in the domainInfo attribute, reducing
redundancy and potential inconsistencies.
Domain stripping improvements (#9931): The domain stripping mode now
properly handles DomainSubfieldOp by replacing uses with UnknownValueOp
before erasure.

Intrinsics

All intrinsics migrated to TableGen (#9847): The remaining 34
manually-registered FIRRTL intrinsics have been moved to the
FIRRTLIntrinsics.td TableGen file. This enables automatic generation of both
registration code and documentation. Previously undocumented intrinsics (LTL
ops, clock_inv, clock_div, mux cells, has_been_reset, fpga_probe) now have
proper descriptions with argument/result tables.

Instance Choice Support

ExpandWhens support (#9956): The ExpandWhens pass now properly handles
InstanceChoiceOp, treating it the same as regular InstanceOp for
when-block expansion.
InstanceInfo tracking (#9811): The InstanceInfo analysis now tracks
modules instantiated within instance choice operations, following the same
pattern as other module attributes like inDesign and inEffectiveDesign.

Cross-Module References (XMR)

Cleaner port references (#9954): When a RefSendOp references a port,
the LowerXMR pass now adds an inner symbol directly to the port instead of
creating an intermediate node. This produces cleaner Verilog output and works
around issues with certain formal tools that treat output ports assigned from
probe nodes as "uncovered".

Layer Improvements

Capture naming (#9957): Changed the namehint for layer-captured
expressions from _layer_probe to _layerCapture to avoid conflicts with
protocols that use "probe" terminology.

Other Improvements

Circuit linking (#9928): The firld tool now allows private extmodules
in circuit linking, providing more flexibility in modular compilation
workflows.

OM Dialect

New Features

String concatenation (2f9b5c9, 34e5533): Added om.string.concat
operation with full evaluator support for runtime string concatenation.
Python bindings (#9868): Added Python bindings for OM unknown value
operations.

HW Dialect

New Optimization Pass

Inter-Module Dead Code Elimination (IMDCE) (#9609): A new aggressive
optimization pass that performs inter-module liveness analysis. The pass
considers a value alive only if it connects to a port of a public module or a
value with a symbol. This can significantly reduce design size by removing
unused logic across module boundaries.

Breaking Changes

Removed hw.instance_choice (#9849): The hw.instance_choice operation
has been removed from the HW dialect. firrtl.instance_choice now lowers
directly to implement the FIRRTL ABI in LowerFIRRTLToHW, avoiding the need to
carry specialized ABI information (macros and headers) into the HW dialect.

Formal Verification and Model Checking

This release significantly expands formal verification capabilities,
particularly for BTOR2-based model checking:

Verification Dialect

New FoldAssume pass (#9968): Optimizes verification code by folding and
simplifying assume operations.
Named symbolic values (#9919): The verif.symbolic_value operation now
accepts an optional name parameter, improving readability in formal backends
while preserving original signal names.
Improved CombineAssertLike (#9983): The pass now supports verif.formal
operations, enabling better optimization of formal verification constructs.

BTOR2 Backend Enhancements

The HWToBTOR2 conversion has received substantial improvements for formal
verification workflows:

Formal operation support (#9926): Added basic support for verif.formal
operations, enabling structured formal verification blocks in BTOR2 output.
Symbolic value emission (#9924): verif.symbolic_value operations now
emit as input in BTOR2, properly representing free variables in model
checking.
Initialization assumptions (#9844): New --assume-init-reset option
allows assuming reset initialization in formal proofs, simplifying
verification of designs with complex reset logic.
Clock conversion (#9837): Added support for seq.to_clock operation,
enabling proper handling of clock type conversions in BTOR2 output.
Improved register handling (#9916, #9838): The backend now only
accepts integer-typed registers and avoids generating invalid BTOR2 when
multiple registers share the same name.

Temporal Logic

LTL past operations (#9845, #9892): Added lowering for ltl.past
operations with clock operands, and integrated these lowerings into the
firtool BTOR2 pipeline.
Clock assumption control (#9863): New --assume-first-clock flag for
LTLToCore enables better control over clock assumptions when ingesting
SystemVerilog assertions.

Synthesis and Optimization

Synth Dialect

The Synth dialect introduces new abstractions for synthesis choices and
optimizations:

New synth.choice operation (#9857, #9872, #9876, #9940):
Represents synthesis alternatives, allowing the compiler to choose between
different implementations. The operation folds when only a single operand
remains and is supported throughout the lowering pipeline (LowerWordToBits,
ConvertSynthToComb).
Functional reduction pass (#9886): New optimization pass for functional
reduction (without SAT solving). This enables simplification of synthesis
choices based on functional equivalence.
Majority graph folding (#9033): Implements optimization for majority
gate graphs, a common pattern in certain synthesis flows.
Operation reuse in LowerVariadic (#9850): The LowerVariadic pass now
implements operation reuse, reducing redundant operations when lowering
variadic operations.

Seq Dialect

Clock-enable register lowering (#9890): Added lowering from
seq.compreg.ce (clock-enable register) to seq.compreg (standard register),
expanding the range of register types that can be processed through the
standard pipeline.
Preset value validation (#6856): The FirRegOp printer/parser now
enforces non-negative preset values, catching errors earlier in the
compilation flow.
Memory address type fix (#9827): Fixed invalid address type generation
for single-element memories in the RegOfVecToMem pass.

SystemVerilog Import (ImportVerilog)

This release dramatically expands SystemVerilog import capabilities,
particularly for advanced language features:

Interface Support

Full interface support (#9792): Added comprehensive support for
interface definitions, instantiation, and interface port handling. This is a
major milestone for importing designs that use SystemVerilog interfaces.
Unconnected ports (#9759): Support for unconnected InOut and Ref
instance ports, allowing partial port connections.

Dynamic and Associative Arrays

Dynamic array creation (#9679): Added support for dynamic array creation
with new size and length operations.
Associative array methods (#9853, #9901, #9907): Implemented
Size(), Num(), exists(), First(), Last(), Next(), and Prev()
methods for associative arrays.
Queue operations (#9791, #9818): Added support for queue
concatenations and queue comparisons (equality/inequality).

Concurrency and Timing

Wait statements (#9824): Added support for wait and wait fork
statements, enabling import of designs with complex synchronization.
Fork-join fixes (#9951): Fixed bugs in fork-join statement handling.

Assertions and Verification

Disable iff support (#9875): Added support for disable iff in clocked
assertions, a commonly-used SVA feature.

String Operations

String indexing (#9867): Added string indexing support with new
sim.string.get operation.

DPI Support

Open-array lowering (#9882): Added DPI open-array lowering support in
MooreToCore, enabling import of DPI functions with open array arguments.

Type Conversions

Real number conversion (#9980): Lowering of convert_real to extf or
truncf of arith dialect, properly handling floating-point conversions.

Semantic Analysis

Slang integration (#9862): Introduced semantic analysis of slang,
improving the quality and correctness of SystemVerilog imports.
System task improvements (#9923): Converted arity-based system task
matching to named-based matching, improving robustness.

Bug Fixes

Fixed segmentation fault in certain import scenarios.
Fixed crash when using $ in queue range selection.
Fixed moore.conversion legalization failure on interface ports.
Dropped trivially inferrable assoc_array type annotations.

FSM and State Machine Synthesis

The CoreToFSM conversion and FSMToSMT backend received several important fixes
and optimizations:

Guard optimization (#9883): The CoreToFSM pass now optimizes guard
region logic that is duplicated in action regions, reducing redundancy in
generated state machines.
Initial state management (#9893): Fixed initial state management in
FSMToSMT, ensuring correct model checking of state machine initialization.
Guard prioritization (#9864): Added prioritization of guards in
FSMToSMT, improving the quality of generated SMT formulas.
Bug fixes (#9899, #9905, #9950, #9952): Fixed infinite loop in
GuardConditionFoldPattern on constants, fixed crash on registers without
resets, and fixed guard-constant folding incorrectly replacing fsm.update
variable operands. Also fixed concat-in-mux losing possible state values.
Empty domain handling (#9888): FSMToSMT now skips conversion when the
FSM domain is empty, avoiding generation of invalid SMT.

RTG Dialect and Test Generation

The RTG (Random Test Generation) dialect and its TableGen backend received
extensive improvements for generating Python test infrastructure:

Python Code Generation

Instruction wrapper generation (#9880): New TableGen backend for
auto-generating Python instruction wrappers, simplifying test development.
Instruction listing (#9922): Added backend to list instructions,
providing better introspection capabilities.
Convenience dispatcher (#9881): Emits convenience dispatcher functions
for easier test authoring.
Identifier sanitization (#9884): Python identifiers are now properly
sanitized to avoid conflicts with Python keywords.

Filtering and Selection

Extension-based filtering: Support for filtering instructions by ISA
extension.
XLEN-based filtering: Support for filtering based on register width
(XLEN).
Custom directives: Added support for custom directives in instruction
definitions.

Language Features

Decimal literals: Added support for decimal literals in RTG
specifications.
Conditional expressions: Support for conditional expressions in
instruction definitions.
Header support: Added support for headers with integration tests.

Improvements

Improved whitespace handling in generated code.
Fully specified namespace paths to avoid ambiguity.
Factored out OperandType handling for better code reuse.
Generate source/dest register methods even when instructions have no
registers.
Small performance fix in LinearScanRegisterAllocation.

Arc Dialect

Simulation time control (#9909): Added time increment operand to
SimStepOp, enabling more precise control over simulation stepping.

Verilog Export

Error propagation fix (#9976): Fixed missing error propagation in
ExportVerilog, ensuring errors are properly reported.
Import fix (#9937): Fixed PruneZeroValuedLogic imports.

Infrastructure and Tooling

SAT Solver Support

New SAT solver interface (#9903): Added a generic SAT solver interface
with z3 wrapper, enabling integration of SAT-based optimizations and
verification.

Testing Tools

circt-test improvements (#9852, #9855, #9918): The circt-test tool
received several enhancements:
- Waveform tracing option for debugging test failures
- Test filtering by name and attribute
- Config file support for managing test suites

Build System

CMake improvements (#9906): Disabled precompiled headers in Slang-facing
code to avoid compilation issues.
CI enhancements (#9854, #9934): Added workflow_dispatch selector
for uploadWheels and added check for slang tests missing valgrind
marker.

LLVM Updates

Bumped LLVM to 055b1efc (#9741), bringing in upstream
improvements and fixes.

Domain-Specific Tools

domaintool

Used StringAttr instead of StringRef in Clock Spec JSON (CSJ) for better
type safety.
Added "synchronousTo" support in CSJ.
Used "define_period" in CSJ handler.

ImportLiberty

Allowed missing "function" attribute, improving robustness when importing
Liberty files with non-standard formatting.

Documentation

Clarified contribution guidelines and AI tool use policies.

New Contributors

@Mohamed-Khairy-SWE made their first contribution in #9759
@sunhailong2001 made their first contribution in #9894
@joaovam made their first contribution in #9850
@yuriyKulinchenko made their first contribution in #9679

Full Changelog: firtool-1.142.0...circt-obfuscator-1.143.0

firtool-1.143.0