Convert the remaining option-less FIRRTL passes to use ODS constructors
instead of rolling our own. There's no actual benefit in using the custom
ones other than making things more complex (and adding confusing
boilerplate that developers think they need to copy).
h/t @eunoku for the suggestion to do this.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
To verify correctness of transformations involving datapath operations,
include a lowering from datapath to SMT. Will later be integrated into
circt-lec to enable verification of these operators. Each operator
satisfied a contract, rather than providing a precise semantics for
every operator. This is because the datapath operators return values in
redundant number representations, meaning there are many valid
implementations.
For example:
```mlir
%0:2 = datapath.compress %a, %b, %c : i8 [3 -> 2]
```
Will be verified by introducing free variables for each return value
`(%0#0, %0#1)` then asserting that the sum of the associated free
variables is equal to the sum of the inputs:
`assert(%0#0 + %0#1 == %a + %b + %c)`.
Whilst this is encoded as an assert it really represents an assumption
that must be satisfied by a valid implementation of datapath.compress.
Set the `bin` flag on the `comb.mux` that we insert for enable
flip-flops in LLHD's Deseq pass. This allows circt-verilog to preserve
the difference between `if (en) q <= d` and `q <= en ? d : q` enables.
In the future we'll probably want to have more explicit ops to describe
these differences. But adding the `bin` flag causes the pipeline to
preserve the property we're interested in for now.
* [FIRRTL] Add "knownlayers" specifications to ExtModules
In a circuit, we only know about the layers which have been declared. If we
have an extmodule, it may have been defined under a different set of layers
than what is in the current circuit. In particular, if there is a layer which
we know about, but the extmodule does not, then the extmodule will not have a
bind file for us to include.
This commit adds a "knownlayer" declaration to extmodules, which is an explicit
specification of the layers which an extmodule was defined with. For each
bound-in layer that an extmodule knows about, we can assume that there will be
a bindfile to include.
Changes:
FExtModule: Add a knownLayers property. Update the verifier so that, if a layer
is mentioned by an enablelayer specification or port type, then that layer must
be known by the exmodule. Bonus: implement verifySymbolUses for extmodules.
FIRParser: add parsing for knownlayer declarations on extmodules.
LowerLayersPass: Use the known-layers of extmodules while building the
bindfiles for modules in the current circuit. If a module in the current
circuit instantiates an extmodule, then that module's bindfiles will include
the bindfiles for the known-layers of the extmodule.
SpecializeLayers: Clean up known-layers when a layer is specialized away.
FirEmitter: Emit knownlayer declarations.
* Apply suggestions from code review
Co-authored-by: Schuyler Eldridge <schuyler.eldridge@gmail.com>
* Address comments
* Fix typo
* Clean up layer verification messages
* Use nextFIRVersion for guarding knownlayer
---------
Co-authored-by: Schuyler Eldridge <schuyler.eldridge@gmail.com>
Fixes a problem during VerifToSMT lowering when creating the smt::BVConstantOps for initial integer values of registers in the BMC operation. The current implementation calls getSExtValue() on the APInt provided by the initial value attribute. This causes a crash in either of the following situations:
- The initial value type is lager than 64 bits
- The initial value type is smaller than 64 bits and the MSB of the value is set. By sign-extending to 64 bits, the resulting integer value exceeds the width of the created BitVector.
This is fixed by passing the APInt directly to the builder of smt::BVConstantOp and adding a check beforehand ensuring that the types of the initial attribute and the initialized register match.
Co-authored-by: Martin Erhart <maerhart@outlook.com>
Adds a new transaction‐level snoop operation (`snoop.xact`) to the ESI dialect, lowers it to hardware, and wires it through the Python front end.
- Introduce `SnoopTransactionOp` in ESIChannels.td with `verify` and `inferReturnTypes` in ESIOps.cpp
- Extend the HW lowering pass to remove `snoop.xact` via `RemoveSnoopTransactionOp`
- Update MLIR tests and the PyCDE API (`snoop_xact`) to exercise the new operation
Change from using custom pass constructors to using the ODS-generated pass
constructors. This both saves on line count and also generates nicer,
more consistent constructors for passes which have options.
This migrates some passes that do not use options. More passes need to be
migrated.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Advanced layer sink is now the only "layer sinking" pass that can run, it is no
longer possible to run the original layer sink pass. This commit also disables
layer sinking when optimizations are disabled.
Remove the LayerSink pass and rename advanced-layer-sink to layer-sink.
Change the default value for `-lint-xmrs-in-design` to `false`. This
provides at least one version where this linting is available, but
opt-in (which is backwards compatible) as opposed to opt-out (which is
not). Additionally, for flows that are using `-enable-layers` and
`-sv-extract-test-code`, defaulting this to `true` creates issues where
you _need_ to turn it off because linting happens after layers are
inlined, but before they are extracted.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Implement the following canonicalizations which essentially assume the
value of a mux condition to be a constant in the op that supplies the
true or false value of the mux:
```
mux(cond, op(cond), x) -> mux(cond, op(1), x)
mux(cond, x, op(cond)) -> mux(cond, x, op(0))
```
This only works if the true or false value only have a single use.
The canonicalizers in the Comb dialect generate `hw.constant`
operations. If the input does not contain any HW ops that would trigger
the HW dialect to load, the canonicalizers would crash when trying to
create a constant.
Marking HW as a dependent dialect causes it to be loaded.
This commit introduces a standardized synthesis pipeline and restructures the codebase:
* Creates a new SynthesisPipeline class to define the default synthesis pipeline. This pipeline serves both circt-synth and is exposed through the C API for Python bindings.
* Added a dedicated Synthesis directory under `lib/` to house synthesis-related code. This architectural change is aimed to promote synthesis capabilities to a first-class component within CIRCT rather than limiting it to the circt-synth tool.
The `transformReduce` utility was moved out of FIRRTL and into a CIRCT
support library. Update a user of this in the `Lint` pass.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
* [CIRCT] Move parallelTransformReduce to common util header
* [FIRRTL] Lower registers under ifdefs
In seq-to-sv, we transform seq FirRegOps to sv RegOps. This is done using a
helper called FirRegLowering. This PR changes FirRegLowering to correctly lower
registers under ifdef blocks.
The initialization of registers is placed in an initial block at the footer of
the enclosing HWModuleOp. In order to initialize registers buried under ifdefs,
we have to refer to these registers by a local XMR, because the buried
registers will not dominate the initial block. We build these in a prepass over
the MLIR module, returning a "PathTable" sending buried FirRegOps to their
HierPathOps.
The main FirRegLowering procedure operates in parallel on each HWModuleOp. Each
invocation is now handed a const reference to the path table, which allows us
to produce an XMRRefOp as needed while emitting the register initialization
code at the footer of the HWModule.
The initialization code for a register has to be guarded under the same ifdef
conditions as the register itself. To do this, while lowering registers, we
record the conditions under which the register is defined, and recreate them to
guard the initialization code.
When we lower a register, we attempt to transform any input mux tree into an SV
if-else tree of connects. This PR modifies the if-else generation to co-locate
the if-else with the register. So if a register is guarded under an ifdef, then
the if-else structure driving it will also be under the same ifdef.
Use the names of surrounding generate blocks as a prefix for variable
and instance names. This makes the names match up more closely with how
existing EDA tools would label variables and instances embededded in
generate blocks.
Consider the following Verilog input:
```systemverilog
module Top;
int x;
begin : foo
int y;
for (genvar i = 2; i < 6; ++i) begin : bar
int z;
end
end
endmodule
```
The ImportVerilog conversion pass will now produce the following
variables:
```mlir
%x = moore.variable : <i32> // before: %x
%foo.y = moore.variable : <i32> // before: %y
%foo.bar_2.z = moore.variable : <i32> // before: %z
%foo.bar_3.z = moore.variable : <i32> // before: %z_0
%foo.bar_4.z = moore.variable : <i32> // before: %z_1
%foo.bar_5.z = moore.variable : <i32> // before: %z_2
```
This closely matches names like `foo.bar[2].z` or `foo_bar_2_z` that
would be generated by common EDA tools. Ideally we would be able to use
a name like `foo.bar[2].z` directly, but ExportVerilog currently does
not support escaped identifiers, causing the name to be sanitized to
something like `foo_bar5B25D_z`.
By incorporating for-generate loop indices and block names into the
variable name, logical equivalence checking should become easier and the
signal names in Arcilator waveforms will match user expectations more
closely.
Fixes#8679.
Fix an issue with the `moveDut=true` behavior of the `InjectDUTHierarchy`
pass that would occur if the design-under-test (DUT) was the main module
in a circuit. If this happens, this would create a new wrapper module
above the DUT, mark it private, and keep the main module of the circuit
pointing at the wrapper. This would then cause the new DUT to be deleted
as it was a private module.
This is not FIRRTL ABI compatible as it will create a new public module
and cause things like additional ref files to be created.
CC: @azidar
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Remove an unused variable in the `CreateSiFiveMetadata` pass. This fixes
a compilation warning.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Support `sequence` and `property` declarations. Slang already handles
the references and variable ports. Make visiting of `AssertionInstance`
legal. Those are part of `Expressions` of the `Simple` case. Adapt this
visitor to handle the varied return types.
Fix a few issues in the conversion of indexed ranges selects like
`[a+:b]` and `[a-:b]`. These would not properly convert from the bit
indices to the bit offsets of the underlying storage. The `+:` and `-:`
directions and ascending/descending range specifications make for
strange combinations that need to be handled.
Also pull the code that is almost identical between lvalue and rvalue
lowering into a new common `ExprVisitor` base class. This class has an
`isLvalue` boolean member that can be consulted by the conversion to
either build lvalue ops such as `moore.extract_ref`, or rvalue ops such
as `moore.extract`. This allows us to have a single implementation for
bit and range selects, as well as member accesses.
Add tests for all flavors of range selects, for both ascending and
descending ranges, and rvalues and lvalues.
Fixes#8671.
Refactor FIRRTL's Lint pass to use the ODS-generated constructor as
opposed to hand-rolling one. This avoids weirdness where the command-line
options have different defaults from what they are specified as in ODS and
avoids the need for a "Config" struct inside the linter's namespace (as
the ODS-generated one can be used).
h/t @uenoku for the suggestion.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Add an option to the `firtool` command line that allows for
disabling/enabling the linting of XMRs that exist in the "design". While
there is now a general policy of exposing each lint option in firtool, I
am particularly nervous about this option as it has a high likelihood of
causing problems (false positives).
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Add an option to FIRRTL's linter that allows for disabling/enabling
linting of XMRs that exist in the "design".
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Extend the FIRRTL linter to check that there are no XMRs that will be
located in the "design". This intentionally only checks for problems in
the "design" and NOT the "effective design". This errs on the side of
having more false negatives without introducing the possibility of false
positives for separate compilation flows.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Expose an option to turn off/on the linting of trivially false assertions.
This option defaults to "on" because this was the behavior originally.
Also, I am intending to follow this going forward where lint checks are
always on and have to be turned off.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Make the linting of static assertions an option to the linter. While this
appears unnecessary now, I am intending to add additional lint checks to
the linter and I want to be able to turn each of them off if they become
problematic.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Convert the FIRRTL linting pass to be a `CircuitOp` pass with internally
handled parallelism. This is done in preparation to add XMR linting which
requires an `InstanceInfo` analysis which needs to be on the `CircuitOp`.
There are two ways of doing this:
1. Make the pass operate on the `CircuitOp` as this patch does.
2. Use a cached parent analysis which requires a dedicated pass to
compute the `InstanceInfo` analysis and then careful pass pipeline
structuring.
(2): is used in one place in IREE and nowhere else. Additionally, (1) was
suggested by multiple people in "Hallway Usabilty Testing"-type
discussions. (Many people thought (2) was odd.)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Schuyler Eldridge