diff --git a/src/main/scala/vexriscv/VexRiscv.scala b/src/main/scala/vexriscv/VexRiscv.scala index 297570a..34f775e 100644 --- a/src/main/scala/vexriscv/VexRiscv.scala +++ b/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)) diff --git a/src/main/scala/vexriscv/demo/FormalSimple.scala b/src/main/scala/vexriscv/demo/FormalSimple.scala index 9d28a19..abb4d1f 100644 --- a/src/main/scala/vexriscv/demo/FormalSimple.scala +++ b/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()) } diff --git a/src/main/scala/vexriscv/plugin/BranchPlugin.scala b/src/main/scala/vexriscv/plugin/BranchPlugin.scala index f6c0e39..d1cbcd2 100644 --- a/src/main/scala/vexriscv/plugin/BranchPlugin.scala +++ b/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)) } diff --git a/src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala b/src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala index 07e21d0..13c2d7e 100644 --- a/src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala +++ b/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){ diff --git a/src/main/scala/vexriscv/plugin/DecoderSimplePlugin.scala b/src/main/scala/vexriscv/plugin/DecoderSimplePlugin.scala index cbcb5d5..3a85412 100644 --- a/src/main/scala/vexriscv/plugin/DecoderSimplePlugin.scala +++ b/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 diff --git a/src/main/scala/vexriscv/plugin/FomalPlugin.scala b/src/main/scala/vexriscv/plugin/FomalPlugin.scala index 9d03adc..89a2420 100644 --- a/src/main/scala/vexriscv/plugin/FomalPlugin.scala +++ b/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.rs2.addr := output(INSTRUCTION)(rs2Range).asUInt - rvfi.rs1.rdata := output(RS1) - rvfi.rs2.rdata := output(RS2) +// 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_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 + } } } } diff --git a/src/main/scala/vexriscv/plugin/HaltOnExceptionPlugin.scala b/src/main/scala/vexriscv/plugin/HaltOnExceptionPlugin.scala new file mode 100644 index 0000000..44c06a9 --- /dev/null +++ b/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 + } + }) + } +}