Commit Graph

3454 Commits

Author SHA1 Message Date
Andrew Young 1fd4c9ec11 [SV] Use SymbolOpUserInterface to speed up verifiers
This change moves two InferfaceInstanceOp and GetModportOp to use the
symbol user op interface when checking the referenced operation. This
significantly reduces the cost of verifying this.
2024-11-02 00:03:49 -07:00
Andrew Young cb90e658ab [FIRRTL] Make `sym_name` an inherent attr for symbol ops
Making this an inherent attribute means that it will be stored in the
properties of the operation. Some module-like classes already had
declared it as an input, but our older modules kinds did not.
2024-11-01 23:16:34 -07:00
Fabian Schuiki c08df96a5a
[LTL] Canonicalize ltl.and to comb.and for i1 properties (#7759)
Extend `ltl.and`, `ltl.or`, and `ltl.intersect` to infer their return
type as `i1` if all operands are `i1`. Also add a canonicalization
method that replaces these ops with `comb.and` and `comb.or` if they
operate entirely on `i1`.
2024-11-01 09:11:00 -07:00
Jiahan Xie 963d6950a8
Calyx Binary Floating Point AddF Operator (#7089)
* binary floating point add operator for IEEE754
2024-10-31 17:41:21 -04:00
Martin Erhart e1e10ae469
[HW] Add port name accessors to HWInstanceLike (#7757)
HWInstanceLike is currently 'empty' and thus essentially the same as InstanceGraphInstanceOpInterface. On the other hand, HWModuleLike deals with port names and hw::InstanceOp caches them and verifies they match the referenced module's port names. This PR basically makes this behavior part of what it means to be an HWInstanceLike. If one has an instance operation that does not deal with port names, it's still possible to just make it an InstanceGraphInstanceOpInterface directly
2024-10-31 18:36:28 +00:00
Leon Hielscher f91b47e93d [NFC][Sim] Rename "formatting token" to "formatting fragment"
Avoid the ambigous "token" term and use the same naming as the Moore dialect for
a part of a formatting string.

Signed-off-by: Leon Hielscher <hielscher@fzi.de>
2024-10-31 13:34:56 +01:00
Fabian Schuiki 9d92072435
[Verif][NFC] Use auto-generated constructors for all passes (#7754)
Drop the `let constructor` line from the Verif pass definitions. This
causes TableGen to automatically generate the constructors for these
passes, and also handle pass options if we ever decide to add them.

This requires adding a `...Pass` to the end of each pass def to produce
a constructor name of the form `create...Pass()`.
2024-10-30 20:06:11 -07:00
Jiahan Xie b49d2b3adc
Calyx ConstantOp Support (#7086)
* create register based on type

* support calyx constant op and the corresponding emitter

Co-authored-by: Chris Gyurgyik <Gyurgyikcp@gmail.com>

---------

Co-authored-by: Chris Gyurgyik <Gyurgyikcp@gmail.com>
2024-10-30 19:29:01 -04:00
Andrew Young f22f11aa40 [FIRRTL] enable properties for inherent attributes
This enables properties in the FIRRTL dialect. Some op parsers which
called `inferReturnTypes` had to be updated to store inherent attributes
as properties on the OperationState, as the call to `inferReturnTypes`
expects properties to have already been populated.  This is a change
that we should make for all operation parsers and builders, to make
things faster, but is not strictly necessary at this time.
2024-10-30 15:02:43 -07:00
Andrew Young fd56341db4 [FIRRTL] Clean up inferReturnTypes implementation
This is a big change to clean up our implementation of
`inferReturnTypes` in an effort to get ourselves ready to enable
properties in the FIRRTL dialect. We had structured our API so that
`inferReturnType` would call out to a simpler version of itself with
some of the useless arguments removed.  This prevented us from using op
adaptors to abstract over whether or not an inherent attribute was
contained inside the attr-dict or the properties.

This change keeps the old structure of a two level API, but with
different boundaries: The large API takes all arguments, creates an
adapter, pulls out the necessary attributes and then calls in to the
simpler interface. FIRParser uses the simpler API when inferring return
types.  The simpler interface is now specific to each operation and not
common with other operations.

This last change caused a problem for `parsePrimExp`, which relied on a
generic interface to create all expressions. This function is now
templated over exactly how many arguments the specific prim op takes,
parses exactly that many, and splats them out when calling
`inferReturnType`.  As an upside to this, we can also call a more
specific builder for each operation, which should speed up building
operations when we move to properties.
2024-10-30 15:02:43 -07:00
Prithayan Barua 07133326ae
[OM] Add a new API to update fields of a ClassOp (#7748)
Add a new API to update the fields of an existing `FieldsOp` in a class.
This also renames the `addFields` to ensure it is used only to add a new op.
2024-10-29 12:17:32 -07:00
Fabian Schuiki 1244f589bd
[Sim] Include operations and types in dialect doc
The dialect documentation was missing operations and types. Add those
as separate subsections.
2024-10-29 08:07:17 -07:00
Hideto Ueno c301a0f15c
[AIGToComb] [circt-synth] Add a AIG to Comb conversion pass (#7742)
This adds a conversion pass from AIG dialect to Comb dialect. AndInverterOp can be easily converted into comb.and + comb.xor + hw.constant.

This enables us to utilize core dialects tools for synthesis results without any addition. Primarly use case is running LEC on IR before and after synthesis.
2024-10-29 14:15:41 +09:00
Fabian Schuiki 332fd27147
[Verif] Adjust contract ops to match documentation (#7745)
Slightly tweak the `verif.contract`, `verif.require`, and `verif.ensure`
ops to match the usage outlined in the Verif dialect documentation. This
also adjusts the operands and constraints slightly.
2024-10-28 15:24:03 -07:00
Fabian Schuiki ed17d333b1
[Arc] Remove obsolete arc.clock_tree and arc.passthrough ops (#7704)
The new LowerState pass does not produce `arc.clock_tree` and
`arc.passthrough` ops anymore. Remove them from the dialect entirely.
2024-10-28 15:01:34 -07:00
Fabian Schuiki 3181b0317d
[Arc] Improve LowerState to never produce read-after-write conflicts (#7703)
This is a complete rewrite of the `LowerState` pass that makes the
`LegalizeStateUpdate` pass obsolete.

The old implementation of `LowerState` produces `arc.model`s that still
contain read-after-write conflicts. This primarily happens because the
pass simply emits `arc.state_write` operations that write updated values
to simulation memory for each `arc.state`, and any user of `arc.state`
would use an `arc.state_read` operation to retrieve the original value
of the state before any writes occurred. Memories are similar. The Arc
dialect considers `arc.state_write` and `arc.memory_write` operations to
be _deferred_ writes until the `LegalizeStateUpdate` pass runs, at which
point they become _immediate_ since the legalization inserts the
necessary temporaries to resolve the read-after-write conflicts.

The previous implementation would also not handle state-to-output and
state-to-side-effecting-op propagation paths correctly. When a model's
eval function is called, registers are updated to their new value, and
any outputs that combinatorially depend on those new values should also
immediately update. Similarly, operations such as asserts or debug
trackers should observe new values for states immediately after they
have been written. However, since all writes are considered deferred,
there is no way for `LowerState` to produce a mixture of operations that
depend on a register's _old_ state (because they are used to compute a
register's new state), and on a _new_ state because they are
combinatorially derived values.

This new implementation of `LowerState` completely avoids
read-after-write conflicts. It does this by changing the way modules are
lowered in two ways:

**Phases:** The pass tracks in which _phase_ of the simulation lifecycle
a value is needed and allows for operations to have different lowerings
in different phases. An `arc.state` operation for example requires its
inputs, enable, and reset to be computed based on the _old_ value they
had, i.e. the value the end of the previous call to the model's eval
function. The clock however has to be computed based on the _new_ value
it has in the current call to eval. Therefore, the ops defining the
inputs, enable, and reset are lowered in the _old_ phase, while the ops
defining the clock are lowered in the _new_ phase. The `arc.state` op
lowering will then write its _new_ value to simulation storage.

This phase tracking allows registers to be used as the clock for other
registers: since the clocks require _new_ values, registers serving as
clock to others are lowered first, such that the dependent registers can
immediately react to the updated clock. It also allows for module
outputs and side-effecting ops based on `arc.state`s to be scheduled
after the states have been updated, since they depend on the state's
_new_ value.

The pass also covers the situation where an operation depends on a
module input and a state, and feeds into a module output as well as
another state. In this situation that operation has to be lowered twice:
once for the _old_ phase to serve as input to the subsequent state, and
once for the _new_ phase to compute the new module output.

In addition to the _old_ and _new_ phases representing the previous and
current call to eval, the pass also models an _initial_ and _final_
phase. These are used for `seq.initial` and `llhd.final` ops, and in
order to compute the initial values for states. If an `arc.state` op has
an initial value operand it is lowered in the _initial_ phase. Similarly
for the ops in `llhd.final`. The pass places all ops lowered in the
initial and final phases into corresponding `arc.initial` and
`arc.final` ops. At a later point we may want to generate the
`*_initial`, `*_eval`, and `*_final` functions directly.

**No more clock trees:** The new implementation also no longer generates
`arc.clock_tree` and `arc.passthrough` operations. These were a holdover
from the early days of the Arc dialect, where no eval function would be
generated. Instead, the user was required to directly call clock
functions. This was never able to model clocks changing at the exact
same moment, or having clocks derived from registers and other
combinatorial operations. Since Arc has since switched to generating an
eval function that can accurately interleave the effects of different
clocks, grouping ops by clock tree is no longer needed. In fact,
removing the clock tree ops allows for the pass to more efficiently
interleave the operations from different clock domains.

The Rocket core in the circt/arc-tests repository still works with this
new implementation of LowerState. In combination with the MergeIfs pass
the performance stays the same.

I have renamed the implementation and test files to make the git diffs
easier to read. The names will be changed back in a follow-up commit.

Fixes #6390.
2024-10-28 14:57:03 -07:00
Andrew Young 6f5e0a8744 [FIRRTL] Remove validation from type inference code
In FIRRTL, all expression operations have a `validate` hook which can be
used to check operands and attributes before passing them in to
`inferResultTypes`.  FIRParser will verify the same invariants right
before calling `validate`, making it redundant.  Since `validate` is
only called from the parser, we can delete the entire hook.
2024-10-28 14:46:24 -07:00
Schuyler Eldridge e08011253e
[OM] Add ClassOp region verifier
Add a region verifier to OM dialect's Class Op.  This verifies that the
terminator returns the right number of fields with the correct types that
match the declared type of the Class Op.

Fixes #7736.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2024-10-28 16:39:10 -04:00
Schuyler Eldridge b76a3629d2
[OM] Whitespace cleanup in TD
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2024-10-28 16:09:02 -04:00
Bea Healy dae5c1ef36
[circt-bmc] Add initial_values attribute to BMC op (#7729)
Adds support for register initial values in the BMC op and the lowering to the BMC op
2024-10-28 16:03:13 +00:00
Hideto Ueno c6983697fb
[AIG] Add CutOp (#7743)
The `aig.cut` operation represents a cut in the And-Inverter-Graph.
This operation is variadic and can take multiple inputs and outputs,
which corresponds to the input and output edges in AIG conceptually.
2024-10-28 19:40:56 +09:00
Hideto Ueno 5b8b18e9e4
[CombToAIG] Add CombToAIG conversion pass (#7740)
This adds a conversion pass from Comb to AIG. Currently conversion patterns for variadic `comb.or/and` 
and binary xor are supported. There will be a follow up to implement conversion patterns for arithmetic ops.
2024-10-26 20:57:00 +09:00
Hideto Ueno 4f0edf4cfe [AIG] Add LowerWordToBits pass
This commit ads LowerWordToBits pass that perform bit-blasting for
AndInverterOp.
2024-10-26 19:27:58 +09:00
Hideto Ueno f2fc8c7214 [AIG] Add LowerVariadic pass
This commit adds AIG LowerVariadic pass to lower variadic AndInverter
op to have at most two operands. This makes IR closer to traditinal
AIG representation combined with LowerWordToBits pass
2024-10-26 19:27:58 +09:00
Hideto Ueno c2c00c69e0
[AIG] Add AndInverterOp (#7738)
This commit adds `aig.and_inv` op that represents an And-Inverter in AIG.
DenseBoolArray `inverted` field specifies if each operand is inverted.
This commit also adds a basic canonicalizer for it.
2024-10-26 17:45:29 +09:00
Hideto Ueno e937bb7f56 [AIG] Add AIG dialect
This adds a template for AIG dialect, a dialect used for
representing and transforming And-Inverter Graphs.
2024-10-26 16:18:17 +09:00
Andrew Young 54aa4e3d05 Use properties for attributes for many dialects
This change enables the use of operation properties for more dialects in
CIRCT. The option to *not* use properties is going to be removed in a
future release of MLIR, but as well we expect this change to bring a
performance improvement.

For all these dialects, the only change required was to properly infer
return types.  Some operations were hardcoded to search through the
attributes, and the attribute was moved to the property storage. By
using the generated adaptor classes, we can abstract over where the
interesting attribute is stored.

For future work, some code may be refactored for further performance
wins now that we are using properties. In particular usages `setAttr`
and `getAttr` may be made faster by using a less generic op
transformation interface.
2024-10-25 23:42:32 -07:00
Andrew Young 542d7e5f37 [FIRRTL] Make FModuleLike op interface friendly with properties 2024-10-25 16:26:52 -07:00
Andrew Young 70df0eced7 [FIRRTL] Make FNameableOpInterface friendly with properties 2024-10-25 16:26:52 -07:00
Schuyler Eldridge ad28fd2291
[FIRRTL] Add "effective" design to Instance Info
Expand the API of the InstanceInfo analysis to include queries for if
something is in the "effective" design.  This is equivalent to querying if
something is not under a layer.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2024-10-24 18:43:42 -04:00
Schuyler Eldridge 4d03e88ab6
[FIRRTL] Add "inDesign" to InstanceInfo Analysis
Extend the existing InstanceInfo analysis to track information about if a
module is in the "design".  The design is defined is everything that is or
is under the design-under-test, but is not in a layer.  I.e., this
excludes things that are in layers.

This is added because it is not possible to compute this using the
existing information about something being under the DUT or under a layer.
A module could have mixed instantiation under the DUT and mixed
instantiation under a layer, yet not be in the design.

Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
2024-10-24 00:17:07 -04:00
Robert Young ec8ffaf4fe
Advanced LayerSink (#7548) 2024-10-22 10:18:07 -04:00
Hideto Ueno c0e31955ce
[HW][Seq] Allow typed attr to be an element of aggregate_constant and make seq.const_clock typed attr (#7718)
This fixes https://github.com/llvm/circt/issues/7716. Aggregate constant verifier rejects unknown attributes hence hw.aggregate_constant cannot be used for attributes defined by other dialects (in this case seq.const_clock) was rejected even when hw.aggregate_create allows users to create clock type arrays. This PR loosen the restriction by allowing TypedAttribute. 

This commits also adds TypedAttrInterface to seq.const_clock and support its lowering.
2024-10-22 15:53:10 +09:00
Lenny Truong 3a9ccf9583
[OM] Rework ClassOp to use return style for class fields (#7537)
This changes the OM dialect Class/ExternClass to use a return style
field name/type specifier syntax and, for non-extern class, a terminator
op in the style of hw.output.
2024-10-21 17:15:36 -04:00
John Demme 313ac7a40e
[ESI] Promote and generalize 'channel assignments' (#7715)
Previously, cosim store its ESI channel to cosim channel name in the
`implDetails`. DMA engines to make channel communication work in real
hardware need this information as well.
2024-10-18 02:18:14 -07:00
Bea Healy 117b5ecaa4
[NFC] Fix typo in Arc PrintCostModel summary 2024-10-17 14:57:04 +01:00
Lenny Truong ea952baa3e
[Verif] Add LowerFormalToHW pass (#7707)
* Rewrites `verif.formal` to `hw.module`
* Lifts `verif.symbolic_value` to be an input to the module
2024-10-15 17:04:44 -07:00
Fabian Schuiki 2085d0d91e
[Arc] Add dominance-aware pass to sink ops and merge scf.if ops (#7702)
Add the `MergeIfs` pass to the Arc dialect. This pass covers a handful
of control flow optimizations that are valuable to pick up after
`hw.module`s have been linearized and lowered into `arc.model` ops:

- It moves operations closer to their earliest user, if possible sinking
  them into blocks if all uses are nested in the same block.
- It merges adjacent `scf.if` operations with the same condition.
- It moves operations in between two `scf.if` operations ahead of the
  first if op to allow them to be merged.

The `MergeIfs` pass can operate on SSACFG regions. It assigns an integer
order to each operation and considers that order to determine up to
which point operations can be moved without moving beyond their first
use and without crossing interfering side-effecting ops. The pass is
aware of side-effects, and in particular uses the non-aliasing between
`arc.state` and `arc.memory` to track read/write side-effects at a
per-state level, which allows for fairly aggressive optimization. Other
side-effecting ops act as a hard barrier and will not be moved or moved
over.

This pass supersedes the very effective `GroupResetsAndEnables` pass
we have been using until now. The latter relies on the
`LegalizeStateUpdate` pass to run at a later point however, which will
be removed in a future PR, thus making this new pass necessary.

This is a preparatory step for a later PR that overhauls the LowerState
pass. That rewrite will make the `arc.clock_tree` and `arc.passthrough`
ops obsolete, which is why they are not present in the tests.
2024-10-15 11:38:29 -07:00
Fabian Schuiki 629abefea2
[Arc] Make arc.model have an SSACFG region (#7701)
Remove the `RegionKindInterface` from `arc.model` such that its body
region becomes an SSACFG region. The current implementation of the
LowerState pass already creates models which honor SSA dominance, and
future improvements to the Arc dialect will benefit from models
enforcing dominance.
2024-10-14 09:57:07 -07:00
Fabian Schuiki 24522338f2
[Arc] Add arc.final op (#7700)
Add the `arc.final` op to complement the existing `arc.initial`. The
body of `arc.final` is executed after the last time step, when the
simulation is shut down. This corresponds to SystemVerilog's `final`
procedure, and can also be used to report statistics about which `cover`
statements were hit, or to check if an `eventually` property has been
satisfied.

The `arc.final` op is extracted into a `*_final` function. The contract
with the user is that the `*_final` function must be called exactly once
after the last call to `*_eval`. The simulation lifetime now looks like
this:

```
design_initial()
design_eval()
design_eval()
design_eval()
...
design_eval()
design_final()
```

The `arc.sim.instantiate` op inserts a corresponding call to `*_final`
when lowering to LLVM.
2024-10-14 09:49:24 -07:00
Fabian Schuiki 822ac6bba4
[Arc][NFC] Tweak arc op docs and add missing test
Slightly tweak the summary and description fields of a few Arc ops and
add missing tests for `arc.state_write` and `arc.state_read` to the
basic Arc dialect test.
2024-10-13 18:24:37 -07:00
Prithayan Barua d92ed2781a
[ExtractInstances] Add the extract instances metadata to OM Classes (#7667)
This commit adds the ExtractInstances metadata to the OM classes. The emitted
OM dialect can then be parsed to generate the respective metadata files. This
change enables to move all the metadata to the OM dialect, instead of existing
as verbatim ops.
Also move some common ClassOp utilities to the builder and update the
CreateSifiveMetadata pass accordingly.
2024-10-11 08:58:32 -07:00
Fabian Schuiki dc387c57fc
[MooreToCore] Add support for format strings and display task (#7694)
Lower the format string ops and the `moore.builtin.display` task to the
corresponding ops in the Sim dialect. This is not perfect yet, since Sim
does not support some of the formatting options. They will be easy to
add in the future though.
2024-10-10 19:56:19 -07:00
mingzheTerapines acd335d215
[MooreToCore] Support assert, assume, cover ops (#7681)
* [MooreToCore] Support assert, assume, cover ops

Add conversion patterns from moore.{assert,assume,cover} to the corresponding verif.* op in MooreToConv. Consider rejecting deferred assertions for now. https://chipsalliance.github.io/sv-tests-results/?v=circt_verilog+16.2+assert_test
Fix issue https://github.com/llvm/circt/issues/7630


* Do not differentiate between the different scheduling regions in SV
2024-10-11 09:40:59 +08:00
Fabian Schuiki 71b8665123
[Sim][NFC] Include InferTypeOpInterface in SimOps.td (#7693)
Include the `InferTypeOpInterface.td` file in `SimOps.td`, which causes
TableGen to automatically generate builders without result type for
operations where the result type is either fixed or derived from the
operands. This makes one of the builders obsolete.
2024-10-10 17:26:33 -07:00
Fabian Schuiki 9d96d50c45
[Verif] Simplify the FormalOp (#7691)
Simplify the definition of the `verif.formal` operation which describes
a single formal unit test. This op used to have a "k" parameter which is
now gone in favor of more generically using the attributes dictionary to
capture execution parameters. As we build out the testing flows, we can
reintroduce necessary attributes to this operation.

Rename `verif.symbolic_input` to `verif.symbolic_value`.

Remove `verif.concrete_input` in favor of explicitly describing the
concrete input using one of the registers in the Seq dialect. This also
makes the associated clock explicit, which was missing from this op.
2024-10-10 11:21:44 -07:00
Fabian Schuiki ef3303e793
[Verif] Minor verif.formal tweaks 2024-10-09 10:05:32 -07:00
Martin Erhart f75bbd7986
[LLHD][HW] Implement SROA interfaces (#7672) 2024-10-07 19:46:31 +01:00
Martin Erhart f287ba2f7b
[OM] Add integer shift left op (#7658) 2024-10-04 09:44:18 +01:00
Martin Erhart e12dafcb0f
[FIRRTL] Add integer shift left property op (#7657) 2024-10-03 20:23:04 +01:00