Skip to content

Commit

Permalink
Merge pull request #2 from SeddonShen/seddon
Browse files Browse the repository at this point in the history 
Support formal verification for privileged instructions
  • Loading branch information
@liuyic00
liuyic00 authored Nov 3, 2023
2 parents d73915d + ca4dae2 commit bb9ff59
Show file tree
Hide file tree
Showing 9 changed files with 158 additions and 23 deletions.
38 changes: 38 additions & 0 deletions .github/workflows/formal.yml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
name: Formal Btormc

on: [push, pull_request]

jobs:
ci:
name: ci
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Cleanup
run: sed -i "s/%NAME%/test/g" build.sc
- name: Setup Scala
uses: olafurpg/setup-scala@v10
with:
java-version: [email protected]
- name: Submodule
run: git submodule update --init
- name: Setup BtorMC
uses: SeddonShen/[email protected]
- name: Setup Mill
uses: jodersky/[email protected]
with:
mill-version: 0.9.7
- name: Cache Scala
uses: coursier/cache-action@v5
- name: mill Test
run: mill _.test
# - name: Single BtorMC Run 15 Steps
# if: always()
# run: btormc ./test_run_dir/NutCoreFormal_should_pass/NutCore.btor -kmax 15 --trace-gen-full --btor-stats > ./test_run_dir/NutCoreFormal_should_pass/15step.txt
- name: Archive production artifacts
if: always()
uses: actions/upload-artifact@v3
with:
name: Btormc Output Files
path: test_run_dir/NutCoreFormal_should_pass
2 changes: 1 addition & 1 deletion build.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ trait HasChisel3 extends ScalaModule {
}
override def ivyDeps = Agg(
ivy"edu.berkeley.cs::chisel3:3.5.4",
ivy"cn.ac.ios.tis::riscvspeccore:0.1.0"
ivy"cn.ac.ios.tis::riscvspeccore:1.0-SNAPSHOT"
)
override def scalacPluginIvyDeps = Agg(
ivy"edu.berkeley.cs:::chisel3-plugin:3.5.4",
Expand Down
4 changes: 3 additions & 1 deletion src/main/scala/nutcore/NutCore.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import bus.simplebus._
import bus.axi4._
import utils._
import top.Settings
import rvspeccore.core.RV64Config

trait HasNutCoreParameter {
// General Parameter for NutShell
Expand Down Expand Up @@ -69,7 +70,8 @@ case class NutCoreConfig (
Formal: Boolean = Settings.get("Formal"),
EnableILA: Boolean = Settings.get("EnableILA"),
EnableDebug: Boolean = Settings.get("EnableDebug"),
EnhancedLog: Boolean = true
EnhancedLog: Boolean = true ,
FormalConfig: RV64Config = RV64Config("MCS")
)
// Enable EnhancedLog will slow down simulation,
// but make it possible to control debug log using emu parameter
Expand Down
61 changes: 56 additions & 5 deletions src/main/scala/nutcore/backend/fu/CSR.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,7 @@ class CSR(implicit val p: NutCoreConfig) extends NutCoreModule with HasCSRConst{
val mcounteren = RegInit(UInt(XLEN.W), 0.U)
val mcause = RegInit(UInt(XLEN.W), 0.U)
val mtval = RegInit(UInt(XLEN.W), 0.U)
val mepc = Reg(UInt(XLEN.W))
val mepc = RegInit(UInt(XLEN.W), 0.U)

val mie = RegInit(0.U(XLEN.W))
val mipWire = WireInit(0.U.asTypeOf(new Interrupt))
Expand All @@ -276,6 +276,7 @@ class CSR(implicit val p: NutCoreConfig) extends NutCoreModule with HasCSRConst{
val mimpid = RegInit(UInt(XLEN.W), 0.U) // provides a unique encoding of the version of the processor implementation
val mhartid = RegInit(UInt(XLEN.W), 0.U) // the hardware thread running the code
val mstatus = RegInit(UInt(XLEN.W), "h00001800".U)
// val mstatus = RegInit(UInt(XLEN.W), "h000E0800".U)
// val mstatus = RegInit(UInt(XLEN.W), "h8000c0100".U)
// mstatus Value Table
// | sd |
Expand Down Expand Up @@ -330,13 +331,16 @@ class CSR(implicit val p: NutCoreConfig) extends NutCoreModule with HasCSRConst{
// Sstatus Read Mask = (SSTATUS_WMASK | (0xf << 13) | (1ull << 63) | (3ull << 32))
val stvec = RegInit(UInt(XLEN.W), 0.U)
// val sie = RegInit(0.U(XLEN.W))
val sieMask = "h222".U & mideleg
val sipMask = "h222".U & mideleg
// val satp = RegInit(UInt(XLEN.W), "h8000000000087fbe".U)
// FIXME: need to fix this important bugs
// val sieMask = "h222".U & mideleg
// val sipMask = "h222".U & mideleg
val sieMask = "h222".U
val sipMask = "h222".U
// val satp = RegInit(UInt(XLEN.W), "h8000000000080002".U)
val satp = RegInit(UInt(XLEN.W), 0.U)
val sepc = RegInit(UInt(XLEN.W), 0.U)
val scause = RegInit(UInt(XLEN.W), 0.U)
val stval = Reg(UInt(XLEN.W))
val stval = RegInit(UInt(XLEN.W), 0.U)
val sscratch = RegInit(UInt(XLEN.W), 0.U)
val scounteren = RegInit(UInt(XLEN.W), 0.U)

Expand Down Expand Up @@ -920,6 +924,53 @@ class CSR(implicit val p: NutCoreConfig) extends NutCoreModule with HasCSRConst{
difftestArchEvent.io.exceptionInst := RegNext(RegNext(io.cfIn.instr))

} else {
if (p.Formal) {
val resultCSRWire = rvspeccore.checker.ConnectCheckerResult.makeCSRSource()(64, p.FormalConfig)
val resultEventWire = rvspeccore.checker.ConnectCheckerResult.makeEventSource()(64, p.FormalConfig)
resultEventWire.valid := RegNext(RegNext((raiseIntr && io.instrValid) || (raiseException && io.instrValid), 0.U), 0.U)
resultEventWire.intrNO := RegNext(RegNext(Mux(raiseIntr && io.instrValid && valid, intrNO, 0.U)))
resultEventWire.cause := RegNext(RegNext(Mux(raiseException && io.instrValid, exceptionNO, 0.U)))
resultEventWire.exceptionPC := RegNext(RegNext(SignExt(io.cfIn.pc, XLEN)))
resultEventWire.exceptionInst := RegNext(RegNext(io.cfIn.instr))

resultCSRWire.misa := RegNext(misa)
resultCSRWire.mvendorid := RegNext(mvendorid)
resultCSRWire.marchid := RegNext(marchid)
resultCSRWire.mimpid := RegNext(mimpid)
resultCSRWire.mhartid := RegNext(mhartid)
resultCSRWire.mstatus := RegNext(mstatus)
// resultCSRWire.mstatush := 0.U //FIXME: how to deal with unimplemented CSRs
resultCSRWire.mscratch := RegNext(mscratch)
resultCSRWire.mtvec := RegNext(mtvec)
resultCSRWire.mcounteren:= RegNext(mcounteren)
resultCSRWire.medeleg := RegNext(medeleg)
resultCSRWire.mideleg := RegNext(mideleg)
resultCSRWire.mip := RegNext(mipReg)
resultCSRWire.mie := RegNext(mie)
resultCSRWire.mepc := RegNext(mepc)
resultCSRWire.mcause := RegNext(mcause)
resultCSRWire.mtval := RegNext(mtval)
resultCSRWire.scounteren:= RegNext(scounteren)
resultCSRWire.scause := RegNext(scause)
resultCSRWire.stvec := RegNext(stvec)
resultCSRWire.sepc := RegNext(sepc)
resultCSRWire.stval := RegNext(stval)
// not need to compare, because compare signal means mstatus equals to sstatus
// resultCSRWire.sstatus
// resultCSRWire.sie
// resultCSRWire.sip
resultCSRWire.sscratch := RegNext(sscratch)
resultCSRWire.satp := RegNext(satp)
resultCSRWire.pmpcfg0 := RegNext(pmpcfg0)
resultCSRWire.pmpcfg1 := RegNext(pmpcfg1)
resultCSRWire.pmpcfg2 := RegNext(pmpcfg2)
resultCSRWire.pmpcfg3 := RegNext(pmpcfg3)
resultCSRWire.pmpaddr0 := RegNext(pmpaddr0)
resultCSRWire.pmpaddr1 := RegNext(pmpaddr1)
resultCSRWire.pmpaddr2 := RegNext(pmpaddr2)
resultCSRWire.pmpaddr3 := RegNext(pmpaddr3)
// resultCSRWire.cycle := 0.U //FIXME: how to deal with unimplemented CSRs
}
if (!p.FPGAPlatform) {
BoringUtils.addSource(readWithScala(perfCntList("Mcycle")._1), "simCycleCnt")
BoringUtils.addSource(readWithScala(perfCntList("Minstret")._1), "simInstrCnt")
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/nutcore/backend/fu/UnpipelinedLSU.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -430,8 +430,8 @@ class LSExecUnit extends NutCoreModule {
io.storeAddrMisaligned := valid && (isStore || isAMO) && !addrAligned

// Formal assume
assume(io.loadAddrMisaligned === false.B)
assume(io.storeAddrMisaligned === false.B)
// assume(io.loadAddrMisaligned === false.B)
// assume(io.storeAddrMisaligned === false.B)

Debug(io.loadAddrMisaligned || io.storeAddrMisaligned, "misaligned addr detected\n")

Expand Down
10 changes: 5 additions & 5 deletions src/main/scala/nutcore/backend/seq/WBU.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,17 +101,17 @@ class WBU(implicit val p: NutCoreConfig) extends NutCoreModule{
BoringUtils.addSource(io.wb.rfData, "ilaWBUrfData")
}
if (p.Formal) {
val checker = Module(new CheckerWithResult(checkMem = true)(RV64Config("")))
val checker = Module(new CheckerWithResult(checkMem = true)(p.FormalConfig))

checker.io.instCommit.valid := RegNext(io.in.valid, false.B)
checker.io.instCommit.inst := RegNext(io.in.bits.decode.cf.instr)
checker.io.instCommit.pc := RegNext(SignExt(io.in.bits.decode.cf.pc, AddrBits))

ConnectCheckerResult.setChecker(checker, 2)(XLEN)
ConnectCheckerResult.setChecker(checker)(XLEN, p.FormalConfig)

when (RegNext(io.in.valid && rvspeccore.checker.RVI.loadStore(io.in.bits.decode.cf.instr)(64), false.B)) {
assert(false.B)
}
// when (RegNext(io.in.valid && rvspeccore.checker.RVI.loadStore(io.in.bits.decode.cf.instr)(64), false.B)) {
// assert(false.B)
// }
}
}
}
27 changes: 23 additions & 4 deletions src/main/scala/nutcore/frontend/Frontend.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import bus.simplebus._
import chisel3.experimental.IO

import rvspeccore.checker._

import rvspeccore.core.spec.instset.csr.{CSR => SpecCSR}
class FrontendIO(implicit val p: NutCoreConfig) extends Bundle with HasNutCoreConst {
val imem = new SimpleBusUC(userBits = ICacheUserBundleWidth, addrBits = VAddrBits)
val out = Vec(2, Decoupled(new DecodeIO))
Expand Down Expand Up @@ -117,15 +117,34 @@ class Frontend_inorder(implicit val p: NutCoreConfig) extends NutCoreModule with
io.bpFlush <> ifu.io.bpFlush
io.ipf <> ifu.io.ipf
io.imem <> ifu.io.imem

def hasCSR(addr: UInt) :Bool = {
val speccsr = new SpecCSR()(64, p.FormalConfig)
MuxLookup(addr, false.B, speccsr.table.map { x => x.info.addr -> true.B })
}
if (p.Formal) {
// here is the earliest place to assume the inst
// before this, the inst may not been assemble/splite to 32bit
val tmpInst = ibf.io.out.bits.instr(31, 0)
implicit val checker_xlen = 64

when (ibf.io.out.valid){
assume(RVI.regImm(tmpInst) || RVI.loadStore(tmpInst))
// Some assume example
// assume(RVI.regImm(tmpInst) || RVI.loadStore(tmpInst))
// assume(RVI.loadStore(tmpInst))
// assume(RVI.loadStore(tmpInst))
assume(
(hasCSR(tmpInst(31,20)) && (RVZicsr.reg(tmpInst) || RVZicsr.imm(tmpInst)))
||
( RVI.regImm(tmpInst) || RVI.loadStore(tmpInst) || RVI.other(tmpInst))
||
(RVPriviledged.trap_return(tmpInst))
// (RVPriviledged.trap_return(tmpInst))
)
// assume(
// (hasCSR(tmpInst(31,20)) && (RVZicsr.reg(tmpInst) || RVZicsr.imm(tmpInst)))
// ||
// SV39Translate.regImm(tmpInst)
// )
}
}

Expand Down
32 changes: 28 additions & 4 deletions src/main/scala/nutcore/mem/EmbeddedTLB.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import bus.axi4._
import chisel3.experimental.IO
import utils._
import top.Settings

import rvspeccore.core.tool.TLBSig
trait HasTLBIO extends HasNutCoreParameter with HasTlbConst with HasCSRConst {
class TLBIO extends Bundle {
val in = Flipped(new SimpleBusUC(userBits = userBits, addrBits = VAddrBits))
Expand Down Expand Up @@ -235,7 +235,14 @@ class EmbeddedTLBExec(implicit val tlbConfig: TLBConfig) extends TlbModule{
if (tlbname == "dtlb") {
BoringUtils.addSink(isAMO, "ISAMO")
}

// val resultTLBWire = Wire(new TLBSig()(64))
// if (tlbname == "itlb"){
// resultTLBWire := rvspeccore.checker.ConnectCheckerResult.makeTLBSource(false)(64)
// }
// if (tlbname == "dtlb"){
// resultTLBWire := rvspeccore.checker.ConnectCheckerResult.makeTLBSource(true)(64)
// }
val resultTLBWire = rvspeccore.checker.ConnectCheckerResult.makeTLBSource(if(tlbname == "itlb") false else true)(64)
io.pf.loadPF := RegNext(loadPF, init =false.B)
io.pf.storePF := RegNext(storePF, init = false.B)

Expand Down Expand Up @@ -267,7 +274,11 @@ class EmbeddedTLBExec(implicit val tlbConfig: TLBConfig) extends TlbModule{
when (io.out.fire && needFlush) { needFlush := false.B}

val missIPF = RegInit(false.B)

when(RegNext(io.mem.resp.fire, false.B)){
assert(RegNext(resultTLBWire.read.valid, false.B) === true.B)
assert(RegNext(resultTLBWire.read.addr, 0.U) === RegNext(io.mem.req.bits.addr, 0.U))
assert(RegNext(resultTLBWire.read.data, 0.U) === RegNext(io.mem.resp.bits.rdata, 0.U))
}
// state machine to handle miss(ptw) and pte-writing-back
switch (state) {
is (s_idle) {
Expand All @@ -290,15 +301,25 @@ class EmbeddedTLBExec(implicit val tlbConfig: TLBConfig) extends TlbModule{
needFlush := false.B
}.elsewhen (io.mem.req.fire) { state := s_memReadResp}
}

is (s_memReadResp) {
val missflag = memRdata.flag.asTypeOf(flagBundle)
// assume(!(missflag.x && missflag.w && !missflag.r && missflag.v))
when (io.mem.resp.fire) {
resultTLBWire.read.valid := true.B
resultTLBWire.read.addr := io.mem.req.bits.addr
resultTLBWire.read.data := io.mem.resp.bits.rdata
resultTLBWire.read.level := (level-1.U)
when (isFlush) {
state := s_idle
needFlush := false.B
}.elsewhen (!(missflag.r || missflag.x) && (level===3.U || level===2.U)) {
// !(0||1) && 1
//= 0
// hdd
// D A G U X W R V
// 1 1 0 1 1 1 0 1
when(!missflag.v || (!missflag.r && missflag.w)) { //TODO: fix needflush
// 0 || (1 && 1)
if(tlbname == "itlb") { state := s_wait_resp } else { state := s_miss_slpf }
if(tlbname == "itlb") { missIPF := true.B }
if(tlbname == "dtlb") {
Expand All @@ -311,9 +332,12 @@ class EmbeddedTLBExec(implicit val tlbConfig: TLBConfig) extends TlbModule{
Debug(false, "\n")
}.otherwise {
state := s_memReadReq
// assume(memRdata.reserved === 0.U)
raddr := paddrApply(memRdata.ppn, Mux(level === 3.U, vpn.vpn1, vpn.vpn0))
}
}.elsewhen (level =/= 0.U) { //TODO: fix needFlush
// D A G U X W R V
// 1 1 0 1 1 1 0 1
val permCheck = missflag.v && !(pf.priviledgeMode === ModeU && !missflag.u) && !(pf.priviledgeMode === ModeS && missflag.u && (!pf.status_sum || ifecth))
val permExec = permCheck && missflag.x
val permLoad = permCheck && (missflag.r || pf.status_mxr && missflag.x)
Expand Down
3 changes: 2 additions & 1 deletion src/main/scala/top/Settings.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,8 @@ object FormalSettings {
"HasDcache" -> false,
"HasIcache" -> false,

"MmodeOnly" -> true,
// "MmodeOnly" -> true,
"MmodeOnly" -> false,
"EnableRVC" -> true
)
}
Expand Down

0 comments on commit bb9ff59

Please sign in to comment.