add HaltOnExceptionPlugin

wip

src/main/scala/vexriscv/VexRiscv.scala

@@ -32,6 +32,7 @@ case class VexRiscvConfig(plugins : Seq[Plugin[VexRiscv]]){
   object SRC_LESS_UNSIGNED extends Stageable(Bool)
 
   //Formal verification purposes
+  object FORMAL_HALT       extends Stageable(Bool)
   object FORMAL_PC_NEXT    extends Stageable(UInt(32 bits))
   object FORMAL_MEM_ADDR   extends Stageable(UInt(32 bits))
   object FORMAL_MEM_RMASK  extends Stageable(Bits(4 bits))

src/main/scala/vexriscv/demo/FormalSimple.scala

@@ -12,6 +12,7 @@ object FormalSimple extends App{
     config = VexRiscvConfig(
       plugins = List(
         new FomalPlugin,
+        new HaltOnExceptionPlugin,
         new PcManagerSimplePlugin(
           resetVector = 0x00000000l,
           relaxedPcCalculation = false
@@ -25,11 +26,12 @@ object FormalSimple extends App{
           catchAccessFault = false
         ),
         new DecoderSimplePlugin(
-          catchIllegalInstruction = false
+          catchIllegalInstruction = true,
+          forceLegalInstructionComputation = true
         ),
         new RegFilePlugin(
           regFileReadyKind = plugin.SYNC,
-          zeroBoot = true
+          zeroBoot = false
         ),
         new IntAluPlugin,
         new SrcPlugin(
@@ -48,12 +50,12 @@ object FormalSimple extends App{
         ),
         new BranchPlugin(
           earlyBranch = false,
-          catchAddressMisaligned = false,
+          catchAddressMisaligned = true,
           prediction = NONE
         ),
         new YamlPlugin("cpu0.yaml")
       )
     )
   )
-  SpinalVerilog(cpu())
+  SpinalConfig(defaultConfigForClockDomains = ClockDomainConfig(resetKind = spinal.core.SYNC)).generateVerilog(cpu())
 }

src/main/scala/vexriscv/plugin/BranchPlugin.scala

@@ -65,7 +65,7 @@ class BranchPlugin(earlyBranch : Boolean,
     ))
 
     val pcManagerService = pipeline.service(classOf[JumpService])
-    jumpInterface = pcManagerService.createJumpInterface(pipeline.execute)
+    jumpInterface = pcManagerService.createJumpInterface(if(earlyBranch) pipeline.execute else pipeline.memory)
     if (prediction != NONE)
       predictionJumpInterface = pcManagerService.createJumpInterface(pipeline.decode)
 
@@ -114,7 +114,9 @@ class BranchPlugin(earlyBranch : Boolean,
         BranchCtrlEnum.JALR -> imm.i_sext,
         default             -> imm.b_sext
       ).asUInt
-      insert(BRANCH_CALC) := branch_src1 + branch_src2
+
+      val branchAdder = branch_src1 + branch_src2
+      insert(BRANCH_CALC) := branchAdder(31 downto 1) @@ ((input(BRANCH_CTRL) === BranchCtrlEnum.JALR) ? False | branchAdder(0))
     }
 
     //Apply branchs (JAL,JALR, Bxx)
@@ -220,7 +222,8 @@ class BranchPlugin(earlyBranch : Boolean,
           branch_src2 := (input(PREDICTION_HAD_BRANCHED) ? B(4) | imm.b_sext).asUInt
         }
       }
-      insert(BRANCH_CALC) := branch_src1 + branch_src2
+      val branchAdder = branch_src1 + branch_src2
+      insert(BRANCH_CALC) := branchAdder(31 downto 1) @@ ((input(BRANCH_CTRL) === BranchCtrlEnum.JALR) ? False | branchAdder(0))
     }
 
 

src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala

@@ -233,7 +233,7 @@ class DBusSimplePlugin(catchAddressMisaligned : Boolean, catchAccessFault : Bool
 
 
       insert(MEMORY_READ_DATA) := dBus.rsp.data
-      arbitration.haltItself setWhen(arbitration.isValid && input(MEMORY_ENABLE) && input(REGFILE_WRITE_VALID) && !dBus.rsp.ready)
+      arbitration.haltItself setWhen(arbitration.isValid && input(MEMORY_ENABLE) && !input(INSTRUCTION)(5) && !dBus.rsp.ready)
 
       if(catchAccessFault || catchAddressMisaligned){
         if(!catchAccessFault){

src/main/scala/vexriscv/plugin/DecoderSimplePlugin.scala

@@ -39,7 +39,7 @@ case class Masked(value : BigInt,care : BigInt){
   def toString(bitCount : Int) = (0 until bitCount).map(i => if(care.testBit(i)) (if(value.testBit(i)) "1" else "0") else "-").reverseIterator.reduce(_+_)
 }
 
-class DecoderSimplePlugin(catchIllegalInstruction : Boolean) extends Plugin[VexRiscv] with DecoderService {
+class DecoderSimplePlugin(catchIllegalInstruction : Boolean, forceLegalInstructionComputation : Boolean = false) extends Plugin[VexRiscv] with DecoderService {
   override def add(encoding: Seq[(MaskedLiteral, Seq[(Stageable[_ <: BaseType], Any)])]): Unit = encoding.foreach(e => this.add(e._1,e._2))
   override def add(key: MaskedLiteral, values: Seq[(Stageable[_ <: BaseType], Any)]): Unit = {
     assert(!encodings.contains(key))
@@ -118,7 +118,7 @@ class DecoderSimplePlugin(catchIllegalInstruction : Boolean) extends Plugin[VexR
     // logic implementation
     val decodedBits = Bits(stageables.foldLeft(0)(_ + _.dataType.getBitsWidth) bits)
     decodedBits := Symplify(input(INSTRUCTION),spec, decodedBits.getWidth)
-    if(catchIllegalInstruction) insert(LEGAL_INSTRUCTION) := Symplify.logicOf(input(INSTRUCTION), SymplifyBit.getPrimeImplicants(spec.unzip._1.toSeq, 32))
+    if(catchIllegalInstruction || forceLegalInstructionComputation) insert(LEGAL_INSTRUCTION) := Symplify.logicOf(input(INSTRUCTION), SymplifyBit.getPrimeImplicants(spec.unzip._1.toSeq, 32))
 
 
     //Unpack decodedBits and insert fields in the pipeline

src/main/scala/vexriscv/plugin/FomalPlugin.scala

@@ -45,8 +45,19 @@ case class RvfiPort() extends Bundle with IMasterSlave {
 }
 
 
+//Tool stuff
+//https://www.reddit.com/r/yosys/comments/77g5hn/unsupported_cell_type_error_adff/
+//rd_addr == 0  => no rd_wdata check
+//instruction that doesn't use RSx have to force the formal port address to zero
 
+//feature added
+//Halt CPU on decoding exception
 
+//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)
 class FomalPlugin extends Plugin[VexRiscv]{
 
   var rvfi : RvfiPort = null
@@ -69,18 +80,23 @@ class FomalPlugin extends Plugin[VexRiscv]{
         order := order + 1
       }
 
+
       rvfi.valid :=  arbitration.isFiring
       rvfi.order := order
       rvfi.insn := output(INSTRUCTION)
       rvfi.trap := False
       rvfi.halt := False
       rvfi.intr := False
-      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)
-      rvfi.rs2.rdata := output(RS2)
+//      rvfi.rs2.rdata := output(RS2)
+      rvfi.rs1.addr := output(RS1_USE) ? output(INSTRUCTION)(rs1Range).asUInt | U(0)
+      rvfi.rs2.addr := output(RS2_USE) ? output(INSTRUCTION)(rs2Range).asUInt | U(0)
+      rvfi.rs1.rdata := output(RS1_USE) ? output(RS1) | B(0)
+      rvfi.rs2.rdata := output(RS2_USE) ? output(RS2) | B(0)
       rvfi.rd.addr := output(REGFILE_WRITE_VALID) ? output(INSTRUCTION)(rdRange).asUInt | U(0)
-      rvfi.rd.wdata := output(REGFILE_WRITE_DATA)
+      rvfi.rd.wdata := output(REGFILE_WRITE_VALID) ? output(REGFILE_WRITE_DATA) | B(0)
       rvfi.pc.rdata := output(PC)
       rvfi.pc.wdata := output(FORMAL_PC_NEXT)
       rvfi.mem.addr  := output(FORMAL_MEM_ADDR)
@@ -88,6 +104,21 @@ class FomalPlugin extends Plugin[VexRiscv]{
       rvfi.mem.wmask := output(FORMAL_MEM_WMASK)
       rvfi.mem.rdata := output(FORMAL_MEM_RDATA)
       rvfi.mem.wdata := output(FORMAL_MEM_WDATA)
+
+      val haltRequest = False
+      stages.map(s => {
+        when(s.arbitration.isValid && s.output(FORMAL_HALT)){ //Stage is exception halted
+          when(stages.drop(indexOf(s) + 1).map(!_.arbitration.isValid).foldLeft(True)(_ && _)){ //There nothing in futher stages
+            haltRequest := True
+          }
+        }
+      })
+
+      when(Delay(haltRequest, 5)){ //Give time for value propagation from decode stage to writeback stage
+        rvfi.valid := True
+        rvfi.trap := True
+        rvfi.halt := True
+      }
     }
   }
 }

src/main/scala/vexriscv/plugin/HaltOnExceptionPlugin.scala

@@ -0,0 +1,38 @@
+
+package vexriscv.plugin
+
+import spinal.core._
+import spinal.lib._
+import vexriscv._
+import vexriscv.Riscv._
+
+import scala.collection.mutable.ArrayBuffer
+import scala.collection.mutable
+
+
+class HaltOnExceptionPlugin() extends Plugin[VexRiscv] with ExceptionService {
+  def xlen = 32
+
+  //Mannage ExceptionService calls
+  val exceptionPortsInfos = ArrayBuffer[ExceptionPortInfo]()
+  def exceptionCodeWidth = 4
+  override def newExceptionPort(stage : Stage, priority : Int = 0) = {
+    val interface = Flow(ExceptionCause())
+    exceptionPortsInfos += ExceptionPortInfo(interface,stage,priority)
+    interface
+  }
+
+  override def build(pipeline: VexRiscv): Unit = {
+    import pipeline._
+    import pipeline.config._
+    stages.head.insert(FORMAL_HALT) := False
+    stages.foreach(stage => {
+      val stagePorts = exceptionPortsInfos.filter(_.stage == stage)
+      if(stagePorts.nonEmpty)
+        when(stagePorts.map(_.port.valid).orR){
+          stage.output(FORMAL_HALT) := True
+          stage.arbitration.haltItself := True
+        }
+    })
+  }
+}