Add FormalPlugin

Add FormalSimple CPU configuration

src/main/scala/vexriscv/VexRiscv.scala

@@ -31,6 +31,14 @@ 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_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,59 @@
+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 PcManagerSimplePlugin(
+          resetVector = 0x00000000l,
+          relaxedPcCalculation = false
+        ),
+        new IBusSimplePlugin(
+          interfaceKeepData = false,
+          catchAccessFault = false
+        ),
+        new DBusSimplePlugin(
+          catchAddressMisaligned = false,
+          catchAccessFault = false
+        ),
+        new DecoderSimplePlugin(
+          catchIllegalInstruction = false
+        ),
+        new RegFilePlugin(
+          regFileReadyKind = plugin.SYNC,
+          zeroBoot = true
+        ),
+        new IntAluPlugin,
+        new SrcPlugin(
+          separatedAddSub = false,
+          executeInsertion = false
+        ),
+        new LightShifterPlugin,
+        new HazardSimplePlugin(
+          bypassExecute           = false,
+          bypassMemory            = false,
+          bypassWriteBack         = false,
+          bypassWriteBackBuffer   = false,
+          pessimisticUseSrc       = false,
+          pessimisticWriteRegFile = false,
+          pessimisticAddressMatch = false
+        ),
+        new BranchPlugin(
+          earlyBranch = false,
+          catchAddressMisaligned = false,
+          prediction = NONE
+        ),
+        new YamlPlugin("cpu0.yaml")
+      )
+    )
+  )
+  SpinalVerilog(cpu())
+}

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
@@ -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/FomalPlugin.scala

@@ -0,0 +1,93 @@
+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)
+}
+
+
+
+
+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.rd.addr := output(REGFILE_WRITE_VALID) ? output(INSTRUCTION)(rdRange).asUInt | U(0)
+      rvfi.rd.wdata := output(REGFILE_WRITE_DATA)
+      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)
+    }
+  }
+}

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._