From 276f7895e7aa02ec807df36620a0fdc8f6713d31 Mon Sep 17 00:00:00 2001 From: Dolu1990 Date: Sat, 4 Nov 2017 00:55:32 +0100 Subject: [PATCH] Add FormalPlugin Add FormalSimple CPU configuration --- src/main/scala/vexriscv/VexRiscv.scala | 8 ++ .../scala/vexriscv/demo/FormalSimple.scala | 59 ++++++++++++ .../vexriscv/plugin/DBusSimplePlugin.scala | 14 +++ .../scala/vexriscv/plugin/FomalPlugin.scala | 93 +++++++++++++++++++ .../plugin/PcManagerSimplePlugin.scala | 13 ++- 5 files changed, 186 insertions(+), 1 deletion(-) create mode 100644 src/main/scala/vexriscv/demo/FormalSimple.scala create mode 100644 src/main/scala/vexriscv/plugin/FomalPlugin.scala diff --git a/src/main/scala/vexriscv/VexRiscv.scala b/src/main/scala/vexriscv/VexRiscv.scala index 82f7a8c..297570a 100644 --- a/src/main/scala/vexriscv/VexRiscv.scala +++ b/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 diff --git a/src/main/scala/vexriscv/demo/FormalSimple.scala b/src/main/scala/vexriscv/demo/FormalSimple.scala new file mode 100644 index 0000000..9d28a19 --- /dev/null +++ b/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()) +} diff --git a/src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala b/src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala index b8f50bc..07e21d0 100644 --- a/src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala +++ b/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 } } } diff --git a/src/main/scala/vexriscv/plugin/FomalPlugin.scala b/src/main/scala/vexriscv/plugin/FomalPlugin.scala new file mode 100644 index 0000000..9d03adc --- /dev/null +++ b/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) + } + } +} diff --git a/src/main/scala/vexriscv/plugin/PcManagerSimplePlugin.scala b/src/main/scala/vexriscv/plugin/PcManagerSimplePlugin.scala index 3ec06bb..0c219f0 100644 --- a/src/main/scala/vexriscv/plugin/PcManagerSimplePlugin.scala +++ b/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._