Commit Graph

10108 Commits

Author SHA1 Message Date
Leon Hielscher 7775fb9ee9
[VerifToSMT] Move some LEC lowering code to a superclass, NFC (#8748)
Move two chunks of code out of the `LogicEquivalenceCheckingOpConversion` class to a new super class so they can be reused in the conversion of the `RefinementCheckingOp`. The conversion is added in a follow-up PR.
No functional change.
2025-07-21 14:32:21 +02:00
Martin Erhart c7213930da [PyRTG] Fix test
We have folders for these ops now
2025-07-21 11:57:00 +01:00
Martin Erhart a8600777dc
[RTG] Support immediate slice/concat after validate (#8744) 2025-07-20 09:15:27 +01:00
Hideto Ueno dc524e9ea0
[AIG][LongestPathAnalysis] Fix a bug in deduplicatePathsImpl (#8746)
This commit fixes a bug in deduplicatePathsImpl within the AIG LongestPathAnalysis.

Close https://github.com/llvm/circt/issues/8745
2025-07-19 20:51:17 -07:00
Martin Erhart 24bd19e3cc
[RTG] Fix ValidateOp elaboration (#8743) 2025-07-19 11:10:36 +01:00
Martin Erhart 418459fd0d
[RTG] Add concat_immediate and slice_immediate folders (#8738) 2025-07-19 09:23:48 +01:00
Martin Erhart fb0b3dae45
[RTG] Add immediate concat and slice operations (#8735) 2025-07-19 09:22:02 +01:00
Andrew Young 9c54fa5619
[FIRRTL] Do not allow uninferred widths or resets in enums (#8740)
This adds verifiers to the FIRRTL parser and to the FEnumType to prevent
having uninferred widths and resets inside enumerations.  It seems like
the trickiness to implement these features would be hard to take
advantage of in practice, making it not worth it.  This also fixes the
error messages produced by the type verifier that had extraneous quotes
around the field name, and rearranges some tests to be co-located in the
test file.
2025-07-18 15:32:34 -07:00
Schuyler Eldridge 47cf87cdcd
[firtool] Fix argument passing to LowerAnnotations
Fix a bug introduced in [[1]] where two parameters passed to the
LowerAnnotations pass were swapped.  Swap these back and add a test of
this behavior.

[1]: 2b98e4233

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2025-07-18 16:39:05 -04:00
Andrew Young 0671e9d440
[FIRRTL] LowerToHW: handle TagExtractOp (#8726)
This updates LowerToHW to handle the TagExtractOp.  This reflects on the
lowered input value's type to determine how the enum was lowered.  If it
was lowered to a struct, we extract the tag field. If it was lowered to
a integer, we can return the integer directly.
2025-07-18 12:05:20 -07:00
Andrew Young 20fd9f4ae8 [FIRRTL] FIRParser: parse tagExtract operations 2025-07-18 12:04:46 -07:00
Andrew Young c88358475e [FIRRTL] FIRParser: support minimum spec versions for prim ops 2025-07-18 12:04:46 -07:00
Andrew Young 6ece8a3005
[FIRRTL] Enums: Add user-defined constructor encodings (#8724)
This adds the ability to specify the constants used to encode
enumeration variants in the tag. For example,
``` firrtl
wire a : {| A = 10, B = 5 |}
```

The values can be unspecified, in which case it defaults to one higher
than the previous value, or zero if it is the first value. For example,
these two enumerations are the same:
``` firrtl
{| A = 0, B = 1 |} == {| A, B |}
```

In FIRRTL, Two enumeration types are considered equal if they have the
same variants with the same values and data, without regard to variant
order.  Internally in FIRRTL dialect IR, enumerations types must have
the variants sorted from low to high. For example the following two
enumeration types are equivalent:
``` firrtl
{| B = 1, A = 0 |} == {| A, B |}
```

The mlir syntax has been updated to ellide the the tag values and data
types if they are implicit.  For example, the first type would be
roundtripped to the second type:
``` mlir
!firrtl.enum<a = 0 : uint<0>> => !firrtl.enum<a>
```

Enumerations are no longer lowered to SystemVerilog enumerations, but to
regular integer types.  This is for a variety of reasons, but mainly
because enumerations in SV are nominal and it was not a good fit for our
structural enumerations.

In LowerToHW, the `firrtl.istag` operation lowers to a comparison to a
constant value created with  a localparam, which can show up in the
output depending on how the module is optimized. The  FIRRTL code below,

``` firrtl
FIRRTL version 4.0.0
circuit Enums:
  public module Enums:
    input in : {|A = 8 : UInt<8>, B = 16 |}
    output out : UInt<8>
    match in:
      A(data):
        connect out, data
      B:
        connect out, UInt<8>(16)
```
produces:
``` verilog
module Enums(
  input  struct packed {logic [4:0] tag; union packed {logic [7:0] A;/*B: Zero Width;*/ } body; } in,
  output [7:0]                                                                                    out
);

  localparam [4:0] A = 8;
  assign out = in.tag == A ? in.body.A : 8'h10;
endmodule
```
2025-07-18 11:26:31 -07:00
Leon Hielscher 71dec45d65
[Verif] Add RefinementCheckingOp (#8713)
This PR adds the RefinementCheckingOp to the verif dialect. The motivation behind this operation is to be able to automatically check whether a 'target' circuit is a refinement of a 'source' circuit. This should be a small step towards performing translation validation comparable to Alive2. The operation is structurally identical to the LogicEquivalenceCheckingOp, so I factored out most of the ODS into a common CircuitRelationCheckOp. If there is no non-determinism present in the circuits, the operation is also functionally identical to LogicEquivalenceCheckingOp.

Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>
2025-07-18 19:36:58 +02:00
Martin Erhart f741e83f0f
[RTG] Add a pass to print a list of tests (#8734)
This pass prints the names of the tests in the IR. Since tests can be duplicated and elaborated differently during compilation, it prints both the newly uniqued name and the original name as specified by the user in the frontend.
2025-07-18 18:08:19 +01:00
Andrew Young cfe267e907
[FIRRTL] LowerSigs: Add enum support (#8731)
This adds support for enumerations to LowerSigs so that the pass no
longer fails when it encounters an enum, and just passes them through
unchanged.

Fixes #7106
2025-07-18 08:58:52 -07:00
Martin Erhart 277d3ec03c
[CombToSMT] Force conversion from bool to bv<1> after icmp (#8737) 2025-07-18 14:02:13 +01:00
Hideto Ueno ba24efca88
[circt-synth] Add an option to disable WordsToBits, remove verification code from design (#8733)
This modifies circt-synth to make it more practical.
* Remove verification code from synthesis parts. ExtarctTestCode is currently used, but eventually it must be replaced with something cleaner. 
* Add an option to disable wordsToBits.
2025-07-18 01:51:51 -07:00
Samuel Coward 7a165d8c45
[circt-lec] Adding support for the datapath dialect (#8721)
* Add support for datapath dialect to circt-lec

* Correct integration test
2025-07-18 09:21:58 +01:00
Andrew Young 62a6582687 [ExportVerilog] localparam should always print bitwidths
We are currently printing 1-bit localparams without a size, which causes
verilator to complain that it does not have a known bitwidth when used
in some expressions.  This changes ExportVerilog to always print the
bitwidth of localparams, which is something we already do for
parameters.
2025-07-17 17:30:05 -07:00
John Demme 3e42dbce12
[ESI] Fix wrap op canonicalizers (#8730)
Fixes the canonicalizers for wrap operations in the ESI dialect by replacing problematic attribute-based folding with proper operation creation and improving pattern matching logic.

- Updates `WrapValidReadyOp` and `WrapFIFOOp` fold methods to create `NullSourceOp` operations instead of using attributes
- Improves the `WrapFIFOOp` canonicalize method with better error handling and more robust user checking
- Delegates constant materialization to the HW dialect for better consistency
2025-07-17 15:50:53 -07:00
Andrew Young 0b3976c12e [FIRRTL] TagExtract: make type inference parser friendly
This also changes TagExtract to use the simpler type inference
signatures used by other operations, which will be used when parsing
this operation from fir files.
2025-07-17 15:12:54 -07:00
Andrew Young e5c0e6f20f [FIRRTL] verify no duplicate fields in bundles 2025-07-17 15:10:37 -07:00
Andrew Young f9ef4cd72a [FIRRTL] FIRParser: check the bundle field names are unique 2025-07-17 15:10:37 -07:00
Andrew Young dc0940687a
[FIRRTL] FIRParser: support caching constants in match statements (#8723)
This fixes a long standing bug when parsing match statements which
contain numeric constants.

The FIRParser has a contant cache so that we can reuse any constant
operation created as we parse, by inserting them into the top-level body
of the module.  To find the top level block, we were searching upwards
from the current insertion point.

In general, when creating any operation, we are required to know how
many regions the operation has; it is impossible to add more regions
after creating the operation. Due to this, when parsing the arms of a
match statement, the expressions are inserted into a region which is not
attached to any operation.  This means we can not search upwards from
the insertion point to find the top level block. When operations do not
have this problem as they always have space 2 regions.

This change passes in the top level block when creating the
FIRModuleContext.  If it turns out that the region we are inserting into
is not underneath the module, then we can insert the constant at the end
of the module's block.

This change also makes the cache itself a private member, and removes a
bit of code which was unnecessarily directly accessing the cache.
2025-07-17 11:45:25 -07:00
Andrew Young ad3d990f9b
[FIRRTL] SFCCompat: properly lower invalidated enums (#8722)
Enum types were not handled by this pass, and so it would hit an
unreachable assert.  This handles enum types using the aggregate
codepath, which creates a 0 value and bitcasts it to the aggregate type.
2025-07-17 11:45:15 -07:00
Robert Young 194a788319
[FIRRTL] Remove circuit from macro used by inline layers (#8714)
We want to use the same macro for an inline layer across all compilation units
(circuits) in a design.  Remove the circuit name from the macro name.
2025-07-17 14:24:10 -04:00
Martin Erhart c67c8b205d
[Python] Speed up type_to_pytype and attribute_to_var (#8718) 2025-07-17 19:19:05 +01:00
Martin Erhart 058f2b4e1b
[PyRTG] Support Python config parameters (#8719) 2025-07-17 17:57:39 +01:00
Martin Erhart 46d768d98e
[circt-verilog] Enable SROA again (#8720)
Enable SROA again since the stackoverflow bug upstream is resolved now.
2025-07-17 17:43:41 +01:00
Hideto Ueno c59018ac98
[AIG] Use llvm::stable_sort to sort paths (#8717)
since llvm::sort is non-determnisic it's not suitable for using it for user-facing API. Also fix inconsistent bit position emission.
2025-07-17 01:51:47 -07:00
Martin Erhart 6ad1b83d7a [RTG][RTGTest] Use new OpTy::create instead of builder.create 2025-07-17 09:11:54 +01:00
Martin Erhart 47d8fe3d05 Fix some compiler warnings 2025-07-17 09:00:33 +01:00
Martin Erhart 1e70370de2
[RTG] Enable conditional value forwarding for ValidateOp (#8712) 2025-07-17 08:59:04 +01:00
Martin Erhart 916ff355ee
[RTG] Add custom tuple type to support empty tuples (#8711)
The builtin tuple type does not allow empty tuples, but they can avoid special casing in the frontend and can also be used as indicators (something like a none type could otherwise be used for but which we don't have in RTG).
2025-07-17 08:13:28 +01:00
Martin Erhart 5ee54acb05
Bump LLVM to d9190f8141661bd6120dea61d28ae8940fd775d0 (#8715)
Preparing this week's bump to get
* https://github.com/llvm/llvm-project/pull/149087
* https://github.com/llvm/llvm-project/pull/139694

Changes:
* Remove ambiguous builder in SV
2025-07-16 17:54:58 -04:00
Michael 16f899d52d
[MooreToCore] Lower empty string constant to expected bit width (#8688)
Fix type bit width mismatch when lowering empty string constants.
2025-07-16 13:19:19 -07:00
Hideto Ueno 1f671d6452
[AIG] Add slice indexing support to LongestPathCollection in AIG python on bindings (#8709)
This commit implements slice indexing functionality for the LongestPathCollection
class, allowing users to access multiple timing paths using Python's standard
slice notation. The implementation handles all slice types including negative
indices, step values, and empty slices through Python's built-in slice.indices()
method.
2025-07-16 12:58:52 -07:00
Martin Erhart 0ee3284927
[RTG] Redefine RandomNumberInRangeOp upper bound to be inclusive (#8710)
When we want to be able to get all possible numbers that fit in a 64 bit register, we would need a 65 bit number as the upper bound. However, an iindex typed attribute uses an APInt with 64 bits and would thus make this complicated.
2025-07-16 19:41:55 +01:00
Mike Urbach 2b1b9fe240
Bump LLVM to ace1c838ca91c83c7a271d9378b86ea56051e83f. (#8705)
This is mostly a clean bump, but I did clean up a couple warnings that
the fresh compile revealed.

The one minor breaking change was a change to argument order in
ConstantIntOp::build, which was added in:

https://github.com/llvm/llvm-project/commit/a45fda6

This just swaps the order.
2025-07-14 21:04:09 -06:00
Prithayan Barua 2beb8e783f
[OM] Deprecate the OM Map and Tuple (#8606)
Remove the support for OM Map and Tuple. 
All the dependence on them have been removed.
---------

Co-authored-by: Mike Urbach <mikeurbach@gmail.com>
2025-07-14 19:57:59 -07:00
Schuyler Eldridge e5603e1437
[ExportVerilog] Use ODS constructor for pre-passes
Convert ExportVerilog pre-passes to use ODS constructors instead of
unnecessarily hand-rolling custom constructors.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2025-07-14 21:54:30 -04:00
Schuyler Eldridge ec79b1b617
[hw] Convert HW Passes to use ODS constructors (#8703)
Change all HW passes to use ODS consturctors as opposed to hand-rolling
them.  The hand-rolled constructors aren't necessary and add a bunch of
boilerplate.

Note: a number of these passes do not have users and hence may break out
of tree users.  The out of tree users are likely @teqdruid and @mortbopet.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2025-07-14 18:59:07 -04:00
Leon Hielscher 8fa6b23567
[Verif][LEC] Make LECOp result optional to avoid unsafe conversion (#8701)
#8497 introduced a lowering pattern for the LogicEquivalenceCheckingOp which changes behavior depending on whether the result of the operation is used. This is generally not safe and can cause lowerings to erroneously consider the result to be used/unused. The pattern must only depend on the operation itself, not on its def-use context.

By making the result of the operation optional, we should be able to retain the current behavior. In the pattern op.use_empty() is simply replaced by op.getNumResults() == 0. However, we now have to decide at the point of creating the LogicEquivalenceCheckingOp whether the result should be made accessible to the IR.


Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>
2025-07-14 20:30:30 +02:00
Will Dietz e9cde40aa8 comb-to-aig test: fix typo in filecheck directive, fix capture 2025-07-14 13:03:55 -05:00
Will Dietz 34929f4564 lower-to-hw test: fix directive and tweak to match output 2025-07-14 13:03:55 -05:00
Schuyler Eldridge e012bda4aa
[FIRRTL] Remove MemToRegOfVec shadowed parameters
Remove shadowed pass parameters for MemToRegOfVec.  These are now provided
by the base class and don't need to exist.  This also fixes an observed
nightly valgrind failure where these were used uninitialized.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2025-07-12 14:26:11 -04:00
Hideto Ueno bb8e97b88a
[AIG] Add canonicalization to simplify inversion (#8697)
Add a canonicalization pattern for AndInverterOp that flattens nested
inversions by detecting when an and_inv operation takes as input another
and_inv operation with a single inverted operand.

This eliminates redundant double inversions and simplifies the AIG
representation by reducing the depth of inversion chains.
2025-07-11 18:40:43 -07:00
Fabian Schuiki 7df789c3ba
[Comb] Fix excessive const shifts causing crashes and invalid IR (#8696)
The folders and canonicalizers for `comb.shl`, `comb.shru`, and
`comb.shrs` perform unchecked `getZExtValue()` calls which can crash
if the shift amount does not fit into 64 bits. The shift amount is also
not clamped to the width of the result, which causes the shift to be
replaced with ops that have a different type.

Found with [VlogHammer], which turns out to be a very handy tool!

Fixes #8694.
Fixes #8695.

[VlogHammer]: https://github.com/YosysHQ/VlogHammer
2025-07-11 17:30:48 -07:00
Schuyler Eldridge 4a23fec916
[FIRRTL] Cleanup Passes.h after constructors rm'd
Cleanup FIRRTL's Passes.h header now that all the non-ODS pass
constructors have been removed.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2025-07-11 19:27:11 -04:00