[t1rocket] use ltl api

ipemu/src/TestBench.scala

@@ -10,6 +10,8 @@ import chisel3.experimental.{ExtModule, SerializableModuleGenerator}
 import chisel3.properties.{AnyClassType, Class, ClassType, Property}
 import chisel3.util.circt.dpi.{RawClockedNonVoidFunctionCall, RawClockedVoidFunctionCall, RawUnclockedNonVoidFunctionCall}
 import chisel3.util.{HasExtModuleInline, PopCount, UIntToOH, Valid}
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.amba.axi4.bundle._
 import org.chipsalliance.t1.ipemu.dpi._
 import org.chipsalliance.t1.rtl.{T1, T1Parameter}
@@ -271,7 +273,7 @@ class TestBench(generator: SerializableModuleGenerator[T1, T1Parameter])
       }
       when(scoreboardEnq(tag)) {
         scoreboard.valid := true.B
-        assert(!scoreboard.valid)
+        AssertProperty(BoolSequence(!scoreboard.valid))
         scoreboard.bits := 0.U
       }
   }

rocketv/src/CSR.scala

@@ -8,6 +8,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.instantiable
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 // @todo: remove me
 import org.chipsalliance.rocketv.rvdecoderdbcompat._
 
@@ -1175,8 +1177,8 @@ class CSR(val parameter: CSRParameter)
 
   when(io.retire(0) || exception) { reg_singleStepped := true.B }
   when(!io.singleStep) { reg_singleStepped := false.B }
-  assert(!io.singleStep || io.retire <= 1.U)
-  assert(!reg_singleStepped || io.retire === 0.U)
+  AssertProperty(BoolSequence(!io.singleStep || io.retire <= 1.U))
+  AssertProperty(BoolSequence(!reg_singleStepped || io.retire === 0.U))
 
   val epc = formEPC(io.pc)
   val tval = Mux(insn_break, epc, io.tval)
@@ -1349,7 +1351,7 @@ class CSR(val parameter: CSRParameter)
   val set_fs_dirty = WireDefault(io.setFsDirty.getOrElse(false.B))
   if (coreParams.haveFSDirty) {
     when(set_fs_dirty) {
-      assert(reg_mstatus.fs > 0.U)
+      AssertProperty(BoolSequence(reg_mstatus.fs > 0.U))
       when(reg_mstatus.v) { reg_vsstatus.fs := 3.U }
       reg_mstatus.fs := 3.U
     }

rocketv/src/FPU.scala

@@ -10,6 +10,8 @@ import chisel3.experimental.{BaseModule, SerializableModule, SerializableModuleP
 import chisel3.probe.{define, Probe, ProbeValue}
 import chisel3.util._
 import chisel3.util.circt.ClockGate
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 
 class FPUWrite(param: FPUParameter) extends Bundle {
   val rfWen:   Bool = Bool()
@@ -129,7 +131,7 @@ class FPU(val parameter: FPUParameter)
     when(load_wb) {
       val wdata = recode(load_wb_data, load_wb_typeTag)
       regfile(load_wb_tag) := wdata
-      assert(consistent(wdata))
+      AssertProperty(BoolSequence(consistent(wdata)))
     }
 
     val ex_rs = ex_ra.map(a => regfile(a))
@@ -346,7 +348,7 @@ class FPU(val parameter: FPUParameter)
     val wdata = box(Mux(divSqrt_wen, divSqrt_wdata, VecInit(pipes.map(_.res.data))(wbInfo(0).pipeid)), wtypeTag)
     val wexc = VecInit(pipes.map(_.res.exc))(wbInfo(0).pipeid)
     when((!wbInfo(0).cp && wen(0)) || divSqrt_wen) {
-      assert(consistent(wdata))
+      AssertProperty(BoolSequence(consistent(wdata)))
       regfile(waddr) := wdata
     }
 

rocketv/src/Frontend.scala

@@ -10,6 +10,8 @@ import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util._
 import chisel3.util.circt.ClockGate
 import chisel3.util.experimental.BitSet
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.amba.axi4.bundle.{AXI4BundleParameter, AXI4ROIrrevocable, AXI4RWIrrevocable}
 
 object FrontendParameter {
@@ -310,7 +312,7 @@ class Frontend(val parameter: FrontendParameter)
   fq.io.clock := io.clock
   fq.io.reset := io.reset.asBool || io.nonDiplomatic.cpu.req.valid
 
-  assert(!(io.nonDiplomatic.cpu.req.valid || io.nonDiplomatic.cpu.sfence.valid || io.nonDiplomatic.cpu.flush_icache || io.nonDiplomatic.cpu.bht_update.valid || io.nonDiplomatic.cpu.btb_update.valid) || io.nonDiplomatic.cpu.might_request)
+  AssertProperty(BoolSequence(!(io.nonDiplomatic.cpu.req.valid || io.nonDiplomatic.cpu.sfence.valid || io.nonDiplomatic.cpu.flush_icache || io.nonDiplomatic.cpu.bht_update.valid || io.nonDiplomatic.cpu.btb_update.valid) || io.nonDiplomatic.cpu.might_request))
 
   withClock(gated_clock) { // entering gated-clock domain
     val s1_valid = Reg(Bool())
@@ -582,7 +584,7 @@ class Frontend(val parameter: FrontendParameter)
         }
       }
 
-      assert(!s2_partial_insn_valid || fq.io.enq.bits.mask(0))
+      AssertProperty(BoolSequence(!s2_partial_insn_valid || fq.io.enq.bits.mask(0)))
       when(s2_redirect) { s2_partial_insn_valid := false.B }
       when(io.nonDiplomatic.cpu.req.valid) { wrong_path := false.B }
     }

rocketv/src/HellaCache.scala

@@ -9,6 +9,8 @@ import chisel3.experimental.hierarchy.{Instance, Instantiate, instantiable}
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter, SourceInfo}
 import chisel3.util.experimental.{BitSet, InlineInstance}
 import chisel3.util.{Arbiter, BitPat, Cat, Enum, Fill, FillInterleaved, Mux1H, MuxLookup, OHToUInt, PriorityEncoder, PriorityEncoderOH, PriorityMux, Queue, RegEnable, SRAM, SRAMInterface, UIntToOH, isPow2, log2Ceil}
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.amba.axi4.bundle.{AXI4BundleParameter, AXI4ChiselBundle, AXI4ROIrrevocable, AXI4RWIrrevocable, R, W}
 
 object HellaCacheParameter {
@@ -698,7 +700,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     val s1_mask_xwr = new StoreGen(s1_req.size, s1_req.addr, 0.U, wordBytes).mask
     val s1_mask = Mux(s1_req.cmd === M_PWR, io.cpu.s1_data.mask, s1_mask_xwr)
     // for partial writes, s1_data.mask must be a subset of s1_mask_xwr
-    assert(!(s1_valid_masked && s1_req.cmd === M_PWR) || (s1_mask_xwr | ~io.cpu.s1_data.mask).andR)
+    AssertProperty(BoolSequence(!(s1_valid_masked && s1_req.cmd === M_PWR) || (s1_mask_xwr | ~io.cpu.s1_data.mask).andR))
 
     val s2_valid = RegNext(s1_valid_masked && !s1_sfence, init = false.B)
     val s2_valid_no_xcpt = s2_valid && !io.cpu.s2_xcpt.asUInt.orR
@@ -889,7 +891,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     val pstore1_valid = s2_store_valid || pstore1_held
     any_pstore_valid := pstore1_held || pstore2_valid
     val pstore_drain_structural = pstore1_valid_likely && pstore2_valid && ((s1_valid && s1_write) || pstore1_rmw)
-    assert(pstore1_rmw || pstore1_valid_not_rmw(io.cpu.s2_kill) === pstore1_valid)
+    AssertProperty(BoolSequence(pstore1_rmw || pstore1_valid_not_rmw(io.cpu.s2_kill) === pstore1_valid))
     ccover(pstore_drain_structural, "STORE_STRUCTURAL_HAZARD", "D$ read-modify-write structural hazard")
     ccover(pstore1_valid && pstore_drain_on_miss, "STORE_DRAIN_ON_MISS", "D$ store buffer drain on miss")
     ccover(s1_valid_not_nacked && s1_waw_hazard, "WAW_HAZARD", "D$ write-after-write hazard")
@@ -990,7 +992,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     // !s2_uncached -> read cache line
     val accessWillRead: Bool = !s2_uncached || !s2_write
     // If no managers support atomics, assert fail if processor asks for them
-    assert(!(memAccessValid && s2_read && s2_write && s2_uncached))
+    AssertProperty(BoolSequence(!(memAccessValid && s2_read && s2_write && s2_uncached)))
     io.loadStoreAXI.ar.valid := memAccessValid && accessWillRead
     io.loadStoreAXI.ar.bits := DontCare
     io.loadStoreAXI.ar.bits.burst := 1.U
@@ -1116,7 +1118,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     when(io.loadStoreAXI.r.fire) {
       when(grantIsCached) {
         grantInProgress := true.B
-        assert(cached_grant_wait, "A GrantData was unexpected by the dcache.")
+        AssertProperty(BoolSequence(cached_grant_wait))
         when(d_last) {
           cached_grant_wait := false.B
           grantInProgress := false.B
@@ -1153,7 +1155,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     uncachedAckIndex.asBools.zip(uncachedInFlight).foreach {
       case (s, f) =>
         when(s) {
-          assert(f, "An uncached AccessAck was unexpected by the dcache.") // TODO must handle Ack coming back on same cycle!
+          AssertProperty(BoolSequence(f)) // TODO must handle Ack coming back on same cycle!
           f := false.B
         }
     }
@@ -1168,7 +1170,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     // Finish TileLink transaction by issuing a GrantAck
     // tl_out.e.valid := tl_out.d.valid && d_first && grantIsCached && canAcceptCachedGrant
     // tl_out.e.bits := edge.GrantAck(tl_out.d.bits)
-    // assert(tl_out.e.fire === (tl_out.d.fire && d_first && grantIsCached))
+    // AssertProperty(BoolSequence(tl_out.e.fire === (tl_out.d.fire && d_first && grantIsCached)))
 
     // data refill
     // note this ready-valid signaling ignores E-channel backpressure, which
@@ -1283,7 +1285,7 @@ class HellaCache(val parameter: HellaCacheParameter)
 
     if (!usingDataScratchpad) {
       when(s2_victimize) {
-        assert(s2_valid_flush_line || s2_flush_valid || io.cpu.s2_nack)
+        AssertProperty(BoolSequence(s2_valid_flush_line || s2_flush_valid || io.cpu.s2_nack))
         val discard_line = s2_valid_flush_line && s2_req.size(1) || s2_flush_valid && flushing_req.size(1)
         release_state := Mux(
           s2_victim_dirty && !discard_line,
@@ -1344,7 +1346,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     io.cpu.s2_xcpt := Mux(RegNext(s1_xcpt_valid), s2_tlb_xcpt, 0.U.asTypeOf(s2_tlb_xcpt))
 
     if (usingDataScratchpad) {
-      assert(!(s2_valid_masked && (s2_req.cmd === M_XLR || s2_req.cmd === M_XSC)))
+      AssertProperty(BoolSequence(!(s2_valid_masked && (s2_req.cmd === M_XLR || s2_req.cmd === M_XSC))))
     } else {
       // ccover(tl_out.b.valid && !tl_out.b.ready, "BLOCK_B", "D$ B-channel blocked")
     }
@@ -1360,7 +1362,7 @@ class HellaCache(val parameter: HellaCacheParameter)
     io.cpu.resp.valid := (s2_valid_hit_pre_data_ecc || doUncachedResp) && !s2_data_error
     io.cpu.replay_next := io.loadStoreAXI.r.fire && grantIsUncachedData && !cacheParams.separateUncachedResp.B
     when(doUncachedResp) {
-      assert(!s2_valid_hit)
+      AssertProperty(BoolSequence(!s2_valid_hit))
       io.cpu.resp.bits.replay := true.B
       io.cpu.resp.bits.addr := s2_uncached_resp_addr
     }
@@ -1412,7 +1414,7 @@ class HellaCache(val parameter: HellaCacheParameter)
       })
     }.getOrElse {
       if (!usingAtomics) {
-        assert(!(s1_valid_masked && s1_read && s1_write), "unsupported D$ operation")
+        AssertProperty(BoolSequence(!(s1_valid_masked && s1_read && s1_write)))
       }
     }
 
@@ -1627,7 +1629,7 @@ class HellaCache(val parameter: HellaCacheParameter)
   def likelyNeedsRead(req: HellaCacheReq): Bool = {
     // req.cmd.isOneOf(M_XWR, M_PFW)
     val res = !Seq(M_XWR, M_PFW).map(_ === req.cmd).reduce(_ ||_) || req.size < log2Ceil(eccBytes).U
-    assert(!needsRead(req) || res)
+    AssertProperty(BoolSequence(!needsRead(req) || res))
     res
   }
 

rocketv/src/IBuf.scala

@@ -7,6 +7,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.{Instantiate, instantiable}
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 
 object IBufParameter {
   implicit def rwP: upickle.default.ReadWriter[IBufParameter] = upickle.default.macroRW[IBufParameter]
@@ -142,7 +144,7 @@ class IBuf(val parameter: IBufParameter)
   val xcpt = (0 until bufMask.getWidth).map(i => Mux(bufMask(i), buf.xcpt, io.imem.bits.xcpt))
   val buf_replay = Mux(buf.replay, bufMask, 0.U)
   val ic_replay = buf_replay | Mux(io.imem.bits.replay, valid & ~bufMask, 0.U)
-  assert(!io.imem.valid || !io.imem.bits.btb.taken || io.imem.bits.btb.bridx >= pcWordBits)
+  AssertProperty(BoolSequence(!io.imem.valid || !io.imem.bits.btb.taken || io.imem.bits.btb.bridx >= pcWordBits))
 
   io.btb_resp := io.imem.bits.btb
   io.pc := Mux(nBufValid > 0.U, buf.pc, io.imem.bits.pc)

rocketv/src/ICache.scala

@@ -9,6 +9,8 @@ import chisel3.experimental.hierarchy.instantiable
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util.random.LFSR
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.amba.axi4.bundle.{AXI4BundleParameter, AXI4ROIrrevocable, AXI4RWIrrevocable}
 
 case class ICacheParameter(useAsyncReset: Boolean,
@@ -345,7 +347,7 @@ class ICache(val parameter: ICacheParameter)
         val mask = nWays - (BigInt(1) << (i + 1))
         v = v | (lineInScratchpad(Cat(v0 | mask.U, refill_idx)) << i)
       }
-      assert(!lineInScratchpad(Cat(v, refill_idx)))
+      AssertProperty(BoolSequence(!lineInScratchpad(Cat(v, refill_idx))))
       v
     }
 
@@ -700,7 +702,7 @@ class ICache(val parameter: ICacheParameter)
           //            ccover(itim_increase && refilling, "ITIM_SIZE_INCREASE_WHILE_REFILL", "ITIM size increased while I$ refill")
         }
 
-        assert(!s2_valid || RegNext(RegNext(s0_vaddr)) === io.s2_vaddr)
+        AssertProperty(BoolSequence(!s2_valid || RegNext(RegNext(s0_vaddr)) === io.s2_vaddr))
         when(
           !(axi.w.valid || s1_slaveValid || s2_slaveValid || respValid)
             && s2_valid && s2_data_decoded.error && !s2_tag_disparity
@@ -844,7 +846,7 @@ class ICache(val parameter: ICacheParameter)
   // tl_out.b.ready := true.B
   // tl_out.c.valid := false.B
   // tl_out.e.valid := false.B
-  assert(!(io.instructionFetchAXI.ar.valid && addrMaybeInScratchpad(io.instructionFetchAXI.ar.bits.addr)))
+  AssertProperty(BoolSequence(!(io.instructionFetchAXI.ar.valid && addrMaybeInScratchpad(io.instructionFetchAXI.ar.bits.addr))))
 
   // if there is an outstanding refill, cannot flush I$.
   when(!refill_valid) { invalidated := false.B }

rocketv/src/PTW.scala

@@ -9,6 +9,8 @@ import chisel3.experimental.hierarchy.instantiable
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util.circt.ClockGate
 import chisel3.util.{Arbiter, Cat, Enum, Mux1H, OHToUInt, PopCount, PriorityEncoder, PriorityEncoderOH, RegEnable, SRAM, SRAMInterface, UIntToOH, Valid, is, isPow2, log2Ceil, switch}
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 
 object PTWParameter {
   implicit def rwP: upickle.default.ReadWriter[PTWParameter] = upickle.default.macroRW[PTWParameter]
@@ -323,7 +325,7 @@ class PTW(val parameter: PTWParameter)
     val mem_resp_valid = RegNext(io.mem.resp.valid)
     val mem_resp_data = RegNext(io.mem.resp.bits.data)
     io.mem.uncached_resp.map { resp =>
-      assert(!(resp.valid && io.mem.resp.valid))
+      AssertProperty(BoolSequence(!(resp.valid && io.mem.resp.valid)))
       resp.ready := true.B
       when(resp.valid) {
         mem_resp_valid := true.B
@@ -570,7 +572,7 @@ class PTW(val parameter: PTWParameter)
         io.dpath.perf.l2hit := s2_hit
         when(s2_hit) {
           l2_plru.access(r_idx, OHToUInt(s2_hit_vec))
-          assert((PopCount(s2_hit_vec) === 1.U) || s2_error, "L2 TLB multi-hit")
+          AssertProperty(BoolSequence((PopCount(s2_hit_vec) === 1.U) || s2_error))
         }
 
         val s2_pte = Wire(new PTE)
@@ -706,7 +708,7 @@ class PTW(val parameter: PTWParameter)
           resp_fragmented_superpage := false.B
           r_hgatp := io.dpath.hgatp
 
-          assert(!arb.io.out.bits.bits.need_gpa || arb.io.out.bits.bits.stage2)
+          AssertProperty(BoolSequence(!arb.io.out.bits.bits.need_gpa || arb.io.out.bits.bits.stage2))
         }
       }
       is(s_req) {
@@ -812,13 +814,13 @@ class PTW(val parameter: PTWParameter)
     )
 
     when(l2_hit && !l2_error) {
-      assert(state === s_req || state === s_wait1)
+      AssertProperty(BoolSequence(state === s_req || state === s_wait1))
       next_state := s_ready
       resp_valid(r_req_dest) := true.B
       count := (pgLevels - 1).U
     }
     when(mem_resp_valid) {
-      assert(state === s_wait3)
+      AssertProperty(BoolSequence(state === s_wait3))
       next_state := s_req
       when(traverse) {
         when(do_both_stages && !stage2) { do_switch := true.B }
@@ -864,7 +866,7 @@ class PTW(val parameter: PTWParameter)
       }
     }
     when(io.mem.s2_nack) {
-      assert(state === s_wait2)
+      AssertProperty(BoolSequence(state === s_wait2))
       next_state := s_req
     }
 

rocketv/src/RocketCore.scala

@@ -11,6 +11,8 @@ import chisel3.probe.{Probe, ProbeValue, define}
 import chisel3.util.circt.ClockGate
 import chisel3.util.experimental.decode.DecodeBundle
 import chisel3.util.{BitPat, Cat, DecoupledIO, Fill, MuxLookup, PriorityEncoder, PriorityMux, Queue, RegEnable, Valid, log2Ceil, log2Up}
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.rocketv.rvdecoderdbcompat.Causes
 import org.chipsalliance.rvdecoderdb.Instruction
 
@@ -1142,7 +1144,7 @@ class Rocket(val parameter: RocketParameter)
     csr.io.htval := {
       val htvalValidImem = wbRegException && wbRegCause === Causes.fetch_guest_page_fault.U
       val htvalImem = Mux(htvalValidImem, io.imem.gpa.bits, 0.U)
-      assert(!htvalValidImem || io.imem.gpa.valid)
+      AssertProperty(BoolSequence(!htvalValidImem || io.imem.gpa.valid))
 
       val htvalValidDmem =
         wbException && tvalDmemAddr && io.dmem.s2_xcpt.gf.asUInt.orR && !io.dmem.s2_xcpt.pf.asUInt.orR
@@ -1527,7 +1529,7 @@ class Rocket(val parameter: RocketParameter)
           io.dmem.replay_next || // long-latency load replaying
           (!longLatencyStall && (instructionBufferOut.valid || io.imem.resp.valid)) // instruction pending
 
-      assert(!(exPcValid || memPcValid || wbPcValid) || clockEnable)
+      AssertProperty(BoolSequence(!(exPcValid || memPcValid || wbPcValid) || clockEnable))
     }
 
     // evaluate performance counters

rocketv/src/TLB.scala

@@ -8,6 +8,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.{Instance, Instantiate, instantiable}
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util.{Cat, Decoupled, Enum, Fill, Mux1H, OHToUInt, PopCount, PriorityEncoder, UIntToOH, Valid, log2Ceil}
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 
 object TLBParameter {
   implicit def rwP: upickle.default.ReadWriter[TLBParameter] = upickle.default.macroRW[TLBParameter]
@@ -619,7 +621,7 @@ class TLB(val parameter: TLBParameter)
     when(state === s_request) {
       // SFENCE.VMA will kill TLB entries based on rs1 and rs2. It will take 1 cycle.
       when(sfence) { state := s_ready }
-      // here should be io.ptw.req.fire, but assert(io.ptw.req.ready === true.B)
+      // here should be io.ptw.req.fire, but AssertProperty(BoolSequence(io.ptw.req.ready === true.B))
       // fire -> s_wait
       when(io.ptw.req.ready) { state := Mux(sfence, s_wait_invalidate, s_wait) }
       // If CPU kills request(frontend.s2_redirect)
@@ -636,7 +638,7 @@ class TLB(val parameter: TLBParameter)
 
     // SFENCE processing logic.
     when(sfence) {
-      assert(!io.sfence.bits.rs1 || (io.sfence.bits.addr >> pgIdxBits) === vpn)
+      AssertProperty(BoolSequence(!io.sfence.bits.rs1 || (io.sfence.bits.addr >> pgIdxBits) === vpn))
       val hv = usingHypervisor.B && io.sfence.bits.hv
       val hg = usingHypervisor.B && io.sfence.bits.hg
       sectored_entries.flatten.foreach{ e =>

t1/src/Lane.scala

@@ -15,6 +15,8 @@ import chisel3.util.experimental.decode.DecodeBundle
 import org.chipsalliance.t1.rtl.decoder.{Decoder, DecoderParam}
 import org.chipsalliance.t1.rtl.lane._
 import org.chipsalliance.t1.rtl.vrf.{RamType, VRF, VRFParam, VRFProbe}
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 
 // 1. Coverage
 // 2. Performance signal via XMR
@@ -833,7 +835,7 @@ class Lane(val parameter: LaneParameter) extends Module with SerializableModule[
     queue.io.enq.bits.last := DontCare
     queue.io.enq.bits.instructionIndex := port.enq.bits.instructionIndex
     queue.io.enq.bits.mask := FillInterleaved(2, port.enq.bits.mask)
-    assert(queue.io.enq.ready || !port.enq.valid)
+    AssertProperty(BoolSequence(queue.io.enq.ready || !port.enq.valid))
     port.enqRelease := queue.io.deq.fire
   }