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

Fix FormalPlugin to pass liveness again.

This commit is contained in:
Dolu1990 2017-11-06 23:04:33 +01:00
parent 8098a03a9b
commit 200a73bea0
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/main/scala/vexriscv/plugin/FomalPlugin.scala
View File

@ -53,11 +53,14 @@ case class RvfiPort() extends Bundle with IMasterSlave {
//feature added
//Halt CPU on decoding exception
//VexRiscv changes
//input(INSTRUCTION)(5) REGFILE_WRITE_VALID
//VexRiscv bug
//1) pcManagerService.createJumpInterface(pipeline.execute)
// pcManagerService.createJumpInterface(if(earlyBranch) pipeline.execute else pipeline.memory)
//2) input(INSTRUCTION)(5) REGFILE_WRITE_VALID
//3) JALR => clear PC(0)
//2) JALR => clear PC(0)
class FomalPlugin extends Plugin[VexRiscv]{
var rvfi : RvfiPort = null
@ -114,11 +117,14 @@ class FomalPlugin extends Plugin[VexRiscv]{
}
})
when(Delay(haltRequest, 5)){ //Give time for value propagation from decode stage to writeback stage
when(Delay(haltRequest, 5, init=False)){ //Give time for value propagation from decode stage to writeback stage
rvfi.valid := True
rvfi.trap := True
rvfi.halt := True
}
val haltFired = RegInit(False) setWhen(rvfi.valid && rvfi.halt)
rvfi.valid clearWhen(haltFired)
}
}
}