From 92c654ea984f0a8a5269b7fde11d0c7689fdfc93 Mon Sep 17 00:00:00 2001 From: liuyic00 Date: Wed, 10 Jul 2024 11:12:07 +0800 Subject: [PATCH] Fix Scala version problem and support CHA (#18) * build: fix efficiency issues cause by Scala2.13 and ChiselTest0.6 by downgrade to Scala2.12.17 * ci: remove special config for test * build: add CHA version Chisel support through compiling option * docs: update Chinese README --- .github/workflows/Test.yml | 2 +- .scalafmt.conf | 2 +- README.md | 4 +- README.zh-CN.md | 257 +++++++++++++++++++++++++++++++++++++ build.sbt | 37 ++++-- readme_cn.md | 125 ------------------ 6 files changed, 284 insertions(+), 143 deletions(-) create mode 100644 README.zh-CN.md delete mode 100644 readme_cn.md diff --git a/.github/workflows/Test.yml b/.github/workflows/Test.yml index cac10e5..02b3f6e 100644 --- a/.github/workflows/Test.yml +++ b/.github/workflows/Test.yml @@ -16,4 +16,4 @@ jobs: - name: Cache Scala uses: coursier/cache-action@v5 - name: SBT Test - run: sbt "++ 2.12.15! test" + run: sbt test diff --git a/.scalafmt.conf b/.scalafmt.conf index d0df53a..4c55e09 100644 --- a/.scalafmt.conf +++ b/.scalafmt.conf @@ -1,5 +1,5 @@ version = "3.7.15" -runner.dialect = scala213 +runner.dialect = scala212 maxColumn = 120 docstrings.wrapMaxColumn = 80 diff --git a/README.md b/README.md index bc3be9f..d6dfac3 100644 --- a/README.md +++ b/README.md @@ -8,10 +8,10 @@ semantics of the RISC-V ISA document, as well as several `Helper` and `Checker` to connect the user's processor design with the reference model and set verification conditions. -Reference model support RV32/64IMAC, Zicsr, Zifencei, MSU privilege level, +Reference model support RV32/64IMC, Zicsr, MSU privilege level, virtual-momory system with Sv39. -[中文说明](readme_cn.md) +Read more detailed Chinese README: [中文说明](README.zh-CN.md). ## Table of Contents diff --git a/README.zh-CN.md b/README.zh-CN.md new file mode 100644 index 0000000..e89b982 --- /dev/null +++ b/README.zh-CN.md @@ -0,0 +1,257 @@ +# RISC-V Spec Core + +本项目是对 RISC-V 处理器 Chisel 设计的指令集一致性进行形式化验证/测试的工具。 +其中包括一个可配置的 `RiscvCore` 作为参考模型来表达 RISC-V 指令集规范文档的语义，和一些 `Helper`、`Checker` 来连接待验证处理器与参考模型和设置验证条件。 + +其中参考模型支持 RV32/64IMC、Zicsr，MSU 特权级，基于 Sv39 页表分页方案的虚拟内存。 + +[English README](README.md) + +## 目录 + +- [安装](#安装) + - [使用本地发布版本（推荐）](#使用本地发布版本推荐) + - [使用托管版本](#使用托管版本) +- [用法](#用法) + - [添加 Checker 并设置基本信号](#添加-checker-并设置基本信号) + - [参考模型配置选项](#参考模型配置选项) + - [通过 ConnectHelper 获取更多信号](#通过-connecthelper-获取更多信号) + - [获取通用寄存器值](#获取通用寄存器值) + - [获取异常处理与 CSR 寄存器值](#获取异常处理与-csr-寄存器值) + - [获取 TLB 访存相关信号值](#获取-tlb-访存相关信号值) + - [获取访存信号值](#获取访存信号值) + - [设置验证条件](#设置验证条件) + - [通过 ChiselTest 调用形式化验证](#通过-chiseltest-调用形式化验证) +- [验证实例](#验证实例) + +## 安装 + +本项目可以作为项目依赖添加在 Chisel 处理器设计中。 +可以[使用本地发布版本（推荐）](#使用本地发布版本推荐)或者[使用托管版本](#使用托管版本)。 + +### 使用本地发布版本（推荐） + +由于本项目开发可能造成接口变化，使用本地发布的版本可以自行进行版本控制，避免因为依赖更新造成代码突然无法运行。 + +下载项目代码并发布到本地： + +```shell +git clone https://github.com/iscas-tis/riscv-spec-core.git +cd riscv-spec-core +sbt +publishLocal # 将所有交叉编译的版本发布到本地 +# 和 CHA 一起使用请替换为下述命令，以在项目中依赖 CHA 版本的 Chisel： +# sbt -DCHA=true +publishLocal +``` + +在 `build.sbt` 中添加依赖： + +```scala +libraryDependencies += "cn.ac.ios.tis" %% "riscvspeccore" % "1.1-SNAPSHOT" +// CHA 版本请使用： +// libraryDependencies += "cn.ac.ios.tis" %% "riscvspeccore" % "1.1-cha-SNAPSHOT" +``` + +### 使用托管版本 + +本项目 main 分支代码会自动发布到 Maven 仓库，也可以直接在项目中添加依赖。 +托管版本暂不提供 CHA 版本；SNAPSHOT 版较正式版有新的变动，建议使用 SNAPSHOT 版。 +希望锁定依赖版本请[使用本地发布版本（推荐）](#使用本地发布版本推荐)。 + +在 `build.sbt` 中添加代码： + +```scala +resolvers += Resolver.sonatypeRepo("snapshots") // 添加 SNAPSHOT 版本仓库 +libraryDependencies += "cn.ac.ios.tis" %% "riscvspeccore" % "1.1-SNAPSHOT" +``` + +## 用法 + +安装成功后按照下述流程，在处理器中添加代码接入验证。 +或者可以直接参考我们给出的[例子](#验证实例)。 + +### 添加 Checker 并设置基本信号 + +`Checker` 是一个硬件电路模块，其中包含一个 RISC-V 参考模型和预设的指令集一致性性质。 +通过工具提供的一些接口和方法，可以将处理器指令执行信息传入 `Checker`，组成一个可验证的系统。 + +`Checker` 需要获取一条指令的完整执行信息，包括指令本身、PC、更新后的寄存器等，可以将 `Checker` 实例化在指令提交级（如写回级）。 + +```scala + +// 1. 设置 Checker 中参考模型 `RiscvCore` 支持的功能 +// 此处配置为：RV64I 基础指令集，支持 M、C 指令扩展，支持 M/S 两个特权级 +import rvspeccore.core.RV64Config +val FormalConfig = RV64Config("MCS") + +// 2. 实例化 Checker +// 此处实例化一个检查完整寄存器值的 Checker，启用内存检查，使用之前设置的参考模型设置 +import rvspeccore.checker._ +val checker = Module(new CheckerWithResult(checkMem = true)(FormalConfig)) + +// 3. 设置指令提交信号 +// 当一条指令完全执行结束，所有所需的数据应该准备好，`instCommit.valid` 应该为 true.B +// RiscvCore 将在收到指令后的一个时钟内执行这条指令，得到执行结果 +// checker 会在几个时钟内触发性质进行检查 +checker.io.instCommit.valid := XXX +checker.io.instCommit.inst := XXX +checker.io.instCommit.pc := XXX + +// 4. 为信号连接工具 ConnectHelper 设置上文创建的 checker +// 在其他模块中获取的信号将通过 ConnectHelper 传递给 checker +// 此处为 CheckerWithResult 类型 Checker 专用的连接工具 ConnectCheckerResult +import rvspeccore.checker._ +ConnectCheckerResult.setChecker(checker)(XLEN, FormalConfig) +``` + +目前 `Checker` 中只有 `CheckerWithResult` 经过了验证，推荐使用。 + +#### 参考模型配置选项 + +参考模型具体支持的配置选项如下： + +- 位宽和基础指令集 + - `RV64Config`：64位，包含基础指令集 I + - `RV32Config`：32位，包含基础指令集 I +- 扩展指令集 + - "M"：乘除法扩展指令集 M + - "C"：压缩扩展指令集 C +- 特权级 + - 默认包含机器级 M + - "S"：系统级 S + +### 通过 ConnectHelper 获取更多信号 + +`ConnectHelper` 封装了一些飞线（`BoringUtils`）方法，可以跨模块获取信号值。 +需要注意，获取的所有信号值要和指令提交的时钟同步，可能需要通过 `Reg` 调整。 + +目前 `ConnectHelper` 只提供了与 `CheckerWithResult` 对应的 `ConnectCheckerResult`，在 `rvspeccore.checker.ConnectCheckerResult`。 + +#### 获取通用寄存器值 + +对于 `Vec(32, UInt(XLEN.W))` 类型的 `regFile`，可以直接设置寄存器值： + +```scala +ConnectCheckerResult.setRegSource(rf) +``` + +如果不是，需要自行通过 `Vec` 转换格式： + +```scala +val resultRegWire = Wire(Vec(32, UInt(XLEN.W))) +resultRegWire := rf +resultRegWire(0) := 0.U // 该例子中 rf 的 x0 值不总是保持 0，此处手工适配 +ConnectCheckerResult.setRegSource(resultRegWire) +``` + +#### 获取异常处理与 CSR 寄存器值 + +```scala +// CSR寄存器 +val resultCSRWire = ConnectCheckerResult.makeCSRSource()(64, FormalConfig) +resultCSRWire.misa := RegNext(misa) +resultCSRWire.mvendorid := XXX +resultCSRWire.marchid := XXX +// ······ +// 异常处理 +val resultEventWire = ConnectCheckerResult.makeEventSource()(64, FormalConfig) +resultEventWire.valid := XXX +resultEventWire.intrNO := XXX +resultEventWire.cause := XXX +resultEventWire.exceptionPC := XXX +resultEventWire.exceptionInst := XXX +// ······ +``` + +#### 获取 TLB 访存相关信号值 + +通常在待验证处理器的 TLB 模块中获得信号值，需要分析待验证处理器的 TLB 访存状态机。 + +```scala +val resultTLBWire = ConnectCheckerResult.makeTLBSource(if(tlbname == "itlb") false else true)(64) +// 获得访存值 +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) +// ······ +``` + +#### 获取访存信号值 + +在待验证处理器对外进行直接访存的时，从中获得相应的值，需要分析待验证处理器的访存状态机。 + +```scala +val mem = ConnectCheckerResult.makeMemSource()(64) +when(backend.io.dmem.resp.fire) { + // load or store complete + when(isRead) { + isRead := false.B + mem.read.valid := true.B + mem.read.addr := SignExt(addr, 64) + mem.read.data := backend.io.dmem.resp.bits.rdata + mem.read.memWidth := width + }.elsewhen(isWrite) { + isWrite := false.B + mem.write.valid := true.B + mem.write.addr := SignExt(addr, 64) + mem.write.data := wdata + mem.write.memWidth := width + // pass addr wdata wmask + }.otherwise { + // assert(false.B) + // may receive some acceptable error resp, but microstructure can handle + } +} +``` + +### 设置验证条件 + +对于形式化验证，可以通过 `assume` 设置验证的前置条件，仅验证满足 `assume` 条件下的情况。 +本项目提供了工具来判断指令的种类，当指令属于该分类时返回 `true.B`，示例如下： + +```scala +import rvspeccore.checker._ +val inst = XXX // 完整 32 位指令 + +// 要求 inst 是 RVI 指令集中的一条指令，位宽为隐式参数 `implicit XLEN: Int` +assume(RVI(inst)) +// 要求 inst 是 RVI 指令集中的一条指令，显式指定位宽为 64 +assume(RVI(inst)(64)) +// 要求 inst 是 RVI 指令集中寄存器和立即数的运算指令 +assume(RVI.regImm(inst)) +// 要求 inst 是 ADDI 或 ADD 指令 +assume(RVI.ADDI(inst) || RVI.ADD(inst)) +``` + +更多指令分类见代码。 + +### 通过 ChiselTest 调用形式化验证 + +待验证处理器和参考模型连接之后，可以使用测试方法，也可以使用形式化验证在约束的范围内进行检查。 + +下面通过 ChiselTest 对连接好参考模型的 `DUT` 进行形式化验证，调用了 +[BtorMC](https://github.com/Boolector/btor2tools) +模型检测工具，使用 BMC 算法检查了 12 个时钟周期内的指令集一致性： + +```scala +import chisel3._ +import chiseltest._ +import chiseltest.formal._ +import org.scalatest.flatspec.AnyFlatSpec + +import dut._ + +class DUTFormalSpec extends AnyFlatSpec with Formal with ChiselScalatestTester { + behavior of "DUT" + it should "pass BMC check" in { + verify(new DUT(), Seq(BoundedCheck(12), BtormcEngineAnnotation)) + } +} +``` + +## 验证实例 + +[nutshell-fv](https://github.com/iscas-tis/nutshell-fv) +该项目是在 [NutShell](https://github.com/OSCPU/NutShell) 上进行验证的例子。 +我们修改了 NutShell 代码以获取验证所需的处理器信息，并与参考模型进行了同步。 +最终通过 [ChiselTest](https://github.com/ucb-bar/chiseltest) 提供的接口调用了 BMC 算法进行验证。 diff --git a/build.sbt b/build.sbt index cd5e8bd..b45b31f 100644 --- a/build.sbt +++ b/build.sbt @@ -1,6 +1,12 @@ -ThisBuild / version := "1.1-SNAPSHOT" +// use `-DCHA=true` to use CHA version Chisel +lazy val useCHA: Boolean = + sys.props.getOrElse("CHA", "false").toLowerCase == "true" + +ThisBuild / version := { if (useCHA) "1.1-cha-SNAPSHOT" else "1.1-SNAPSHOT" } ThisBuild / organization := "cn.ac.ios.tis" -ThisBuild / scalaVersion := "2.13.8" +ThisBuild / scalaVersion := "2.12.17" +// Use Scala2.13 with ChiselTest0.6.0 will cause efficiency issues in the +// simulation. Here use Scala2.12 and ChiselTest0.6.0 to avoid this problem. ThisBuild / crossScalaVersions := Seq("2.12.15", "2.13.8") @@ -34,23 +40,26 @@ lazy val root = (project in file(".")) .settings(publishSettings: _*) .settings( name := "RiscvSpecCore", - libraryDependencies ++= Seq( - "edu.berkeley.cs" %% "chisel3" % "3.6.0" - ), + libraryDependencies ++= { + if (useCHA) + Seq( + "cn.ac.ios.tis" %% "chisel3" % "3.7-SNAPSHOT", + "cn.ac.ios.tis" %% "chiseltest" % "0.7-SNAPSHOT" % "test" + ) + else + Seq( + "edu.berkeley.cs" %% "chisel3" % "3.6.0", + "edu.berkeley.cs" %% "chiseltest" % "0.6.0" % "test" + ) + }, scalacOptions ++= Seq( "-language:reflectiveCalls", "-deprecation", "-feature", "-Xcheckinit" ), - addCompilerPlugin("edu.berkeley.cs" % "chisel3-plugin" % "3.6.0" cross CrossVersion.full), - // special test configuration to avoid bug in chisel3.6 - // use `sbt "++ 2.12.15! test"` to run tests, should finish in 15 minutes - dependencyOverrides ++= Seq( - "edu.berkeley.cs" %% "chisel3" % "3.5.4" % "test", - compilerPlugin("edu.berkeley.cs" % "chisel3-plugin" % "3.5.4" % "test" cross CrossVersion.full) - ), - libraryDependencies ++= Seq( - "edu.berkeley.cs" %% "chiseltest" % "0.5.4" % "test" + addCompilerPlugin( + if (useCHA) "cn.ac.ios.tis" % "chisel3-plugin" % "3.7-SNAPSHOT" cross CrossVersion.full + else "edu.berkeley.cs" % "chisel3-plugin" % "3.6.0" cross CrossVersion.full ) ) diff --git a/readme_cn.md b/readme_cn.md deleted file mode 100644 index 83b00e5..0000000 --- a/readme_cn.md +++ /dev/null @@ -1,125 +0,0 @@ -# RISC-V Spec Core - -本项目是对 RISC-V 处理器 Chisel 设计的指令集一致性进行形式化验证/测试的工具。 -其中包括一个可配置的 `RiscvCore` 作为参考模型来表达 RISC-V 指令集规范文档的语义， -和一些 `Helper`、`Checker` 来连接待验证处理器与参考模型和设置验证条件。 - -其中参考模型支持 RV32/64IMAC、Zicsr、Zifencei，MSU 特权级，虚拟内存机制和 Sv39 页表分页方案。 - -[English README](README.md) - -## 目录 - -- [用法](#用法) - - [引入依赖](#引入依赖) - - [添加 Checker 并设置基本信号](#添加-checker-并设置基本信号) - - [获取通用寄存器值](#获取通用寄存器值) - - [获取异常处理与 CSR 寄存器值](#获取异常处理与-csr-寄存器值) - - [获取 TLB 访存相关信号值](#获取-tlb-访存相关信号值) - - [获取访存信号值](#获取访存信号值) -- [验证实例](#验证实例) - -## 用法 - -### 引入依赖 - -作为项目依赖使用 riscv-spec-core，在 `build.sbt` 中添加代码： - -```scala -libraryDependencies += "cn.ac.ios.tis" %% "riscvspeccore" % "1.0.0" -``` - -之后按照下述流程，在处理器中添加代码接入验证。 -或者可以直接参考我们给出的[例子](#验证实例)。 - -### 添加 Checker 并设置基本信号 - -在待验证处理器的指令提交处，通常是写回级，声明一个 `checker` 变量，并设定参考模型支持的指令子集。 - -```scala -val FormalConfig = RV64Config("MCS") -val checker = Module(new CheckerWithResult(checkMem = true)(FormalConfig)) - -checker.io.instCommit.valid := XXX -checker.io.instCommit.inst := XXX -checker.io.instCommit.pc := XXX - -ConnectCheckerResult.setChecker(checker)(XLEN, FormalConfig) -``` - -### 获取通用寄存器值 - -```scala -val resultRegWire = Wire(Vec(32, UInt(XLEN.W))) -resultRegWire := rf -resultRegWire(0) := 0.U -ConnectCheckerResult.setRegSource(resultRegWire) -``` - -### 获取异常处理与 CSR 寄存器值 - -```scala -// CSR寄存器 -val resultCSRWire = rvspeccore.checker.ConnectCheckerResult.makeCSRSource()(64, FormalConfig) -resultCSRWire.misa := RegNext(misa) -resultCSRWire.mvendorid := XXX -resultCSRWire.marchid := XXX -// ······ -// 异常处理 -val resultEventWire = rvspeccore.checker.ConnectCheckerResult.makeEventSource()(64, FormalConfig) -resultEventWire.valid := XXX -resultEventWire.intrNO := XXX -resultEventWire.cause := XXX -resultEventWire.exceptionPC := XXX -resultEventWire.exceptionInst := XXX -// ······ -``` - -### 获取 TLB 访存相关信号值 - -通常在待验证处理器的TLB模块中获得信号值，需要分析待验证处理器的 TLB 访存状态机。 - -```scala -val resultTLBWire = rvspeccore.checker.ConnectCheckerResult.makeTLBSource(if(tlbname == "itlb") false else true)(64) -// 获得访存值 -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) -// ······ -``` - -### 获取访存信号值 - -在待验证处理器对外进行直接访存的时，从中获得相应的值，需要分析待验证处理器的访存状态机。 - -```scala -val mem = rvspeccore.checker.ConnectCheckerResult.makeMemSource()(64) -when(backend.io.dmem.resp.fire) { - // load or store complete - when(isRead) { - isRead := false.B - mem.read.valid := true.B - mem.read.addr := SignExt(addr, 64) - mem.read.data := backend.io.dmem.resp.bits.rdata - mem.read.memWidth := width - }.elsewhen(isWrite) { - isWrite := false.B - mem.write.valid := true.B - mem.write.addr := SignExt(addr, 64) - mem.write.data := wdata - mem.write.memWidth := width - // pass addr wdata wmask - }.otherwise { - // assert(false.B) - // may receive some acceptable error resp, but microstructure can handle - } -} -``` - -## 验证实例 - -[nutshell-fv](https://github.com/iscas-tis/nutshell-fv) -该项目是在 [NutShell](https://github.com/OSCPU/NutShell) 上进行验证的例子。 -我们修改了 NutShell 代码以获取验证所需的处理器信息，并与参考模型进行了同步。 -最终通过 [ChiselTest](https://github.com/ucb-bar/chiseltest) 提供的接口调用了 BMC 算法进行验证。