| Age | Commit message (Collapse) | Author |
|---|
|
Co-authored-by: sinofp <sinofp@tuta.io>
|
|
|
|
|
|
Move new transforms, recently added, into existing or new sets of
transforms (defined in firrtl.stage.Forms).
One transform is a mandatory low FIRRTL optimization:
- firrtl.transforms.LegalizeAndReductionsTransform
Previously, this was included as a prerequisite of all Verilog
emitters (minimum, normal, and SystemVerilog).
Two transforms associated with converting and removing the new
verification statements are moved into a new set of transforms,
AssertsRemoved:
- firrtl.transforms.formal.ConvertAsserts
- firrtl.transforms.formal.RemoveVerificationStatements
Previously, these transforms were directly added as prerequisites to
the minimum Verilog and normal Verilog emitter, but not the
SystemVerilog emitter.
The designation of inputForm=LowForm for legacy, custom transforms is
updated to include assertion removal transforms as part of their
optionalPrerequisites. This has the effect of continuing to cause
inputForm=LowForm transforms to run as late as possible (right before
the low FIRRTL, minimum Verilog, Verilog, or SystemVeriog emitter).
Tests are updated to reflect the new order in both CustomTransformSpec
and LoweringCompilersSpec.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
|
|
Refactor the test used in the CustomTransformSpec to assert that
inputForm=LowForm legacy transforms run right before the emitter (see
note below!). The new test looks only for a list of (customTransform,
emitter) in a sliding, size-2 window of the flattened transform order.
Previously, this was looking for a match before and after the custom
transform. The old implementation necessitate busywork updates of the
test when new transforms are added that changed the transform running
before the custom transform.
Note: this test, as written is intentionally wrong. When verification
statements were added, the test was changed to not do what it's
supposed to do. Namely, the test is supposed to ensure that an
inputForm=LowForm transform runs immediately before its emitter.
However, the test is actually checking that the custom transform runs
before transforms that convert and remove verification statements. I'm
intentionally leaving the test broken, but doing the refactor in order
to make this easier to manually backport to the 1.3.x branch.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
|
|
|
|
* Add assume, assert, cover statements
* Assert submodule assumptions
* Add warning when removing verification statements
* Remove System Verilog behaviour emitter warning
* Add option to disable AssertSubmoduleAssumptions
* Document verification statements in the spec
The syntax for the new statements is
assert(clk, cond, en, msg)
assume(clk, cond, en, msg)
cover(clk, cond, en, msg)
With assert as a representative example, the semantics is as follows:
`clk` is the clock, `cond` is the expression being asserted, `en` is the
enable signal (if `en` is low then the assert is not checked) and `msg`
is a string message intended to be reported as an error message by the
model checker if the assertion fails.
In the Verilog emitter, the new statements are handled by a new
`formals` map, which groups the statements by clock domain. All model
checking statements are then emitted within the context of an `ifdef
FORMAL` block, which allows model checking tools (like Symbiyosys) to
utilize the statements while keeping them out of synthesis flows.
Co-authored-by: Albert Magyar <albert.magyar@gmail.com>
|
|
Workaround for https://github.com/verilator/verilator #2300
present in Verilator versions v4.026 - v4.032. This transform turns AND
reductions for expressions > 64-bits into an equality check with all
ones. It is included as a prerequisite for all Verilog emitters.
|
|
This adds missing invalidations to four transforms:
- ExpandConnects
- RemoveAccesses
- SplitExpressions
- VerilogMemDelays
This necessarily updates test cases which expect exact transform
orders to reflect the new order.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
|
|
* Pull out common test utilities into a separate package
* Project a fat jar for test utilities
Co-authored-by: Albert Magyar <albert.magyar@gmail.com>
|
|
Co-authored-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
Co-authored-by: Albert Magyar <albert.magyar@gmail.com>
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
|
|
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
|
|
|
|
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
|
|
Instead, just forward the exception
|
|
|
|
* Rename implict module "clk" input to "clock".
This doesn't rename all the "self-contained" test instances.
nor the memory "clk" enables,
nor the implict module "clk"s in the regress .fir files.
* Consistency: rename implict module "clk" input to "clock" in "self-contained" test instances.
This doesn't rename the memory "clk" enables, nor the implict module "clk"s in the regress .fir files.
|
|
* Transform Ids now handled by Class[_ <: Transform] instead of magic numbers
* Transforms define inputForm and outputForm
* Custom transforms can be inserted at runtime into compiler or the Driver
* Current "built-in" custom transforms handled via above mechanism
* Verilog-specific passes moved to the Verilog emitter
|
