[Seq] FIFO lowering: emits unguarded `assert property`, breaking synthesis

[teqdruid]

This issue written by Claude Opus 4.7 then edited by me.

---

seq.fifo lowering emits unguarded assert property, breaking Quartus (and other) synthesis

Summary

The seq.fifo → HW lowering in LowerSeqFIFO.cpp unconditionally inserts two concurrent assertions ("FIFO empty when read enabled" / "FIFO full when write enabled"). After VerifToSV, these are emitted as bare SystemVerilog assert property statements with no `ifndef SYNTHESIS guard and no other vendor-pragma wrap.

This breaks Intel Quartus, which rejects concurrent assertions in synthesis:

Error (13224): Verilog HDL or VHDL error at ListVoidResultCountAdapter.sv(43):
  Found a non-synthesizable construct "temporal assertion".
  If this construct is not required for design elaboration it must be wrapped in
  `no_translate synthesis pragmas
Error (13224): ... Line: 44 ...

The same pattern is also problematic for several other synthesis tools that don't fully support SVA, even when they accept the rest of the file.

Reproduction

Any design that uses seq.fifo (directly or transitively — e.g. PyCDE's ListWindowToSerial, ESI runtime adapters, etc.) produces output containing:

FIFO_empty_when_read_enabled:
  assert property (@(posedge clk) ~(load_count & fifo_empty));
FIFO_full_when_write_enabled:
  assert property (@(posedge clk) ~(_GEN & fifo_full));

These statements are emitted at module scope, outside any guard.

Root cause

LowerSeqFIFO creates verif::ClockedAssertOp ops directly into the module body at LowerSeqFIFO.cpp#L189-L194:

verif::ClockedAssertOp::create(
    rewriter, loc, notEmptyAndRden, verif::ClockEdge::Pos, clkI1,
    /*enable=*/Value(),
    rewriter.getStringAttr("FIFO empty when read enabled"));

VerifClockedAssertLikeConversion in VerifToSV.cpp#L195-L205 then turns each into an sv::AssertPropertyOp, again with no synthesis guard. ExportVerilog prints them verbatim.

By contrast, the FIRRTL → HW lowering carefully wraps verification statements with addToIfDefBlock("SYNTHESIS", ...) (see e.g. LowerToHW.cpp#L5235 and FirRegLowering.cpp#L413), producing `ifndef SYNTHESIS ... `endif blocks that all major synthesis tools accept by defining the SYNTHESIS macro.

The existing knobs do not help:

• LoweringOptions::disallowClockedAssertions (LoweringOptions.h#L178) only converts the form (concurrent → procedural always block); the result is still a synthesizable-construct error in Quartus.
• -sv-extract-test-code was removed (see Firtool.cpp#L814, comment "-sv-extract-test-code has been removed").
• There is no flag that simply drops or guards verification ops produced by non-FIRRTL frontends.

So any frontend that uses seq.fifo (PyCDE, hand-written MLIR, Calyx-derived flows, etc.) cannot produce Quartus-clean SystemVerilog without post-processing the output file.

Proposed solutions

Local fixes (any one is sufficient)

1. Wrap FIFO assertions in `ifndef SYNTHESIS in LowerSeqFIFO

Smallest, most contained change. In LowerSeqFIFO.cpp#L181-L201, wrap the two verif::ClockedAssertOp::create(...) calls in an sv::IfDefOp("SYNTHESIS", /*then*/ {}, /*else*/ ...). This mirrors the established convention used by FIRRTL lowering and immediately fixes Quartus for everyone using seq.fifo.

Pros: tiny, follows precedent, no API change.
Cons: doesn't help other passes that emit verif.*assert* ops (e.g. anything user-written or future lowerings).

2. Add an ifdef-guard option to LowerVerifToSV

Generalize the fix: give VerifToSVPass (VerifToSV.cpp#L201-L226) a pass option (e.g. guard-with-ifndef=SYNTHESIS, default off) that wraps every produced sv.assert.property / sv.assume.property / sv.cover.property (and the procedural variants) in an sv::IfDefOp with the configured macro name. Pipelines targeting FPGA synthesis can enable it from the driver.

Pros: covers all current and future producers of verif.* ops; opt-in so nothing changes by default.
Cons: slightly larger surface; needs a small amount of design (per-op vs. per-module wrap).

3. Provide a small "strip / guard verification" utility pass

A standalone pass --guard-verification-ops=SYNTHESIS (or --strip-verification-ops for users who want them gone entirely) operating on hw.module bodies, wrapping/erasing all verif::Assert*Op, verif::Assume*Op, verif::CoverOp, and (post-VerifToSV) sv::AssertPropertyOp etc. This is composable and backend-agnostic; any pipeline can add it before ExportVerilog.

Pros: most flexible; gives users an explicit knob; useful even for non-FIFO assertions.
Cons: another pass to maintain; needs to know about both verif and sv flavors.

Orthogonal: vendor-specific synthesis pragma support

Independently of the above, CIRCT could grow first-class support for emitting Quartus / Synopsys / Cadence-style line pragmas (e.g. // synthesis translate_off ... // synthesis translate_on) around assertions, in addition to (or instead of) `ifndef SYNTHESIS. This is what Quartus's error message literally suggests, and it doesn't require the user to define the SYNTHESIS macro in their tool flow.

This is orthogonal to the three fixes above: those decide whether/where a guard appears around verification ops; this decides what kind of guard is emitted. A natural place for this would be a new LoweringOption (e.g. assertionGuardStyle=ifdef|translateOffOn|none) consumed by ExportVerilog when emitting any sv.assert*/sv.assume*/sv.cover* op, regardless of how it got there. Because ExportVerilog is the consumer, LoweringOptions is appropriate for this knob.

References

• seq.fifo assertion creation: LowerSeqFIFO.cpp#L181-L201
• verif.clocked_assert → sv.assert.property (no guard): VerifToSV.cpp#L168-L201
• disallowClockedAssertions option (insufficient for this issue): LoweringOptions.h#L174-L178
• Removal of -sv-extract-test-code: Firtool.cpp#L814
• Existing addToIfDefBlock("SYNTHESIS", ...) precedent in FIRRTL lowering: LowerToHW.cpp#L5235, LowerToHW.cpp#L5283, FirRegLowering.cpp#L413
• LoweringOptions consumers (only ExportVerilog and late SV passes): ExportVerilog.cpp#L36, PrettifyVerilog.cpp#L553, HWLegalizeModules.cpp#L459

[teqdruid]

As usual, I'm writing my opinion as a comment so as to avoid biasing the conversation. (And without Claude.)

I'd like to see the VerifToSV optionally emit guards (option 2).

For guards, I have a slight preference for // synthesis comments since they seem pretty standard. But we don't currently have support for "pragma" blocks. Additionally, ifdefs are already used by the FIRRTL flow so it's the standard in CIRCT.

As Claude implies, should we have a custom op to indicate "this region is not synthesizable" and should be guarded appropriately which ExportVerilog respects?

[teqdruid]

@fabianschuiki @seldridge WDYT?

This is blocking me so if I don't hear back I'll go ahead and write a pass which adds guards since I suspect that'll be the least controversial.

[seldridge]

I would unconditionally lower to guarding with ifndef SYNTHESIS. I wouldn't do this in a pass or make it opt in. If that becomes necessary later, we can deal with it then.