Skip to content

Commit

Permalink
Add Config for TLB (#24)
Browse files Browse the repository at this point in the history 
* feat: add config for tlb

* feat: config tlb in RiscvCore

* feat: config in LoadStore

* feat: config in Checker and ConnectHelper

* refactor: simplify TLBLoadQueue in Checker

* refactor: simplify load/store queue in Checker

* test: support test with tlb config

* test: config tlb in CoreTester

* test: fix test in CheckerSpec

* test: test ConnectHelper with mem
  • Loading branch information
@liuyic00
liuyic00 authored Aug 28, 2024
1 parent 0deda76 commit 07df06c
Show file tree
Hide file tree
Showing 8 changed files with 238 additions and 260 deletions.
222 changes: 105 additions & 117 deletions src/main/scala/rvspeccore/checker/Checker.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,15 +54,15 @@ class QueueModuleTLB(implicit XLEN: Int) extends Module {
* Check pc of commited instruction and next value of all register. Although
* `pc` in the result port, but it won't be checked.
*/
class CheckerWithResult(checkMem: Boolean = true, enableReg: Boolean = false)(implicit config: RVConfig)
class CheckerWithResult(val checkMem: Boolean = true, enableReg: Boolean = false)(implicit config: RVConfig)
extends Checker {
val io = IO(new Bundle {
val instCommit = Input(InstCommit())
val result = Input(State())
val mem = if (checkMem) Some(Input(new MemIO)) else None
val event = Input(new EventSig())
val dtlbmem = if (checkMem) Some(Input(new TLBSig)) else None
val itlbmem = if (checkMem) Some(Input(new TLBSig)) else None
val mem = if (checkMem) Some(Input(new MemIO)) else None
val dtlbmem = if (checkMem && config.functions.tlb) Some(Input(new TLBSig)) else None
val itlbmem = if (checkMem && config.functions.tlb) Some(Input(new TLBSig)) else None
})
// TODO: io.result has .internal states now, consider use it or not

Expand All @@ -81,133 +81,119 @@ class CheckerWithResult(checkMem: Boolean = true, enableReg: Boolean = false)(im
specCore.io.inst := io.instCommit.inst

// initial another io.mem.get.Anotherread
for (i <- 0 until 6) {
specCore.io.tlb.Anotherread(i).data := DontCare
if (config.functions.tlb) {
for (i <- 0 until 6) {
specCore.io.tlb.get.Anotherread(i).data := DontCare
}
}

// assertions

if (checkMem) {
// printf("[specCore] Valid:%x PC: %x Inst: %x\n", specCore.io.valid, specCore.io.now.pc, specCore.io.inst)
// specCore.io.mem.read.data := { if (checkMem) io.mem.get.read.data else DontCare }
val TLBLoadQueue = Seq.fill(3)(Module(new QueueModuleTLB()))
val tlb_load_push = Wire(new StoreOrLoadInfoTLB)
// initial the queue
for (i <- 0 until 3) {
TLBLoadQueue(i).io.out.ready := false.B
TLBLoadQueue(i).io.in.valid := false.B
TLBLoadQueue(i).io.in.bits := 0.U.asTypeOf(new StoreOrLoadInfoTLB)
}
when(io.dtlbmem.get.read.valid) {
tlb_load_push.addr := io.dtlbmem.get.read.addr
tlb_load_push.data := io.dtlbmem.get.read.data
tlb_load_push.level := io.dtlbmem.get.read.level
assert(RegNext(TLBLoadQueue(0).io.in.valid, false.B) === false.B)
assert(RegNext(TLBLoadQueue(0).io.in.bits.addr, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(0).io.in.bits.data, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(0).io.in.bits.level, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(1).io.in.valid, false.B) === false.B)
assert(RegNext(TLBLoadQueue(1).io.in.bits.addr, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(1).io.in.bits.data, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(1).io.in.bits.level, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(2).io.in.valid, false.B) === false.B)
assert(RegNext(TLBLoadQueue(2).io.in.bits.addr, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(2).io.in.bits.data, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(2).io.in.bits.level, 0.U) === 0.U)

if (!config.functions.tlb) {
assert(io.mem.get.read.valid === specCore.io.mem.read.valid)
when(io.mem.get.read.valid || specCore.io.mem.read.valid) {
assert(io.mem.get.read.addr === specCore.io.mem.read.addr)
assert(io.mem.get.read.memWidth === specCore.io.mem.read.memWidth)
}
assert(io.mem.get.write.valid === specCore.io.mem.write.valid)
when(io.mem.get.write.valid || specCore.io.mem.write.valid) {
assert(io.mem.get.write.addr === specCore.io.mem.write.addr)
assert(io.mem.get.write.data === specCore.io.mem.write.data)
assert(io.mem.get.write.memWidth === specCore.io.mem.write.memWidth)
}
specCore.io.mem.read.data := io.mem.get.read.data
} else {
// printf("[specCore] Valid:%x PC: %x Inst: %x\n", specCore.io.valid, specCore.io.now.pc, specCore.io.inst)
// specCore.io.mem.read.data := { if (checkMem) io.mem.get.read.data else DontCare }
val TLBLoadQueue = Seq.fill(3)(Module(new QueueModuleTLB()))
// initial the queue
for (i <- 0 until 3) {
TLBLoadQueue(i).io.in.valid := false.B
TLBLoadQueue(i).io.in.bits := 0.U.asTypeOf(new StoreOrLoadInfoTLB)
TLBLoadQueue(i).io.out.ready := false.B
TLBLoadQueue(i).io.in.valid := false.B
TLBLoadQueue(i).io.in.bits := 0.U.asTypeOf(new StoreOrLoadInfoTLB)
}
switch(io.dtlbmem.get.read.level) {
is(0.U) {
TLBLoadQueue(0).io.in.valid := true.B
TLBLoadQueue(0).io.in.bits := tlb_load_push
when(io.dtlbmem.get.read.valid) {
assert(RegNext(TLBLoadQueue(0).io.in.valid, false.B) === false.B)
assert(RegNext(TLBLoadQueue(0).io.in.bits.addr, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(0).io.in.bits.data, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(0).io.in.bits.level, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(1).io.in.valid, false.B) === false.B)
assert(RegNext(TLBLoadQueue(1).io.in.bits.addr, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(1).io.in.bits.data, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(1).io.in.bits.level, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(2).io.in.valid, false.B) === false.B)
assert(RegNext(TLBLoadQueue(2).io.in.bits.addr, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(2).io.in.bits.data, 0.U) === 0.U)
assert(RegNext(TLBLoadQueue(2).io.in.bits.level, 0.U) === 0.U)

for (i <- 0 until 3) {
when(io.dtlbmem.get.read.level === i.U) {
TLBLoadQueue(i).io.in.valid := true.B
TLBLoadQueue(i).io.in.bits.addr := io.dtlbmem.get.read.addr
TLBLoadQueue(i).io.in.bits.data := io.dtlbmem.get.read.data
TLBLoadQueue(i).io.in.bits.level := io.dtlbmem.get.read.level
}
}
is(1.U) {
TLBLoadQueue(1).io.in.valid := true.B
TLBLoadQueue(1).io.in.bits := tlb_load_push
}
for (i <- 0 until 3) {
when(specCore.io.tlb.get.Anotherread(i).valid) {
TLBLoadQueue(2 - i).io.out.ready := true.B
// printf("Load out Queue.... valid: %x %x %x %x\n", LoadQueue.io.out.valid, LoadQueue.io.out.bits.addr, LoadQueue.io.out.bits.data, LoadQueue.io.out.bits.memWidth)
specCore.io.tlb.get.Anotherread(i).data := {
if (checkMem) TLBLoadQueue(2 - i).io.out.bits.data else DontCare
}
// TODO: 第Level 1 assert is inconsistent nutshell and the condition need to modify.
// assert(TLBLoadQueue(i).io.out.bits.addr === specCore.io.mem.read.addr)
}
is(2.U) {
TLBLoadQueue(2).io.in.valid := true.B
TLBLoadQueue(2).io.in.bits := tlb_load_push
when(regDelay(specCore.io.tlb.get.Anotherread(i).valid)) {
assert(regDelay(TLBLoadQueue(2 - i).io.out.bits.addr) === regDelay(specCore.io.tlb.get.Anotherread(i).addr))
}
is(3.U) {}
}
}.otherwise {
for (i <- 0 until 3) {
TLBLoadQueue(i).io.in.valid := false.B
tlb_load_push := 0.U.asTypeOf(new StoreOrLoadInfoTLB)
TLBLoadQueue(i).io.in.bits := tlb_load_push
val LoadQueue = Module(new QueueModule)
val StoreQueue = Module(new QueueModule)
// LOAD
when(io.mem.get.read.valid) {
LoadQueue.io.in.valid := true.B
LoadQueue.io.in.bits.addr := io.mem.get.read.addr
LoadQueue.io.in.bits.data := io.mem.get.read.data
LoadQueue.io.in.bits.memWidth := io.mem.get.read.memWidth
// printf("Load into Queue.... valid: %x %x %x %x\n", LoadQueue.io.in.valid, load_push.addr, load_push.data, load_push.memWidth)
}.otherwise {
LoadQueue.io.in.valid := false.B
LoadQueue.io.in.bits := 0.U.asTypeOf(new StoreOrLoadInfo)
}
}
for (i <- 0 until 3) {
when(specCore.io.tlb.Anotherread(i).valid) {
TLBLoadQueue(2 - i).io.out.ready := true.B
when(specCore.io.mem.read.valid) {
LoadQueue.io.out.ready := true.B
// printf("Load out Queue.... valid: %x %x %x %x\n", LoadQueue.io.out.valid, LoadQueue.io.out.bits.addr, LoadQueue.io.out.bits.data, LoadQueue.io.out.bits.memWidth)
specCore.io.tlb.Anotherread(i).data := { if (checkMem) TLBLoadQueue(2 - i).io.out.bits.data else DontCare }
// TODO: 第Level 1 assert is inconsistent nutshell and the condition need to modify.
// assert(TLBLoadQueue(i).io.out.bits.addr === specCore.io.mem.read.addr)
specCore.io.mem.read.data := LoadQueue.io.out.bits.data
assert(LoadQueue.io.out.bits.addr === specCore.io.mem.read.addr)
assert(LoadQueue.io.out.bits.memWidth === specCore.io.mem.read.memWidth)
}.otherwise {
TLBLoadQueue(2 - i).io.out.ready := false.B
}
when(regDelay(specCore.io.tlb.Anotherread(i).valid)) {
assert(regDelay(TLBLoadQueue(2 - i).io.out.bits.addr) === regDelay(specCore.io.tlb.Anotherread(i).addr))
LoadQueue.io.out.ready := false.B
specCore.io.mem.read.data := 0.U
}
}
val LoadQueue = Module(new QueueModule)
val StoreQueue = Module(new QueueModule)
LoadQueue.io.out.ready := false.B
StoreQueue.io.out.ready := false.B
// Load Queue
val load_push = Wire(new StoreOrLoadInfo)
val store_push = Wire(new StoreOrLoadInfo)
// LOAD
when(io.mem.get.read.valid) {
LoadQueue.io.in.valid := true.B
load_push.addr := io.mem.get.read.addr
load_push.data := io.mem.get.read.data
load_push.memWidth := io.mem.get.read.memWidth
LoadQueue.io.in.bits := load_push
// printf("Load into Queue.... valid: %x %x %x %x\n", LoadQueue.io.in.valid, load_push.addr, load_push.data, load_push.memWidth)
}.otherwise {
LoadQueue.io.in.valid := false.B
load_push.addr := 0.U
load_push.data := 0.U
load_push.memWidth := 0.U
LoadQueue.io.in.bits := load_push
}
when(specCore.io.mem.read.valid) {
LoadQueue.io.out.ready := true.B
// printf("Load out Queue.... valid: %x %x %x %x\n", LoadQueue.io.out.valid, LoadQueue.io.out.bits.addr, LoadQueue.io.out.bits.data, LoadQueue.io.out.bits.memWidth)
specCore.io.mem.read.data := { if (checkMem) LoadQueue.io.out.bits.data else DontCare }
assert(LoadQueue.io.out.bits.addr === specCore.io.mem.read.addr)
assert(LoadQueue.io.out.bits.memWidth === specCore.io.mem.read.memWidth)
}.otherwise {
specCore.io.mem.read.data := 0.U
}

// Store
when(io.mem.get.write.valid) {
StoreQueue.io.in.valid := true.B
store_push.addr := io.mem.get.write.addr
store_push.data := io.mem.get.write.data
store_push.memWidth := io.mem.get.write.memWidth
StoreQueue.io.in.bits := store_push
// printf("Store into Queue.... valid: %x %x %x %x\n", StoreQueue.io.in.valid, store_push.addr, store_push.data, store_push.memWidth)
}.otherwise {
StoreQueue.io.in.valid := false.B
store_push.addr := 0.U
store_push.data := 0.U
store_push.memWidth := 0.U
StoreQueue.io.in.bits := store_push
}
when(specCore.io.mem.write.valid) {
StoreQueue.io.out.ready := true.B
// printf("Store out Queue.... valid: %x %x %x %x\n", StoreQueue.io.out.valid, StoreQueue.io.out.bits.addr, StoreQueue.io.out.bits.data, StoreQueue.io.out.bits.memWidth)
assert(StoreQueue.io.out.bits.addr === specCore.io.mem.write.addr)
assert(StoreQueue.io.out.bits.data === specCore.io.mem.write.data)
assert(StoreQueue.io.out.bits.memWidth === specCore.io.mem.write.memWidth)
// Store
when(io.mem.get.write.valid) {
StoreQueue.io.in.valid := true.B
StoreQueue.io.in.bits.addr := io.mem.get.write.addr
StoreQueue.io.in.bits.data := io.mem.get.write.data
StoreQueue.io.in.bits.memWidth := io.mem.get.write.memWidth
// printf("Store into Queue.... valid: %x %x %x %x\n", StoreQueue.io.in.valid, store_push.addr, store_push.data, store_push.memWidth)
}.otherwise {
StoreQueue.io.in.valid := false.B
StoreQueue.io.in.bits := 0.U.asTypeOf(new StoreOrLoadInfo)
}
when(specCore.io.mem.write.valid) {
StoreQueue.io.out.ready := true.B
// printf("Store out Queue.... valid: %x %x %x %x\n", StoreQueue.io.out.valid, StoreQueue.io.out.bits.addr, StoreQueue.io.out.bits.data, StoreQueue.io.out.bits.memWidth)
assert(StoreQueue.io.out.bits.addr === specCore.io.mem.write.addr)
assert(StoreQueue.io.out.bits.data === specCore.io.mem.write.data)
assert(StoreQueue.io.out.bits.memWidth === specCore.io.mem.write.memWidth)
}.otherwise {
StoreQueue.io.out.ready := false.B
}
}
} else {
specCore.io.mem.read.data := DontCare
Expand Down Expand Up @@ -272,8 +258,10 @@ class CheckerWithWB(checkMem: Boolean = true)(implicit config: RVConfig) extends
specCore.io.mem.read.data := { if (checkMem) io.mem.get.read.data else DontCare }

// initial another io.mem.get.Anotherread
for (i <- 0 until 6) {
specCore.io.tlb.Anotherread(i).data := DontCare
if (config.functions.tlb) {
for (i <- 0 until 6) {
specCore.io.tlb.get.Anotherread(i).data := DontCare
}
}
val specCoreWBValid = WireInit(false.B)
val specCoreWBDest = WireInit(0.U(5.W))
Expand Down
59 changes: 22 additions & 37 deletions src/main/scala/rvspeccore/checker/ConnectHelper.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ import chisel3.util.experimental.BoringUtils
import rvspeccore.core.RVConfig
import rvspeccore.core.spec.instset.csr.CSR
import rvspeccore.core.spec.instset.csr.EventSig
import rvspeccore.core.tool.TLBMemInfo
import rvspeccore.core.tool.TLBSig

abstract class ConnectHelper {}

/** Connect RegFile to io.result.reg by BoringUtils
Expand All @@ -35,25 +35,8 @@ object ConnectCheckerResult extends ConnectHelper {
val write = new MemOneSig
}
def makeTLBSource(isDTLB: Boolean)(implicit XLEN: Int): TLBSig = {
val tlbmem = Wire(new TLBSig())
tlbmem.read.valid := false.B
tlbmem.read.addr := 0.U
tlbmem.read.data := 0.U
tlbmem.read.memWidth := 0.U
tlbmem.read.access := false.B
tlbmem.read.level := 0.U
tlbmem.write.valid := false.B
tlbmem.write.addr := 0.U
tlbmem.write.data := 0.U
tlbmem.write.memWidth := 0.U
tlbmem.write.access := false.B
tlbmem.write.level := 0.U

if (isDTLB) {
BoringUtils.addSource(tlbmem, uniqueIdDTLB)
} else {
BoringUtils.addSource(tlbmem, uniqueIdITLB)
}
val tlbmem = WireInit(0.U.asTypeOf(new TLBSig))
BoringUtils.addSource(tlbmem, if (isDTLB) uniqueIdDTLB else uniqueIdITLB)
tlbmem
}
def makeMemSource()(implicit XLEN: Int) = {
Expand Down Expand Up @@ -109,24 +92,26 @@ object ConnectCheckerResult extends ConnectHelper {

checker.io.result.internal := DontCare

if (checker.io.mem != None) {
val mem = Wire(new MemSig)
val dtlbmem = Wire(new TLBSig)
val itlbmem = Wire(new TLBSig)
mem := DontCare
dtlbmem := DontCare
itlbmem := DontCare
if (checker.checkMem) {
val mem = Wire(new MemSig)
mem := DontCare
BoringUtils.addSink(mem, uniqueIdMem)
BoringUtils.addSink(dtlbmem, uniqueIdDTLB)
BoringUtils.addSink(itlbmem, uniqueIdITLB)
checker.io.dtlbmem.get := dtlbmem
checker.io.itlbmem.get := itlbmem
checker.io.mem.get := regNextDelay(mem, memDelay)
// expose the signal below
// assert(RegNext(checker.io.dtlbmem.get.read.valid, false.B) === false.B)
// assert(RegNext(dtlbmem.read.valid, false.B) === false.B)
// assert(RegNext(dtlbmem.read.addr, 0.U) === 0.U)
// assert(RegNext(dtlbmem.read.data, 0.U) === 0.U)
checker.io.mem.get := regNextDelay(mem, memDelay)
if (config.functions.tlb) {
val dtlbmem = Wire(new TLBSig)
val itlbmem = Wire(new TLBSig)
dtlbmem := DontCare
itlbmem := DontCare
BoringUtils.addSink(dtlbmem, uniqueIdDTLB)
BoringUtils.addSink(itlbmem, uniqueIdITLB)
checker.io.dtlbmem.get := dtlbmem
checker.io.itlbmem.get := itlbmem
// expose the signal below
// assert(RegNext(checker.io.dtlbmem.get.read.valid, false.B) === false.B)
// assert(RegNext(dtlbmem.read.valid, false.B) === false.B)
// assert(RegNext(dtlbmem.read.addr, 0.U) === 0.U)
// assert(RegNext(dtlbmem.read.data, 0.U) === 0.U)
}
}
// csr
val csr = Wire(CSR())
Expand Down
1 change: 1 addition & 0 deletions src/main/scala/rvspeccore/core/RVConfig.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ case class RVConfig(configs: (String, Any)*) {
object functions {
protected val raw = cfgs.getOrElse("functions", Seq[String]()).asInstanceOf[Seq[String]]
val privileged: Boolean = raw.contains("Privileged")
val tlb: Boolean = raw.contains("TLB")
}

// Formal
Expand Down
Loading

0 comments on commit 07df06c

Please sign in to comment.