From 29c70501f2f65b5315d4f28741cb40409acc529b Mon Sep 17 00:00:00 2001 From: Richard Xia Date: Tue, 28 Nov 2017 19:49:01 -0800 Subject: [PATCH 1/2] Add cover properties for exceptions in the core. --- src/main/scala/rocket/RocketCore.scala | 36 ++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/src/main/scala/rocket/RocketCore.scala b/src/main/scala/rocket/RocketCore.scala index a7f3d175..104e4d37 100644 --- a/src/main/scala/rocket/RocketCore.scala +++ b/src/main/scala/rocket/RocketCore.scala @@ -9,6 +9,7 @@ import chisel3.core.withReset import freechips.rocketchip.config.Parameters import freechips.rocketchip.tile._ import freechips.rocketchip.util._ +import freechips.rocketchip.util.property._ import scala.collection.immutable.ListMap import scala.collection.mutable.ArrayBuffer @@ -239,6 +240,15 @@ class Rocket(implicit p: Parameters) extends CoreModule()(p) (id_xcpt1.ae.inst, UInt(Causes.fetch_access)), (id_illegal_insn, UInt(Causes.illegal_instruction)))) + val idCoverCauses = List( + (CSR.debugTriggerCause, "DEBUG_TRIGGER"), + (Causes.breakpoint, "BREAKPOINT"), + (Causes.fetch_page_fault, "FETCH_PAGE_FAULT"), + (Causes.fetch_access, "FETCH_ACCESS"), + (Causes.illegal_instruction, "ILLEGAL_INSTRUCTION") + ) + coverExceptions(id_xcpt, id_cause, "DECODE", idCoverCauses) + val dcache_bypass_data = if (fastLoadByte) io.dmem.resp.bits.data else if (fastLoadWord) io.dmem.resp.bits.data_word_bypass @@ -357,6 +367,9 @@ class Rocket(implicit p: Parameters) extends CoreModule()(p) val (ex_xcpt, ex_cause) = checkExceptions(List( (ex_reg_xcpt_interrupt || ex_reg_xcpt, ex_reg_cause))) + val exCoverCauses = idCoverCauses + coverExceptions(ex_xcpt, ex_cause, "EXECUTE", exCoverCauses) + // memory stage val mem_pc_valid = mem_reg_valid || mem_reg_replay || mem_reg_xcpt_interrupt val mem_br_target = mem_reg_pc.asSInt + @@ -423,6 +436,13 @@ class Rocket(implicit p: Parameters) extends CoreModule()(p) (mem_reg_xcpt_interrupt || mem_reg_xcpt, mem_reg_cause), (mem_reg_valid && mem_new_xcpt, mem_new_cause))) + val memCoverCauses = (exCoverCauses ++ List( + (CSR.debugTriggerCause, "DEBUG_TRIGGER"), + (Causes.breakpoint, "BREKPOINT"), + (Causes.misaligned_fetch, "MISALIGNED_FETCH") + )).distinct + coverExceptions(mem_xcpt, mem_cause, "MEMORY", memCoverCauses) + val dcache_kill_mem = mem_reg_valid && mem_ctrl.wxd && io.dmem.replay_next // structural hazard on writeback port val fpu_kill_mem = mem_reg_valid && mem_ctrl.fp && io.fpu.nack_mem val replay_mem = dcache_kill_mem || mem_reg_replay || fpu_kill_mem @@ -458,6 +478,16 @@ class Rocket(implicit p: Parameters) extends CoreModule()(p) (wb_reg_valid && wb_ctrl.mem && io.dmem.s2_xcpt.ae.ld, UInt(Causes.load_access)) )) + val wbCoverCauses = List( + (Causes.misaligned_store, "MISALIGNED_STORE"), + (Causes.misaligned_load, "MISALIGNED_LOAD"), + (Causes.store_page_fault, "STORE_PAGE_FAULT"), + (Causes.load_page_fault, "LOAD_PAGE_FAULT"), + (Causes.store_access, "STORE_ACCESS"), + (Causes.load_access, "LOAD_ACCESS") + ) + coverExceptions(wb_xcpt, wb_cause, "WRITEBACK", wbCoverCauses) + val wb_wxd = wb_reg_valid && wb_ctrl.wxd val wb_set_sboard = wb_ctrl.div || wb_dcache_miss || wb_ctrl.rocc val replay_wb_common = io.dmem.s2_nack || wb_reg_replay @@ -702,6 +732,12 @@ class Rocket(implicit p: Parameters) extends CoreModule()(p) def checkExceptions(x: Seq[(Bool, UInt)]) = (x.map(_._1).reduce(_||_), PriorityMux(x)) + def coverExceptions(exceptionValid: Bool, cause: UInt, labelPrefix: String, coverCausesLabels: Seq[(Int, String)]): Unit = { + for ((coverCause, label) <- coverCausesLabels) { + cover(exceptionValid && (cause === UInt(coverCause)), s"${labelPrefix}_${label}") + } + } + def checkHazards(targets: Seq[(Bool, UInt)], cond: UInt => Bool) = targets.map(h => h._1 && cond(h._2)).reduce(_||_) From 4bd9c477ea1467e43d5943fd2b5323bbb7ddb14c Mon Sep 17 00:00:00 2001 From: Richard Xia Date: Thu, 30 Nov 2017 11:56:04 -0800 Subject: [PATCH 2/2] Add cover properties for ECALL exceptions. --- src/main/scala/rocket/CSR.scala | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/main/scala/rocket/CSR.scala b/src/main/scala/rocket/CSR.scala index 9ff2b3a9..d9fb933f 100644 --- a/src/main/scala/rocket/CSR.scala +++ b/src/main/scala/rocket/CSR.scala @@ -8,6 +8,7 @@ import Chisel.ImplicitConversions._ import freechips.rocketchip.config.Parameters import freechips.rocketchip.tile._ import freechips.rocketchip.util._ +import freechips.rocketchip.util.property._ import scala.collection.mutable.LinkedHashMap import Instructions._ @@ -532,6 +533,9 @@ class CSRFile(perfEventSets: EventSets = new EventSets(Seq()))(implicit p: Param Causes.load_page_fault, Causes.store_page_fault, Causes.fetch_page_fault) val badaddr_value = Mux(write_badaddr, io.badaddr, 0.U) + val noCause :: mCause :: hCause :: sCause :: uCause :: Nil = Enum(5) + val xcause_dest = Wire(init = noCause) + when (exception) { when (trapToDebug) { when (!reg_debug) { @@ -544,6 +548,7 @@ class CSRFile(perfEventSets: EventSets = new EventSets(Seq()))(implicit p: Param }.elsewhen (delegate) { reg_sepc := formEPC(epc) reg_scause := cause + xcause_dest := sCause reg_sbadaddr := badaddr_value reg_mstatus.spie := reg_mstatus.sie reg_mstatus.spp := reg_mstatus.prv @@ -552,6 +557,7 @@ class CSRFile(perfEventSets: EventSets = new EventSets(Seq()))(implicit p: Param }.otherwise { reg_mepc := formEPC(epc) reg_mcause := cause + xcause_dest := mCause reg_mbadaddr := badaddr_value reg_mstatus.mpie := reg_mstatus.mie reg_mstatus.mpp := trimPrivilege(reg_mstatus.prv) @@ -560,6 +566,22 @@ class CSRFile(perfEventSets: EventSets = new EventSets(Seq()))(implicit p: Param } } + for ( + (cover_reg, cover_reg_label) <- List( + (mCause, "MCAUSE"), + (sCause, "SCAUSE") + ); + (cover_cause_code, cover_cause_label) <- List( + (Causes.user_ecall, "ECALL_USER"), + (Causes.supervisor_ecall, "ECALL_SUPERVISOR"), + (Causes.hypervisor_ecall, "ECALL_HYPERVISOR"), + (Causes.machine_ecall, "ECALL_MACHINE") + ) + ) { + cover((xcause_dest === cover_reg) && (cause === UInt(cover_cause_code)), + s"${cover_reg_label}_${cover_cause_label}") + } + when (insn_ret) { when (Bool(usingVM) && !io.rw.addr(9)) { reg_mstatus.sie := reg_mstatus.spie