diff --git a/ipemu/src/TestBench.scala b/ipemu/src/TestBench.scala index 0d18057d8..897931d49 100644 --- a/ipemu/src/TestBench.scala +++ b/ipemu/src/TestBench.scala @@ -10,8 +10,6 @@ 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} @@ -273,7 +271,7 @@ class TestBench(generator: SerializableModuleGenerator[T1, T1Parameter]) } when(scoreboardEnq(tag)) { scoreboard.valid := true.B - AssertProperty(BoolSequence(!scoreboard.valid)) + assert(!scoreboard.valid) scoreboard.bits := 0.U } } diff --git a/rocketv/src/CSR.scala b/rocketv/src/CSR.scala index 3f5825fa2..aa72c4fda 100644 --- a/rocketv/src/CSR.scala +++ b/rocketv/src/CSR.scala @@ -8,8 +8,6 @@ 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._ @@ -1177,8 +1175,8 @@ class CSR(val parameter: CSRParameter) when(io.retire(0) || exception) { reg_singleStepped := true.B } when(!io.singleStep) { reg_singleStepped := false.B } - AssertProperty(BoolSequence(!io.singleStep || io.retire <= 1.U)) - AssertProperty(BoolSequence(!reg_singleStepped || io.retire === 0.U)) + assert(!io.singleStep || io.retire <= 1.U) + assert(!reg_singleStepped || io.retire === 0.U) val epc = formEPC(io.pc) val tval = Mux(insn_break, epc, io.tval) @@ -1351,7 +1349,7 @@ class CSR(val parameter: CSRParameter) val set_fs_dirty = WireDefault(io.setFsDirty.getOrElse(false.B)) if (coreParams.haveFSDirty) { when(set_fs_dirty) { - AssertProperty(BoolSequence(reg_mstatus.fs > 0.U)) + assert(reg_mstatus.fs > 0.U) when(reg_mstatus.v) { reg_vsstatus.fs := 3.U } reg_mstatus.fs := 3.U } diff --git a/rocketv/src/FPU.scala b/rocketv/src/FPU.scala index 89dfe7776..ab44e80fb 100644 --- a/rocketv/src/FPU.scala +++ b/rocketv/src/FPU.scala @@ -10,8 +10,6 @@ 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() @@ -132,7 +130,7 @@ class FPU(val parameter: FPUParameter) when(load_wb) { val wdata = recode(load_wb_data, load_wb_typeTag) regfile(load_wb_tag) := wdata - AssertProperty(BoolSequence(consistent(wdata))) + assert(consistent(wdata)) } val ex_rs = ex_ra.map(a => regfile(a)) @@ -349,7 +347,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) { - AssertProperty(BoolSequence(consistent(wdata))) + assert(consistent(wdata)) regfile(waddr) := wdata } diff --git a/rocketv/src/Frontend.scala b/rocketv/src/Frontend.scala index d46e14d15..36a313d84 100644 --- a/rocketv/src/Frontend.scala +++ b/rocketv/src/Frontend.scala @@ -10,8 +10,6 @@ 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 { @@ -312,7 +310,7 @@ class Frontend(val parameter: FrontendParameter) fq.io.clock := io.clock fq.io.reset := io.reset.asBool || io.nonDiplomatic.cpu.req.valid - 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)) + 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) withClock(gated_clock) { // entering gated-clock domain val s1_valid = Reg(Bool()) @@ -584,7 +582,7 @@ class Frontend(val parameter: FrontendParameter) } } - AssertProperty(BoolSequence(!s2_partial_insn_valid || fq.io.enq.bits.mask(0))) + assert(!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 } } diff --git a/rocketv/src/HellaCache.scala b/rocketv/src/HellaCache.scala index 0ef036e27..7a1b28048 100644 --- a/rocketv/src/HellaCache.scala +++ b/rocketv/src/HellaCache.scala @@ -9,8 +9,6 @@ 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 { @@ -700,7 +698,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 - AssertProperty(BoolSequence(!(s1_valid_masked && s1_req.cmd === M_PWR) || (s1_mask_xwr | ~io.cpu.s1_data.mask).andR)) + assert(!(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 @@ -891,7 +889,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) - AssertProperty(BoolSequence(pstore1_rmw || pstore1_valid_not_rmw(io.cpu.s2_kill) === pstore1_valid)) + assert(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") @@ -992,7 +990,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 - AssertProperty(BoolSequence(!(memAccessValid && s2_read && s2_write && s2_uncached))) + assert(!(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 @@ -1118,7 +1116,7 @@ class HellaCache(val parameter: HellaCacheParameter) when(io.loadStoreAXI.r.fire) { when(grantIsCached) { grantInProgress := true.B - AssertProperty(BoolSequence(cached_grant_wait)) + assert(cached_grant_wait, "A GrantData was unexpected by the dcache.") when(d_last) { cached_grant_wait := false.B grantInProgress := false.B @@ -1155,7 +1153,7 @@ class HellaCache(val parameter: HellaCacheParameter) uncachedAckIndex.asBools.zip(uncachedInFlight).foreach { case (s, f) => when(s) { - AssertProperty(BoolSequence(f)) // TODO must handle Ack coming back on same cycle! + assert(f, "An uncached AccessAck was unexpected by the dcache.") // TODO must handle Ack coming back on same cycle! f := false.B } } @@ -1170,7 +1168,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) - // AssertProperty(BoolSequence(tl_out.e.fire === (tl_out.d.fire && d_first && grantIsCached))) + // assert(tl_out.e.fire === (tl_out.d.fire && d_first && grantIsCached)) // data refill // note this ready-valid signaling ignores E-channel backpressure, which @@ -1285,7 +1283,7 @@ class HellaCache(val parameter: HellaCacheParameter) if (!usingDataScratchpad) { when(s2_victimize) { - AssertProperty(BoolSequence(s2_valid_flush_line || s2_flush_valid || io.cpu.s2_nack)) + assert(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, @@ -1346,7 +1344,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) { - AssertProperty(BoolSequence(!(s2_valid_masked && (s2_req.cmd === M_XLR || s2_req.cmd === M_XSC)))) + assert(!(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") } @@ -1362,7 +1360,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) { - AssertProperty(BoolSequence(!s2_valid_hit)) + assert(!s2_valid_hit) io.cpu.resp.bits.replay := true.B io.cpu.resp.bits.addr := s2_uncached_resp_addr } @@ -1414,7 +1412,7 @@ class HellaCache(val parameter: HellaCacheParameter) }) }.getOrElse { if (!usingAtomics) { - AssertProperty(BoolSequence(!(s1_valid_masked && s1_read && s1_write))) + assert(!(s1_valid_masked && s1_read && s1_write), "unsupported D$ operation") } } @@ -1629,7 +1627,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 - AssertProperty(BoolSequence(!needsRead(req) || res)) + assert(!needsRead(req) || res) res } diff --git a/rocketv/src/IBuf.scala b/rocketv/src/IBuf.scala index ce243f88f..781d2a94e 100644 --- a/rocketv/src/IBuf.scala +++ b/rocketv/src/IBuf.scala @@ -7,8 +7,6 @@ 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] @@ -144,7 +142,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) - AssertProperty(BoolSequence(!io.imem.valid || !io.imem.bits.btb.taken || io.imem.bits.btb.bridx >= pcWordBits)) + assert(!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) diff --git a/rocketv/src/ICache.scala b/rocketv/src/ICache.scala index a00531411..ca508f513 100644 --- a/rocketv/src/ICache.scala +++ b/rocketv/src/ICache.scala @@ -9,8 +9,6 @@ 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, @@ -347,7 +345,7 @@ class ICache(val parameter: ICacheParameter) val mask = nWays - (BigInt(1) << (i + 1)) v = v | (lineInScratchpad(Cat(v0 | mask.U, refill_idx)) << i) } - AssertProperty(BoolSequence(!lineInScratchpad(Cat(v, refill_idx)))) + assert(!lineInScratchpad(Cat(v, refill_idx))) v } @@ -702,7 +700,7 @@ class ICache(val parameter: ICacheParameter) // ccover(itim_increase && refilling, "ITIM_SIZE_INCREASE_WHILE_REFILL", "ITIM size increased while I$ refill") } - AssertProperty(BoolSequence(!s2_valid || RegNext(RegNext(s0_vaddr)) === io.s2_vaddr)) + assert(!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 @@ -846,7 +844,7 @@ class ICache(val parameter: ICacheParameter) // tl_out.b.ready := true.B // tl_out.c.valid := false.B // tl_out.e.valid := false.B - AssertProperty(BoolSequence(!(io.instructionFetchAXI.ar.valid && addrMaybeInScratchpad(io.instructionFetchAXI.ar.bits.addr)))) + assert(!(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 } diff --git a/rocketv/src/PTW.scala b/rocketv/src/PTW.scala index 64bdcaeb0..745e4aa66 100644 --- a/rocketv/src/PTW.scala +++ b/rocketv/src/PTW.scala @@ -9,8 +9,6 @@ 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] @@ -325,7 +323,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 => - AssertProperty(BoolSequence(!(resp.valid && io.mem.resp.valid))) + assert(!(resp.valid && io.mem.resp.valid)) resp.ready := true.B when(resp.valid) { mem_resp_valid := true.B @@ -572,7 +570,7 @@ class PTW(val parameter: PTWParameter) io.dpath.perf.l2hit := s2_hit when(s2_hit) { l2_plru.access(r_idx, OHToUInt(s2_hit_vec)) - AssertProperty(BoolSequence((PopCount(s2_hit_vec) === 1.U) || s2_error)) + assert((PopCount(s2_hit_vec) === 1.U) || s2_error, "L2 TLB multi-hit") } val s2_pte = Wire(new PTE) @@ -708,7 +706,7 @@ class PTW(val parameter: PTWParameter) resp_fragmented_superpage := false.B r_hgatp := io.dpath.hgatp - AssertProperty(BoolSequence(!arb.io.out.bits.bits.need_gpa || arb.io.out.bits.bits.stage2)) + assert(!arb.io.out.bits.bits.need_gpa || arb.io.out.bits.bits.stage2) } } is(s_req) { @@ -814,13 +812,13 @@ class PTW(val parameter: PTWParameter) ) when(l2_hit && !l2_error) { - AssertProperty(BoolSequence(state === s_req || state === s_wait1)) + assert(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) { - AssertProperty(BoolSequence(state === s_wait3)) + assert(state === s_wait3) next_state := s_req when(traverse) { when(do_both_stages && !stage2) { do_switch := true.B } @@ -866,7 +864,7 @@ class PTW(val parameter: PTWParameter) } } when(io.mem.s2_nack) { - AssertProperty(BoolSequence(state === s_wait2)) + assert(state === s_wait2) next_state := s_req } diff --git a/rocketv/src/RocketCore.scala b/rocketv/src/RocketCore.scala index fce7561ba..99fa877ea 100644 --- a/rocketv/src/RocketCore.scala +++ b/rocketv/src/RocketCore.scala @@ -11,8 +11,6 @@ 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 @@ -1132,7 +1130,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) - AssertProperty(BoolSequence(!htvalValidImem || io.imem.gpa.valid)) + assert(!htvalValidImem || io.imem.gpa.valid) val htvalValidDmem = wbException && tvalDmemAddr && io.dmem.s2_xcpt.gf.asUInt.orR && !io.dmem.s2_xcpt.pf.asUInt.orR @@ -1542,7 +1540,7 @@ class Rocket(val parameter: RocketParameter) io.dmem.replay_next || // long-latency load replaying (!longLatencyStall && (instructionBufferOut.valid || io.imem.resp.valid)) // instruction pending - AssertProperty(BoolSequence(!(exPcValid || memPcValid || wbPcValid) || clockEnable)) + assert(!(exPcValid || memPcValid || wbPcValid) || clockEnable) } // evaluate performance counters diff --git a/rocketv/src/TLB.scala b/rocketv/src/TLB.scala index c62507f83..3ea02f4f9 100644 --- a/rocketv/src/TLB.scala +++ b/rocketv/src/TLB.scala @@ -8,8 +8,6 @@ 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] @@ -621,7 +619,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 AssertProperty(BoolSequence(io.ptw.req.ready === true.B)) + // here should be io.ptw.req.fire, but assert(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) @@ -638,7 +636,7 @@ class TLB(val parameter: TLBParameter) // SFENCE processing logic. when(sfence) { - AssertProperty(BoolSequence(!io.sfence.bits.rs1 || (io.sfence.bits.addr >> pgIdxBits) === vpn)) + assert(!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 => diff --git a/t1/src/Lane.scala b/t1/src/Lane.scala index 5a251a52a..959fb4108 100644 --- a/t1/src/Lane.scala +++ b/t1/src/Lane.scala @@ -15,8 +15,6 @@ 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 @@ -835,7 +833,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) - AssertProperty(BoolSequence(queue.io.enq.ready || !port.enq.valid)) + assert(queue.io.enq.ready || !port.enq.valid) port.enqRelease := queue.io.deq.fire } diff --git a/t1rocketemu/src/TestBench.scala b/t1rocketemu/src/TestBench.scala index 137875bdf..58b506716 100644 --- a/t1rocketemu/src/TestBench.scala +++ b/t1rocketemu/src/TestBench.scala @@ -11,8 +11,6 @@ import chisel3.util.{HasExtModuleInline, Mux1H, PopCount, Queue, UIntToOH, Valid import org.chipsalliance.amba.axi4.bundle._ import org.chipsalliance.t1.t1rocketemu.dpi._ import org.chipsalliance.t1.tile.{T1RocketTile, T1RocketTileParameter} -import chisel3.ltl._ -import chisel3.ltl.Sequence._ class TestBench(generator: SerializableModuleGenerator[T1RocketTile, T1RocketTileParameter]) extends RawModule @@ -293,7 +291,7 @@ class TestBench(generator: SerializableModuleGenerator[T1RocketTile, T1RocketTil } when(scoreboardEnq(tag)) { scoreboard.valid := true.B - AssertProperty(BoolSequence(!scoreboard.valid)) + assert(!scoreboard.valid) scoreboard.bits := 0.U } }