| Age | Commit message (Collapse) | Author |
|---|
|
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
|
