From 200a73bea0d988f50a611b2706d546f6fd2e0216 Mon Sep 17 00:00:00 2001 From: Dolu1990 Date: Mon, 6 Nov 2017 23:04:33 +0100 Subject: [PATCH] Fix FormalPlugin to pass liveness again. --- src/main/scala/vexriscv/plugin/FomalPlugin.scala | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/main/scala/vexriscv/plugin/FomalPlugin.scala b/src/main/scala/vexriscv/plugin/FomalPlugin.scala index 89a2420..d8a543b 100644 --- a/src/main/scala/vexriscv/plugin/FomalPlugin.scala +++ b/src/main/scala/vexriscv/plugin/FomalPlugin.scala @@ -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) } } }