[Seq] Fix FIFO lowering to correct depth and pointer increments (#8003)

teqdruid · web-flow · commit 44ea9a8f447a · 2024-12-18T09:38:45.000-08:00
Fixes two bugs:
- Incorrect depth constant led to FIFO never reaching capacity.
- Increment pointers only worked for depth which were powers of two.

Updates integration test to test for these two conditions.
diff --git a/include/circt/Dialect/Seq/SeqPasses.td b/include/circt/Dialect/Seq/SeqPasses.td
@@ -18,7 +18,11 @@ include "mlir/Pass/PassBase.td"
 def LowerSeqFIFO : Pass<"lower-seq-fifo", "hw::HWModuleOp"> {
   let summary = "Lower seq.fifo ops";
   let constructor = "circt::seq::createLowerSeqFIFOPass()";
-  let dependentDialects = ["circt::hw::HWDialect", "circt::comb::CombDialect"];
+  let dependentDialects = [
+    "circt::hw::HWDialect",
+    "circt::comb::CombDialect",
+    "circt::verif::VerifDialect"
+  ];
 }
 
 def LowerSeqHLMem: Pass<"lower-seq-hlmem", "hw::HWModuleOp"> {
diff --git a/integration_test/Dialect/Seq/fifo/fifo.mlir b/integration_test/Dialect/Seq/fifo/fifo.mlir
@@ -1,13 +1,13 @@
 // REQUIRES: iverilog,cocotb
 
-// RUN: circt-opt %s --lower-seq-fifo --lower-seq-hlmem --lower-seq-to-sv --sv-trace-iverilog --export-verilog -o %t.mlir > %t.sv
+// RUN: circt-opt %s --lower-seq-fifo --lower-seq-hlmem --lower-seq-to-sv --lower-verif-to-sv --sv-trace-iverilog --export-verilog -o %t.mlir > %t.sv
 // RUN: circt-cocotb-driver.py --objdir=%T --topLevel=fifo \
 // RUN:     --pythonModule=fifo --pythonFolder="%S,%S/.." %t.sv 2>&1
 
 // CHECK: ** TEST
 // CHECK: ** TESTS=[[N:.*]] PASS=[[N]] FAIL=0 SKIP=0
 
 hw.module @fifo(in %clk : !seq.clock, in %rst : i1, in %inp : i32, in %rdEn : i1, in %wrEn : i1, out out: i32, out empty: i1, out full: i1, out almost_empty : i1, out almost_full : i1) {
-  %out, %full, %empty, %almostFull, %almostEmpty = seq.fifo depth 4 almost_full 2 almost_empty 1 in %inp rdEn %rdEn wrEn %wrEn clk %clk rst %rst : i32
+  %out, %full, %empty, %almostFull, %almostEmpty = seq.fifo depth 6 almost_full 2 almost_empty 1 in %inp rdEn %rdEn wrEn %wrEn clk %clk rst %rst : i32
   hw.output %out, %empty, %full, %almostEmpty, %almostFull : i32, i1, i1, i1, i1
 }
diff --git a/integration_test/Dialect/Seq/fifo/fifo.py b/integration_test/Dialect/Seq/fifo/fifo.py
@@ -20,6 +20,7 @@ async def initDut(dut):
 
 async def write(dut, value):
   dut.inp.value = value
+  assert dut.full.value == 0
   dut.wrEn.value = 1
   await clock(dut)
   dut.wrEn.value = 0
@@ -52,14 +53,21 @@ async def readWrite(dut, value):
   return data
 
 
-FIFO_DEPTH = 4
+FIFO_DEPTH = 6
 FIFO_ALMOST_FULL = 2
 FIFO_ALMOST_EMPTY = 1
 
 
+@cocotb.test()
 async def test_separate_read_write(dut):
-  # Run a test where we incrementally write and read values from 1 to FIFO_DEPTH values
-  for i in range(1, FIFO_DEPTH):
+  """Run a test where we incrementally write and read values from 1 to
+  FIFO_DEPTH values."""
+
+  dut.inp.value = 0
+  dut.rdEn.value = 0
+  dut.wrEn.value = 0
+  await initDut(dut)
+  for i in range(1, FIFO_DEPTH + 1):
     for j in range(i):
       await write(dut, 42 + j)
 
@@ -78,29 +86,25 @@ async def test_separate_read_write(dut):
     assert dut.empty.value == 1
 
 
+@cocotb.test()
 async def test_concurrent_read_write(dut):
-  # Fill up the FIFO halfway and concurrently read and write. Should be able
-  # to do this continuously.
+  """Fill up the FIFO halfway and concurrently read and write. Should be able
+  to do this continuously."""
+
+  dut.inp.value = 0
+  dut.rdEn.value = 0
+  dut.wrEn.value = 0
+  await initDut(dut)
+
   counter = 0
   for i in range(FIFO_DEPTH // 2):
     await write(dut, counter)
     counter += 1
 
   for i in range(FIFO_DEPTH * 2):
     expected_value = counter - FIFO_DEPTH // 2
-    print("expected_value: ", expected_value)
+    print(f"expected_value: {expected_value}")
     assert await readWrite(dut, counter) == expected_value
     assert dut.full.value == 0
     assert dut.empty.value == 0
     counter += 1
-
-
-@cocotb.test()
-async def test1(dut):
-  dut.inp.value = 0
-  dut.rdEn.value = 0
-  dut.wrEn.value = 0
-  await initDut(dut)
-
-  await test_separate_read_write(dut)
-  await test_concurrent_read_write(dut)
diff --git a/lib/Dialect/Seq/Transforms/CMakeLists.txt b/lib/Dialect/Seq/Transforms/CMakeLists.txt
@@ -15,6 +15,7 @@ add_circt_dialect_library(CIRCTSeqTransforms
   CIRCTSeq
   CIRCTSupport
   CIRCTSV
+  CIRCTVerif
   MLIRIR
   MLIRPass
   MLIRTransformUtils
diff --git a/lib/Dialect/Seq/Transforms/LowerSeqFIFO.cpp b/lib/Dialect/Seq/Transforms/LowerSeqFIFO.cpp
@@ -10,6 +10,7 @@
 #include "circt/Dialect/SV/SVOps.h"
 #include "circt/Dialect/Seq/SeqOps.h"
 #include "circt/Dialect/Seq/SeqPasses.h"
+#include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Support/BackedgeBuilder.h"
 #include "mlir/Pass/Pass.h"
 #include "mlir/Transforms/DialectConversion.h"
@@ -34,10 +35,10 @@ struct FIFOLowering : public OpConversionPattern<seq::FIFOOp> {
   LogicalResult
   matchAndRewrite(seq::FIFOOp mem, OpAdaptor adaptor,
                   ConversionPatternRewriter &rewriter) const final {
+    Location loc = mem.getLoc();
     Type eltType = adaptor.getInput().getType();
     Value clk = adaptor.getClk();
     Value rst = adaptor.getRst();
-    Location loc = mem.getLoc();
     BackedgeBuilder bb(rewriter, loc);
     size_t depth = mem.getDepth();
     Type countType = rewriter.getIntegerType(llvm::Log2_64_Ceil(depth + 1));
@@ -47,11 +48,12 @@ struct FIFOLowering : public OpConversionPattern<seq::FIFOOp> {
     Backedge nextCount = bb.get(countType);
 
     // ====== Some constants ======
-    Value countTcFull =
-        rewriter.create<hw::ConstantOp>(loc, countType, depth - 1);
+    Value countTcFull = rewriter.create<hw::ConstantOp>(loc, countType, depth);
     Value countTc1 = rewriter.create<hw::ConstantOp>(loc, countType, 1);
     Value countTc0 = rewriter.create<hw::ConstantOp>(loc, countType, 0);
+    Value ptrTc0 = rewriter.create<hw::ConstantOp>(loc, ptrType, 0);
     Value ptrTc1 = rewriter.create<hw::ConstantOp>(loc, ptrType, 1);
+    Value ptrTcFull = rewriter.create<hw::ConstantOp>(loc, ptrType, depth);
 
     // ====== Hardware units ======
     Value count = rewriter.create<seq::CompRegOp>(
@@ -123,8 +125,13 @@ struct FIFOLowering : public OpConversionPattern<seq::FIFOOp> {
     Value wrAndNotFull = rewriter.create<comb::AndOp>(
         loc, adaptor.getWrEn(), comb::createOrFoldNot(loc, fifoFull, rewriter));
     auto addWrAddrPtrTc1 = rewriter.create<comb::AddOp>(loc, wrAddr, ptrTc1);
-    wrAddrNext.setValue(rewriter.create<comb::MuxOp>(loc, wrAndNotFull,
-                                                     addWrAddrPtrTc1, wrAddr));
+
+    auto wrAddrNextNoRollover = rewriter.create<comb::MuxOp>(
+        loc, wrAndNotFull, addWrAddrPtrTc1, wrAddr);
+    auto isMaxAddrWr = rewriter.create<comb::ICmpOp>(
+        loc, comb::ICmpPredicate::eq, wrAddrNextNoRollover, ptrTcFull);
+    wrAddrNext.setValue(rewriter.create<comb::MuxOp>(loc, isMaxAddrWr, ptrTc0,
+                                                     wrAddrNextNoRollover));
     static_cast<Value>(wrAddrNext)
         .getDefiningOp()
         ->setAttr("sv.namehint", rewriter.getStringAttr("fifo_wr_addr_next"));
@@ -133,8 +140,12 @@ struct FIFOLowering : public OpConversionPattern<seq::FIFOOp> {
     Value rdAndNotEmpty =
         rewriter.create<comb::AndOp>(loc, adaptor.getRdEn(), notFifoEmpty);
     auto addRdAddrPtrTc1 = rewriter.create<comb::AddOp>(loc, rdAddr, ptrTc1);
-    rdAddrNext.setValue(rewriter.create<comb::MuxOp>(loc, rdAndNotEmpty,
-                                                     addRdAddrPtrTc1, rdAddr));
+    auto rdAddrNextNoRollover = rewriter.create<comb::MuxOp>(
+        loc, rdAndNotEmpty, addRdAddrPtrTc1, rdAddr);
+    auto isMaxAddrRd = rewriter.create<comb::ICmpOp>(
+        loc, comb::ICmpPredicate::eq, rdAddrNextNoRollover, ptrTcFull);
+    rdAddrNext.setValue(rewriter.create<comb::MuxOp>(loc, isMaxAddrRd, ptrTc0,
+                                                     rdAddrNextNoRollover));
     static_cast<Value>(rdAddrNext)
         .getDefiningOp()
         ->setAttr("sv.namehint", rewriter.getStringAttr("fifo_rd_addr_next"));
@@ -168,6 +179,22 @@ struct FIFOLowering : public OpConversionPattern<seq::FIFOOp> {
           ->setAttr("sv.namehint", rewriter.getStringAttr("fifo_almost_empty"));
     }
 
+    // ====== Protocol checks =====
+    Value clkI1 = rewriter.create<seq::FromClockOp>(loc, clk);
+    Value notEmptyAndRden = comb::createOrFoldNot(
+        loc, rewriter.create<comb::AndOp>(loc, adaptor.getRdEn(), fifoEmpty),
+        rewriter);
+    rewriter.create<verif::ClockedAssertOp>(
+        loc, notEmptyAndRden, verif::ClockEdge::Pos, clkI1, /*enable=*/Value(),
+        rewriter.getStringAttr("FIFO empty when read enabled"));
+    Value notFullAndWren = comb::createOrFoldNot(
+        loc, rewriter.create<comb::AndOp>(loc, adaptor.getWrEn(), fifoFull),
+        rewriter);
+    rewriter.create<verif::ClockedAssertOp>(
+        loc, notFullAndWren, verif::ClockEdge::Pos, clkI1,
+        /*enable=*/Value(),
+        rewriter.getStringAttr("FIFO full when write enabled"));
+
     rewriter.replaceOp(mem, results);
     return success();
   }
@@ -186,7 +213,8 @@ void LowerSeqFIFOPass::runOnOperation() {
 
   // Lowering patterns must lower away all HLMem-related operations.
   target.addIllegalOp<seq::FIFOOp>();
-  target.addLegalDialect<seq::SeqDialect, hw::HWDialect, comb::CombDialect>();
+  target.addLegalDialect<seq::SeqDialect, hw::HWDialect, comb::CombDialect,
+                         verif::VerifDialect>();
   RewritePatternSet patterns(&ctxt);
   patterns.add<FIFOLowering>(&ctxt);
 
diff --git a/test/Dialect/Seq/lower-fifo.mlir b/test/Dialect/Seq/lower-fifo.mlir
@@ -4,94 +4,37 @@
 // RUN: circt-opt --lower-seq-fifo --canonicalize %s | FileCheck %s --implicit-check-not=seq.fifo
 
 
-// CHECK:   hw.module @fifo1(in %[[CLOCK:.*]] : !seq.clock, in %[[VAL_1:.*]] : i1, in %[[VAL_2:.*]] : i32, in %[[VAL_3:.*]] : i1, in %[[VAL_4:.*]] : i1, out out : i32) {
-// CHECK:           %[[VAL_6:.*]] = hw.constant -1 : i2
-// CHECK:           %[[VAL_5:.*]] = hw.constant true
-// CHECK:           %[[VAL_7:.*]] = hw.constant -2 : i2
-// CHECK:           %[[VAL_8:.*]] = hw.constant 1 : i2
-// CHECK:           %[[VAL_9:.*]] = hw.constant 0 : i2
-// CHECK:           %[[VAL_10:.*]] = seq.compreg sym @fifo_count  %[[VAL_11:.*]], %[[CLOCK]] reset %[[VAL_1]], %[[VAL_9]]  : i2
-// CHECK:           %[[VAL_12:.*]] = seq.hlmem @fifo_mem %[[CLOCK]], %[[VAL_1]] : <3xi32>
-// CHECK:           %[[VAL_13:.*]] = seq.compreg sym @fifo_rd_addr  %[[VAL_14:.*]], %[[CLOCK]] reset %[[VAL_1]], %[[VAL_9]]  : i2
-// CHECK:           %[[VAL_15:.*]] = seq.compreg sym @fifo_wr_addr  %[[VAL_16:.*]], %[[CLOCK]] reset %[[VAL_1]], %[[VAL_9]]  : i2
-// CHECK:           %[[VAL_17:.*]] = seq.read %[[VAL_12]]{{\[}}%[[VAL_13]]] rden %[[VAL_3]] {latency = 0 : i64} : !seq.hlmem<3xi32>
-// CHECK:           seq.write %[[VAL_12]]{{\[}}%[[VAL_15]]] %[[VAL_2]] wren %[[VAL_4]] {latency = 1 : i64} : !seq.hlmem<3xi32>
-// CHECK:           %[[VAL_18:.*]] = comb.xor %[[VAL_3]], %[[VAL_5]] : i1
-// CHECK:           %[[VAL_19:.*]] = comb.xor %[[VAL_4]], %[[VAL_5]] : i1
-// CHECK:           %[[VAL_20:.*]] = comb.and %[[VAL_3]], %[[VAL_19]] : i1
-// CHECK:           %[[VAL_21:.*]] = comb.and %[[VAL_4]], %[[VAL_18]] : i1
-// CHECK:           %[[VAL_22:.*]] = comb.icmp eq %[[VAL_10]], %[[VAL_7]] : i2
-// CHECK:           %[[VAL_23:.*]] = comb.add %[[VAL_10]], %[[VAL_8]] : i2
-// CHECK:           %[[VAL_24:.*]] = comb.mux %[[VAL_22]], %[[VAL_10]], %[[VAL_23]] : i2
-// CHECK:           %[[VAL_25:.*]] = comb.icmp eq %[[VAL_10]], %[[VAL_9]] : i2
-// CHECK:           %[[VAL_26:.*]] = comb.add %[[VAL_10]], %[[VAL_6]] : i2
-// CHECK:           %[[VAL_27:.*]] = comb.xor %[[VAL_20]], %[[VAL_5]] : i1
-// CHECK:           %[[VAL_28:.*]] = comb.or %[[VAL_27]], %[[VAL_25]] : i1
-// CHECK:           %[[VAL_29:.*]] = comb.mux %[[VAL_28]], %[[VAL_10]], %[[VAL_26]] : i2
-// CHECK:           %[[VAL_30:.*]] = comb.mux %[[VAL_21]], %[[VAL_24]], %[[VAL_29]] : i2
-// CHECK:           %[[VAL_31:.*]] = comb.or %[[VAL_3]], %[[VAL_4]] : i1
-// CHECK:           %[[VAL_11]] = comb.mux %[[VAL_31]], %[[VAL_30]], %[[VAL_10]] {sv.namehint = "fifo_count_next"} : i2
-// CHECK:           %[[VAL_32:.*]] = comb.icmp ne %[[VAL_10]], %[[VAL_7]] : i2
-// CHECK:           %[[VAL_33:.*]] = comb.and %[[VAL_4]], %[[VAL_32]] : i1
-// CHECK:           %[[VAL_34:.*]] = comb.add %[[VAL_15]], %[[VAL_8]] : i2
-// CHECK:           %[[VAL_16]] = comb.mux %[[VAL_33]], %[[VAL_34]], %[[VAL_15]] {sv.namehint = "fifo_wr_addr_next"} : i2
-// CHECK:           %[[VAL_35:.*]] = comb.icmp ne %[[VAL_10]], %[[VAL_9]] : i2
-// CHECK:           %[[VAL_36:.*]] = comb.and %[[VAL_3]], %[[VAL_35]] : i1
-// CHECK:           %[[VAL_37:.*]] = comb.add %[[VAL_13]], %[[VAL_8]] : i2
-// CHECK:           %[[VAL_14]] = comb.mux %[[VAL_36]], %[[VAL_37]], %[[VAL_13]] {sv.namehint = "fifo_rd_addr_next"} : i2
-// CHECK:           hw.output %[[VAL_17]] : i32
-// CHECK:         }
+// CHECK:  hw.module @fifo1(in %[[CLOCK:.*]] : !seq.clock, in %[[VAL_1:.*]] : i1, in %[[VAL_2:.*]] : i32, in %[[VAL_3:.*]] : i1, in %[[VAL_4:.*]] : i1, out out : i32) {
+// CHECK:    %fifo_count = seq.compreg sym @fifo_count %{{.+}}, %clk reset %rst, %c0_i2 : i2  
+// CHECK:    %fifo_mem = seq.hlmem @fifo_mem %clk, %rst : <3xi32>
+// CHECK:    %fifo_rd_addr = seq.compreg sym @fifo_rd_addr %{{.+}}, %clk reset %rst, %c0_i2 : i2  
+// CHECK:    %fifo_wr_addr = seq.compreg sym @fifo_wr_addr %{{.+}}, %clk reset %rst, %c0_i2 : i2  
+// CHECK:    %fifo_mem_rdata = seq.read %fifo_mem[%fifo_rd_addr] rden %rdEn {latency = 0 : i64} : !seq.hlmem<3xi32>
+// CHECK:    seq.write %fifo_mem[%fifo_wr_addr] %in wren %wrEn {latency = 1 : i64} : !seq.hlmem<3xi32>
+//           All of the comb logic which would be here is pretty much impossible
+//           to verify visually. As a rule, if it's difficult to verify
+//           visually, that's a candidate for a new op: #8002. Since I haven't
+//           verified it visually, I'm not including it here. There are
+//           integration tests for it.
+// CHECK:    verif.clocked_assert %{{.+}}, posedge %{{.+}} label "FIFO empty when read enabled" : i1
+// CHECK:    verif.clocked_assert %{{.+}}, posedge %{{.+}} label "FIFO full when write enabled" : i1
+// CHECK:    hw.output %fifo_mem_rdata : i32
 hw.module @fifo1(in %clk : !seq.clock, in %rst : i1, in %in : i32, in %rdEn : i1, in %wrEn : i1, out out : i32) {
   %out, %full, %empty = seq.fifo depth 3 in %in rdEn %rdEn wrEn %wrEn clk %clk rst %rst : i32
   hw.output %out : i32
 }
 
 
 // CHECK:   hw.module @fifo2(in %[[CLOCK:.*]] : !seq.clock, in %[[VAL_1:.*]] : i1, in %[[VAL_2:.*]] : [[TY:.+]], in %[[VAL_3:.*]] : i1, in %[[VAL_4:.*]] : i1, out out : [[TY]], out empty : i1, out full : i1, out almost_empty : i1, out almost_full : i1) {
-// CHECK:           %[[VAL_5:.*]] = hw.constant 2 : i3
-// CHECK:           %[[VAL_8:.*]] = hw.constant -1 : i3
-// CHECK:           %[[VAL_7:.*]] = hw.constant true
-// CHECK:           %[[VAL_6:.*]] = hw.constant 0 : i2
-// CHECK:           %[[VAL_9:.*]] = hw.constant 3 : i3
-// CHECK:           %[[VAL_10:.*]] = hw.constant 1 : i3
-// CHECK:           %[[VAL_11:.*]] = hw.constant 0 : i3
-// CHECK:           %[[VAL_12:.*]] = hw.constant 1 : i2
-// CHECK:           %[[VAL_13:.*]] = seq.compreg sym @fifo_count  %[[VAL_14:.*]], %[[CLOCK]] reset %[[VAL_1]], %[[VAL_11]]  : i3
-// CHECK:           %[[VAL_15:.*]] = seq.hlmem @fifo_mem %[[CLOCK]], %[[VAL_1]] : <4x[[TY]]>
-// CHECK:           %[[VAL_16:.*]] = seq.compreg sym @fifo_rd_addr  %[[VAL_17:.*]], %[[CLOCK]] reset %[[VAL_1]], %[[VAL_6]]  : i2
-// CHECK:           %[[VAL_18:.*]] = seq.compreg sym @fifo_wr_addr  %[[VAL_19:.*]], %[[CLOCK]] reset %[[VAL_1]], %[[VAL_6]]  : i2
-// CHECK:           %[[VAL_20:.*]] = seq.read %[[VAL_15]]{{\[}}%[[VAL_16]]] rden %[[VAL_3]] {latency = 1 : i64} : !seq.hlmem<4x[[TY]]>
-// CHECK:           seq.write %[[VAL_15]]{{\[}}%[[VAL_18]]] %[[VAL_2]] wren %[[VAL_4]] {latency = 1 : i64} : !seq.hlmem<4x[[TY]]>
-// CHECK:           %[[VAL_21:.*]] = comb.icmp eq %[[VAL_13]], %[[VAL_9]] {sv.namehint = "fifo_full"} : i3
-// CHECK:           %[[VAL_22:.*]] = comb.icmp eq %[[VAL_13]], %[[VAL_11]] {sv.namehint = "fifo_empty"} : i3
-// CHECK:           %[[VAL_23:.*]] = comb.xor %[[VAL_3]], %[[VAL_7]] : i1
-// CHECK:           %[[VAL_24:.*]] = comb.xor %[[VAL_4]], %[[VAL_7]] : i1
-// CHECK:           %[[VAL_25:.*]] = comb.and %[[VAL_3]], %[[VAL_24]] : i1
-// CHECK:           %[[VAL_26:.*]] = comb.and %[[VAL_4]], %[[VAL_23]] : i1
-// CHECK:           %[[VAL_27:.*]] = comb.icmp eq %[[VAL_13]], %[[VAL_9]] : i3
-// CHECK:           %[[VAL_28:.*]] = comb.add %[[VAL_13]], %[[VAL_10]] : i3
-// CHECK:           %[[VAL_29:.*]] = comb.mux %[[VAL_27]], %[[VAL_13]], %[[VAL_28]] : i3
-// CHECK:           %[[VAL_30:.*]] = comb.icmp eq %[[VAL_13]], %[[VAL_11]] : i3
-// CHECK:           %[[VAL_31:.*]] = comb.add %[[VAL_13]], %[[VAL_8]] : i3
-// CHECK:           %[[VAL_32:.*]] = comb.xor %[[VAL_25]], %[[VAL_7]] : i1
-// CHECK:           %[[VAL_33:.*]] = comb.or %[[VAL_32]], %[[VAL_30]] : i1
-// CHECK:           %[[VAL_34:.*]] = comb.mux %[[VAL_33]], %[[VAL_13]], %[[VAL_31]] : i3
-// CHECK:           %[[VAL_35:.*]] = comb.mux %[[VAL_26]], %[[VAL_29]], %[[VAL_34]] : i3
-// CHECK:           %[[VAL_36:.*]] = comb.or %[[VAL_3]], %[[VAL_4]] : i1
-// CHECK:           %[[VAL_14]] = comb.mux %[[VAL_36]], %[[VAL_35]], %[[VAL_13]] {sv.namehint = "fifo_count_next"} : i3
-// CHECK:           %[[VAL_37:.*]] = comb.xor %[[VAL_21]], %[[VAL_7]] : i1
-// CHECK:           %[[VAL_38:.*]] = comb.and %[[VAL_4]], %[[VAL_37]] : i1
-// CHECK:           %[[VAL_39:.*]] = comb.add %[[VAL_18]], %[[VAL_12]] : i2
-// CHECK:           %[[VAL_19]] = comb.mux %[[VAL_38]], %[[VAL_39]], %[[VAL_18]] {sv.namehint = "fifo_wr_addr_next"} : i2
-// CHECK:           %[[VAL_40:.*]] = comb.xor %[[VAL_22]], %[[VAL_7]] : i1
-// CHECK:           %[[VAL_41:.*]] = comb.and %[[VAL_3]], %[[VAL_40]] : i1
-// CHECK:           %[[VAL_42:.*]] = comb.add %[[VAL_16]], %[[VAL_12]] : i2
-// CHECK:           %[[VAL_17]] = comb.mux %[[VAL_41]], %[[VAL_42]], %[[VAL_16]] {sv.namehint = "fifo_rd_addr_next"} : i2
-// CHECK:           %[[VAL_43:.*]] = comb.extract %[[VAL_13]] from 1 : (i3) -> i2
-// CHECK:           %[[VAL_44:.*]] = comb.icmp ne %[[VAL_43]], %[[VAL_6]] {sv.namehint = "fifo_almost_full"} : i2
-// CHECK:           %[[VAL_45:.*]] = comb.icmp ult %[[VAL_13]], %[[VAL_5]] {sv.namehint = "fifo_almost_empty"} : i3
-  // CHECK:           hw.output %[[VAL_20]], %[[VAL_22]], %[[VAL_21]], %[[VAL_45]], %[[VAL_44]] : [[TY]], i1, i1, i1, i1
-// CHECK:         }
+// CHECK:     %fifo_count = seq.compreg sym @fifo_count %16, %clk reset %rst, %c0_i3 : i3  
+// CHECK:     %fifo_mem = seq.hlmem @fifo_mem %clk, %rst : <4x!hw.array<2xi32>>
+// CHECK:     %fifo_rd_addr = seq.compreg sym @fifo_rd_addr %28, %clk reset %rst, %c0_i2 : i2  
+// CHECK:     %fifo_wr_addr = seq.compreg sym @fifo_wr_addr %22, %clk reset %rst, %c0_i2 : i2  
+// CHECK:     %fifo_mem_rdata = seq.read %fifo_mem[%fifo_rd_addr] rden %rdEn {latency = 1 : i64} : !seq.hlmem<4x!hw.array<2xi32>>
+// CHECK:     seq.write %fifo_mem[%fifo_wr_addr] %in wren %wrEn {latency = 1 : i64} : !seq.hlmem<4x!hw.array<2xi32>>
+//            See comment above.
+// CHECK:     verif.clocked_assert %{{.+}}, posedge %{{.+}} label "FIFO empty when read enabled" : i1
+// CHECK:     verif.clocked_assert %{{.+}}, posedge %{{.+}} label "FIFO full when write enabled" : i1
 !testType = !hw.array<2xi32>
 hw.module @fifo2(in %clk : !seq.clock, in %rst : i1, in %in : !testType, in %rdEn : i1, in %wrEn : i1, out out: !testType, out empty: i1, out full: i1, out almost_empty : i1, out almost_full : i1) {
   %out, %full, %empty, %almostFull, %almostEmpty = seq.fifo depth 4 rd_latency 1 almost_full 2 almost_empty 1 in %in rdEn %rdEn wrEn %wrEn clk %clk rst %rst : !testType
