circt/test/firtool
Fabian Schuiki a7bd275fb9
[FIRRTL] Fix folding of when conditions into LTL properties (#7760)
Make ExpandWhen's folding of the when condition into LTL properties work
for more inputs. This used to be very brittle and the condition would
be mapped to a new implication around the entire property:

    when (a):
      assert(@(posedge clock) b |-> c)

used to become

    assert(a |-> @(posedge clock) b |-> c)

This commit improves on this by always pushing implications behind
clocks, and by merging implications like `a |-> b |-> c` into a single
`(a & b) |-> c`. As a result, ExpandWhens now produces the following
output, which is more in line with what users expect:

    assert(@(posedge clock) a & b |-> c)

Also add a FIR-to-Verilog test to nail this behavior down and ensure we
don't regress on user expectations.
2024-11-01 12:42:45 -07:00
..
spec/refs [FIRRTL] Bump minimum to 2.0.0, remove partial conect (#5075) 2024-06-11 11:07:18 -05:00
annotation-error.fir [FIRRTL] Remove test usage of '<=' connect, NFC 2024-10-25 16:59:12 -04:00
annotation-openaggs-error.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
annotation-openaggs.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
assign-output-dirs.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
async-reset-anno.fir [FIRRTL][InferResets] Generalize FART to support sync reset (#7476) 2024-08-08 21:39:25 -07:00
async-reset.fir [FIRRTL][InferResets] Generalize FART to support sync reset (#7476) 2024-08-08 21:39:25 -07:00
blackbox-directories.fir [FIRRTL] Compute LCA of BlackBoxDir output files 2024-08-23 17:07:01 -04:00
blackbox-path.v [FIRRTL] Add black box reader pass (#918) 2021-05-21 20:01:58 +02:00
blackbox.mlir [FIRRTL] Make tests with filepaths platform agnostic 2022-10-19 17:41:50 -07:00
btor2-assertproperty.fir [FIRRTL][Verif][LTL] Replace `ltl.disable` with an enable folded into `verif.assert` (#7150) 2024-06-20 11:24:37 -07:00
btor2.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
chirrtl.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
chisel-interface.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
chisel_assert.fir [FIRRTL][NFC] Drop use of intmodule's in tests. (#7008) 2024-05-08 16:32:32 -05:00
classes-dedupe.fir [OM] Rework ClassOp to use return style for class fields (#7537) 2024-10-21 17:15:36 -04:00
clock-gate.fir [FIRRTL][NFC] Replace intmodules with intrinsic expressions in test. (#7041) 2024-05-15 11:05:35 -05:00
clocking.fir [FIRRTL][NFC] Replace intmodules with intrinsic expressions in test. (#7041) 2024-05-15 11:05:35 -05:00
combinational-loop-errors.fir [firtool] Move SpecializeLayers before LowerLayers 2024-06-18 08:45:22 -07:00
combinational-loops.fir [firtool] verify that comb loop checking resolves last connects 2024-06-18 08:45:22 -07:00
commandline.mlir Don't read lowering options from hidden global options (#4038) 2022-10-04 15:41:03 -05:00
connect-errors.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
connect.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
convention.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
dedup-modules-with-output-dirs.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
dpi.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
export-ref.fir [FIRRTL][LowerXMR] Use FIRRTL 4.0 ref ABI. (#6677) 2024-02-08 16:46:43 -06:00
extract-test-code.fir [SV] Add Intermediary Assert Op for better enable polarity flip (#7302) 2024-07-12 10:34:04 -07:00
firtool-errors.mlir [firrtl] Remove CircuitOp::getMainModule 2023-11-28 15:48:40 -05:00
firtool.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
firtool.fir.anno.1.json [FIRRTL] clang-format annotation JSON, NFC 2022-07-06 22:19:43 -04:00
firtool.fir.anno.json [FIRRTL] clang-format annotation JSON, NFC 2022-07-06 22:19:43 -04:00
firtool.fir.omir.anno.json Object Model 2.0, Part 1: Read in OM 2.0 (#1915) 2021-10-01 20:55:54 -04:00
firtool.mlir [NFC, FIRRTL] Rename StrictConnect to MatchingConnect. (#7116) 2024-06-04 09:19:00 -05:00
has_been_reset.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
import-ref.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
include-dirs-annotations.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
include-dirs.fir [firrtl] Remove CircuitOp::getMainModule 2023-11-28 15:48:40 -05:00
initialization-checking-errors.fir [firtool] Move SpecializeLayers before LowerLayers 2024-06-18 08:45:22 -07:00
instchoice.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
layers-rwprobe.fir fixup! [FIRRTL] Use new layer ABI 2024-08-29 17:13:42 -04:00
layers.fir fixup! [FIRRTL] Use new layer ABI 2024-08-29 17:13:42 -04:00
locators-diagnostics.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
lower-layers-directories.fir fixup! [FIRRTL] Use new layer ABI 2024-08-29 17:13:42 -04:00
lower-layers.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
lower-memories.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
memory.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
memoryLowering.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
memoryMetadata.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
memoryMetadata.fir.anno.json [FIRRTL][CreateSifiveMetadata] Use symbols for memory metadata (#5482) 2023-06-27 14:02:50 -07:00
memoryMetadataRenameFail.fir [FIRRTL] Remove test usage of '<=' connect, NFC 2024-10-25 16:59:12 -04:00
memoryMetadataRenameFail.fir.anno.json [FIRRTL] Create memory metadata (#1923) 2021-10-08 10:08:33 -07:00
module-hier.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
name-preservation.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
optimizations.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
phase-ordering.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
plusargs.fir [FIRRTL][NFC] Replace intmodules with intrinsic expressions in test. (#7041) 2024-05-15 11:05:35 -05:00
prefixMemory.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
print-before.fir [FIRRTL] Bump minimum to 2.0.0, remove partial conect (#5075) 2024-06-11 11:07:18 -05:00
print.fir [SV] Add MacroRefOp to represet macro statement (#7607) 2024-09-25 17:29:57 +09:00
properties.fir [FIRRTL] Add end to end properties example 2023-08-23 15:54:56 -07:00
refs-in-aggs.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
register-optimization.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
register-randomization.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
specialize-layers-cli.fir [firtool] Change layer specialization CLI interface (#7520) 2024-08-15 10:55:22 -07:00
specialize-layers-default.fir [firtool] Add option to specify default layer specialization mode 2024-07-30 13:43:29 -07:00
specialize-layers.fir fixup! [FIRRTL] Use new layer ABI 2024-08-29 17:13:42 -04:00
split-verilog.mlir [ExportVerilog] Drop external module emission (#7558) 2024-08-28 10:56:55 -04:00
stop.fir [SV] Add MacroRefOp to represet macro statement (#7607) 2024-09-25 17:29:57 +09:00
style.fir [FIRRTL] Bump minimum to 2.0.0, remove partial conect (#5075) 2024-06-11 11:07:18 -05:00
sv-attr.fir [FIRRTL] Migrate tests to connect, invalidate, NFC 2024-10-25 01:03:45 -04:00
unr-only.fir [FIRRTL] Don't prefix an empty label for unclocked assume. (#7016) 2024-05-09 12:18:46 -05:00
verbatim-parameter.fir [FIRRTL][HW] Add verbatim literal support (#5774) 2023-08-08 10:15:09 -04:00
verbose-pass-executions.fir [FIRRTL] Bump minimum to 2.0.0, remove partial conect (#5075) 2024-06-11 11:07:18 -05:00
verif-under-when.fir [FIRRTL] Fix folding of when conditions into LTL properties (#7760) 2024-11-01 12:42:45 -07:00
verif.fir [FIRRTL][NFC] Replace intmodules with intrinsic expressions in test. (#7041) 2024-05-15 11:05:35 -05:00