Hardware
/
VexRiscv
mirror of https://github.com/SpinalHDL/VexRiscv.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #253 from mmicko/micko/riscv_formal 

Update to latest risc-v-formal
This commit is contained in:
Dolu1990 2022-05-16 11:48:12 +02:00 committed by GitHub
parent 9c768be7af 32a5206541
commit ba908ebada
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/main/scala/vexriscv/plugin/FormalPlugin.scala
View File

@ -35,6 +35,8 @@ case class RvfiPort() extends Bundle with IMasterSlave {
val trap = Bool val trap = Bool
val halt = Bool val halt = Bool
val intr = Bool val intr = Bool
val mode = Bits(2 bits)
val ixl = Bits(2 bits)
val rs1 = RvfiPortRsRead() val rs1 = RvfiPortRsRead()
val rs2 = RvfiPortRsRead() val rs2 = RvfiPortRsRead()
val rd = RvfiPortRsWrite() val rd = RvfiPortRsWrite()
@ -91,6 +93,8 @@ class FormalPlugin extends Plugin[VexRiscv]{
rvfi.trap := False rvfi.trap := False
rvfi.halt := False rvfi.halt := False
rvfi.intr := False rvfi.intr := False
rvfi.mode := 3
rvfi.ixl := 1
// rvfi.rs1.addr := output(INSTRUCTION)(rs1Range).asUInt // rvfi.rs1.addr := output(INSTRUCTION)(rs1Range).asUInt
// rvfi.rs2.addr := output(INSTRUCTION)(rs2Range).asUInt // rvfi.rs2.addr := output(INSTRUCTION)(rs2Range).asUInt
// rvfi.rs1.rdata := output(RS1) // rvfi.rs1.rdata := output(RS1)