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.
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.
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>
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.
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
```
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>
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.
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
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.
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.
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
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.
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.
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.
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).
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.
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.
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.
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>
#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>
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>
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.
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
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>