Merge branch 'formal'

src/main/scala/vexriscv/VexRiscv.scala

@@ -31,6 +31,15 @@ case class VexRiscvConfig(plugins : Seq[Plugin[VexRiscv]]){
   object SRC_USE_SUB_LESS extends Stageable(Bool)
   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))
+  object FORMAL_MEM_WMASK  extends Stageable(Bits(4 bits))
+  object FORMAL_MEM_RDATA  extends Stageable(Bits(32 bits))
+  object FORMAL_MEM_WDATA  extends Stageable(Bits(32 bits))
+
 
   object Src1CtrlEnum extends SpinalEnum(binarySequential){
     val RS, IMU, FOUR = newElement()   //IMU, IMZ IMJB

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

@@ -0,0 +1,66 @@
+package vexriscv.demo
+
+import vexriscv.plugin._
+import vexriscv.{plugin, VexRiscv, VexRiscvConfig}
+import spinal.core._
+
+/**
+  * Created by spinalvm on 15.06.17.
+  */
+object FormalSimple extends App{
+  def cpu() = new VexRiscv(
+    config = VexRiscvConfig(
+      plugins = List(
+        new FomalPlugin,
+        new HaltOnExceptionPlugin,
+        new PcManagerSimplePlugin(
+          resetVector = 0x00000000l,
+          relaxedPcCalculation = false
+        ),
+        new IBusSimplePlugin(
+          interfaceKeepData = false,
+          catchAccessFault = false
+        ),
+        new DBusSimplePlugin(
+          catchAddressMisaligned = false,
+          catchAccessFault = false
+        ),
+        new DecoderSimplePlugin(
+          catchIllegalInstruction = true,
+          forceLegalInstructionComputation = true
+        ),
+        new RegFilePlugin(
+          regFileReadyKind = plugin.SYNC,
+          zeroBoot = false
+        ),
+        new IntAluPlugin,
+        new SrcPlugin(
+          separatedAddSub = false,
+          executeInsertion = false
+        ),
+        new FullBarrielShifterPlugin,
+        new HazardSimplePlugin(
+          bypassExecute           = false,
+          bypassMemory            = false,
+          bypassWriteBack         = false,
+          bypassWriteBackBuffer   = false,
+          pessimisticUseSrc       = false,
+          pessimisticWriteRegFile = false,
+          pessimisticAddressMatch = false
+        ),
+        new BranchPlugin(
+          earlyBranch = false,
+          catchAddressMisaligned = true,
+          prediction = NONE
+        ),
+        new YamlPlugin("cpu0.yaml")
+      )
+    )
+  )
+  SpinalConfig(
+    defaultConfigForClockDomains = ClockDomainConfig(
+      resetKind = spinal.core.SYNC,
+      resetActiveLevel = spinal.core.HIGH
+    )
+  ).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

@@ -214,6 +214,17 @@ class DBusSimplePlugin(catchAddressMisaligned : Boolean, catchAccessFault : Bool
       }
 
       insert(MEMORY_ADDRESS_LOW) := dBus.cmd.address(1 downto 0)
+
+      //formal
+      val formalMask = dBus.cmd.size.mux(
+        U(0) -> B"0001",
+        U(1) -> B"0011",
+        default -> B"1111"
+      )
+      insert(FORMAL_MEM_ADDR) := dBus.cmd.address
+      insert(FORMAL_MEM_WMASK) := (dBus.cmd.valid &&  dBus.cmd.wr) ? formalMask | B"0000"
+      insert(FORMAL_MEM_RMASK) := (dBus.cmd.valid && !dBus.cmd.wr) ? formalMask | B"0000"
+      insert(FORMAL_MEM_WDATA) := dBus.cmd.payload.data
     }
 
     //Collect dBus.rsp read responses
@@ -222,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){
@@ -275,6 +286,9 @@ class DBusSimplePlugin(catchAddressMisaligned : Boolean, catchAccessFault : Bool
 
       if(!earlyInjection)
         assert(!(arbitration.isValid && input(MEMORY_ENABLE) && !input(INSTRUCTION)(5) && arbitration.isStuck),"DBusSimplePlugin doesn't allow memory stage stall when read happend")
+
+      //formal
+      insert(FORMAL_MEM_RDATA) := rspFormated
     }
   }
 }

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

@@ -40,7 +40,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))
@@ -119,7 +119,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

@@ -0,0 +1,131 @@
+package vexriscv.plugin
+
+import spinal.core._
+import spinal.lib._
+import vexriscv.VexRiscv
+
+case class RvfiPortRsRead() extends Bundle{
+  val addr = UInt(5 bits)
+  val rdata = Bits(32 bits)
+}
+
+case class RvfiPortRsWrite() extends Bundle{
+  val addr = UInt(5 bits)
+  val wdata = Bits(32 bits)
+}
+
+case class RvfiPortPc() extends Bundle{
+  val rdata = UInt(32 bits)
+  val wdata = UInt(32 bits)
+}
+
+
+case class RvfiPortMem() extends Bundle{
+  val addr  = UInt(32 bits)
+  val rmask = Bits(4 bits)
+  val wmask = Bits(4 bits)
+  val rdata = Bits(32 bits)
+  val wdata = Bits(32 bits)
+}
+
+case class RvfiPort() extends Bundle with IMasterSlave {
+  val valid = Bool
+  val order = UInt(64 bits)
+  val insn = Bits(32 bits)
+  val trap = Bool
+  val halt = Bool
+  val intr = Bool
+  val rs1 = RvfiPortRsRead()
+  val rs2 = RvfiPortRsRead()
+  val rd = RvfiPortRsWrite()
+  val pc = RvfiPortPc()
+  val mem = RvfiPortMem()
+
+  override def asMaster(): Unit = out(this)
+}
+
+
+//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 changes
+//
+
+//VexRiscv bug
+//1) pcManagerService.createJumpInterface(pipeline.execute)
+//   pcManagerService.createJumpInterface(if(earlyBranch) pipeline.execute else pipeline.memory)
+//2) JALR => clear PC(0)
+//3) input(INSTRUCTION)(5)  REGFILE_WRITE_VALID  memory read with exception would not fire properly
+
+class FomalPlugin extends Plugin[VexRiscv]{
+
+  var rvfi : RvfiPort = null
+
+
+  override def setup(pipeline: VexRiscv): Unit = {
+    rvfi = master(RvfiPort()).setName("rvfi")
+  }
+
+  override def build(pipeline: VexRiscv): Unit = {
+    import pipeline._
+    import pipeline.config._
+    import vexriscv.Riscv._
+
+    writeBack plug new Area{
+      import writeBack._
+
+      val order = Reg(UInt(64 bits)) init(0)
+      when(arbitration.isFiring){
+        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.rs2.addr  := output(INSTRUCTION)(rs2Range).asUInt
+//      rvfi.rs1.rdata := output(RS1)
+//      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_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)
+      rvfi.mem.rmask := output(FORMAL_MEM_RMASK)
+      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, 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)
+    }
+  }
+}

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
+        }
+    })
+  }
+}

src/main/scala/vexriscv/plugin/PcManagerSimplePlugin.scala

@@ -24,16 +24,27 @@ class PcManagerSimplePlugin(resetVector       : BigInt,
 
 
   override def build(pipeline: VexRiscv): Unit = {
+    import pipeline.config._
+    import pipeline._
+
     if(relaxedPcCalculation)
       relaxedImpl(pipeline)
     else
       cycleEffectiveImpl(pipeline)
+
+    //Formal verification signals generation
+    prefetch.insert(FORMAL_PC_NEXT) := prefetch.input(PC) + 4
+    jumpInfos.foreach(info => {
+      when(info.interface.valid){
+        info.stage.output(FORMAL_PC_NEXT) := info.interface.payload
+      }
+    })
   }
 
   //reduce combinatorial path, and expose the PC to the pipeline as a register
   def relaxedImpl(pipeline: VexRiscv): Unit = {
     import pipeline.config._
-    import pipeline.prefetch
+    import pipeline._
 
     prefetch plug new Area {
       import prefetch._