h&$      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdef RISC-V ISA(c) David Cox, 2024 BSD-3-Clausestandardsemiconductor@gmail.comNone&'(./8:<=>?9glionLoad operationhlionStore operationilionBranch operationjlion ALU operationklionExecute pipeline instructionllionMemory pipeline instructionmlionWriteback pipeline instructionnlionbranch calculationgopqrshtuvwxyz{|i}~jklmnLion arithmetic logic unit(c) David Cox, 2021-2024 BSD-3-Clausestandardsemiconductor@gmail.comNone&'(./8:<=>?"lionALU configurationlion1use hard adder and subtractor from iCE40 SB_MAC16lion-use generic adder and subtractor: (+) and (-)lionaddSub32PipelinedUnsignedlion0 = Add, 1 = Sub)Lion RISC-V Formal Verification Interface(c) David Cox, 2024 BSD-3-Clausestandardsemiconductor@gmail.comNone&'(./8:<=>?lionRISC-V Formal Csr Interface lionRISC-V Formal Interfacelion5When the core retires an instruction, it asserts the J signal and uses the signals described in Rvfi to output the details of the retired instruction. The signals below are only valid during such a cycle and can be driven to arbitrary values in a cycle in which `_rvfiValid is not asserted.lionThe @ field must be set to the instruction index. No indices must be used twice and there must be no gaps. Instructions may be retired in a reordered fashion, as long as causality is preserved (register nad memory write operations must be retired before the read operations that depend on them).lion7 is the instruction word for the retired instruction. In case of an instruction with fewer than ILEN bits, the upper bits of this output must all be zero. For compressed instructions the compressed instruction word must be output on this port. For fused instructions the complete fused instruciton sequence must be outputlionI must be set for an instruction that cannot be decoded as a legal instruction, such as 0x00000000.lion The signal 6 must be set when the instruction is the last instruction that the core retires before halting execution. It should not be set for an instruction that triggers a trap condition if the CPU reacts to the trap by executing a trap handler. This signal enable verification of liveness properties.lion8 must be set for the first instruction that is part of a trap handler, i.e. an instruction that has a A that does not match the B of the previous instruction.lion? must be set to the current privilege level, using the following encoding: 0=U-Mode, 1=S-Mode, 2=Reserved, 3=M-Modelion9 must be set to the value of MXLSXLUXL in the current privilege level, using the following encoding: 1=32, 2=64lionE and G are the decoded rs1 and rs2 register addresses for the retired instruction. For an instruction that reads no rs1/rs2 register, this output can have an arbitrary value. However if this output is nonzero then F or H must carry the value stored in that register in the pre-state.lionF and H are the values of the register addressed by rs1 and rs2 before execute of this instruction. This output must be zero when rs1/rs2 is zero.lionC is the decoded rd register address for the retired instruction. For an instruction that writes no rd register, this output must always be zero.lionD is the value of the register addressed by rd after execution of this instruction. This output must be zero when rd is zero.lion)This is the program counter (pc) before (A) and after (B) execution of this instruciton. I.e. this is the address of the retired instruction and the address of the next instruction.lionFor memory operations (< and/or > are non-zero), :$ holds the accessed memory location. lion<, is a bitmask that specifies which bytes in ; contain valid read data from :.!lion>, is a bitmask that specifies which bytes in =) contain valid data this is written to :."lion;! is the pre-state data read from :. <! specifies which bytes are valid.#lion=# is the post-state data written to :. >! specifies which bytes are valid.KlionUnwrap Rvfi from First monoidLlion%Construct the RISC-V Formal Interface ('&%$#"! )*+,123456789:;<=>?@ABCDEFGHIJKL,+*) ('&%$#"! JIHGFEDCBA@?>=<;:987654321KLRISC-V 5-stage pipeline(c) David Cox, 2024 BSD-3-Clausestandardsemiconductor@gmail.comNone&'(./8:<=>?2'lionPipeline inputsMlionPipeline configurationOlionstart program counterPlionDefault pipeline configurationO = 0lionPipeline outputsQlion Memory busSlionmemory access typeTlionmemory addressUlionmemory byte maskVlionread=Nothing write=Just wrWlion8Memory access - Lion has a shared instruction/memory busXlioninstruction accessYlion data accesslion#Construct instruction memory accesslionConstruct data memory accesslion#First cycle True, then always Falselionexecute stage branch/jumplionmemory stage branch/jumpliondecode stage loadlionexecute stage loadlionmemory stage load/storelionwriteback stage load/storelion memory stage register forwardinglion"writeback stage register forwadinglion5-Stage RISC-V pipelinelionMonadic pipelinelionWriteback stagelion Memory stagelion Execute stagelion Decode stagelionfetch instructionlionforward register writeslion$calcluate byte mask based on addresslion)calculate half word mask based on addresslionslice address based on masklionslice address based on masklion3check if memory address misaligned on word boundarylion8check if memory address misaligned on half-word boundarylion+run monadic action when instruction is Justlioninstruction addresslionmemory addresslion byte masklionwritelionmeRegFwdlionwbRegFwdMNOPQRVUTSWYXLion RISC-V Core(c) David Cox, 2024 BSD-3-Clausestandardsemiconductor@gmail.comNone&'(./8:<=>?Zlion Core outputs\lionshared memory and instruction bus, output from core to memory and peripherals]lion*formal verification interface output, see  https://github.com/standardsemiconductor/lion/tree/main/lion-formal lion-formal for usage^lionCore configuration`lionALU configuration, default: alionpipeline configurationblionDefault core configuration` = a = PclionRISC-V Core: RV32Iclioncore configurationlion#core input, from memory/peripheralslion core outputMNOPQRSTUVWXYZ[]\^_a`bccbP^_a`MNOZ[]\QRSTUVWXY       !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQQRSTTUVWXYZ[\\]^__`abcdefghijklmnopqrstuvwxyz{|}~]^lion-0.4.0.0-inplace Lion.Core Lion.RvfiLion.InstructionLion.Alu Lion.Pipe AluConfigHardSoftRvfiCsr _wdataCsr _rdataCsr _wmaskCsr _rmaskCsr$fGenericRvfiCsr $fShowRvfiCsr $fEqRvfiCsr$fNFDataXRvfiCsrRvfi _rvfiValid _rvfiOrder _rvfiInsn _rvfiTrap _rvfiHalt _rvfiIntr _rvfiMode_rvfiIxl _rvfiRs1Addr _rvfiRs2Addr _rvfiRs1Data _rvfiRs2Data _rvfiRdAddr _rvfiRdWData _rvfiPcRData _rvfiPcWData _rvfiMemAddr _rvfiMemRMask _rvfiMemWMask _rvfiMemRData _rvfiMemWData_rvfiCsrMinstret_rvfiCsrMcycle_rvfiCsrMscratch_rvfiCsrMstatus _rvfiCsrMisardataCsrrmaskCsrwdataCsrwmaskCsr $fGenericRvfi $fShowRvfi$fEqRvfi $fNFDataXRvfi rvfiCsrMcyclervfiCsrMinstret rvfiCsrMisarvfiCsrMscratchrvfiCsrMstatusrvfiHaltrvfiInsnrvfiIntrrvfiIxl rvfiMemAddr rvfiMemRData rvfiMemRMask rvfiMemWData rvfiMemWMaskrvfiMode rvfiOrder rvfiPcRData rvfiPcWData rvfiRdAddr rvfiRdWData rvfiRs1Addr rvfiRs1Data rvfiRs2Addr rvfiRs2DatarvfiTrap rvfiValidfromRvfimkRvfi PipeConfigstartPCdefaultPipeConfigToMem memAccess memAddress memByteMaskmemWrite MemoryAccessInstrMemDataMemFromCoretoMemtoRvfi CoreConfig aluConfig pipeConfigdefaultCoreConfigcore$fGenericCoreConfig$fShowCoreConfig$fEqCoreConfigLoadStoreBranchOpExInstrMeInstrWbInstrbranchLhuLbuLwLhLbSwShSbJumpJalrJalExOpAuipcLuiBgeuBltuBgeBltBneBeqSraSrlXorSltuSltSllAddAndOrSubExAluImmExAluExLoadExStoreExBranchExJumpExMeNopMeLoadMeStoreMeBranchMeJumpMeRegWrWbNopWbStoreWbLoadWbRegWr ExceptionIllegalInstruction parseInstrsliceRdsliceRs1sliceRs2 sliceOpcode sliceFunct3 sliceFunct7 hardAddSubalusoftAluhardAlubaseAluToPipeFromPipeinstrMemdataMem _firstCycle _exBranching _meBranching_deLoad_exLoad _meMemory _wbMemory _meRegFwd _wbRegFwdpipepipeM writebackmemoryexecutedecodefetchfwdbyteMaskhalfMask sliceByte sliceHalf isMisalignedisMisalignedHalf withInstr_fromMem_fromAlu_fromRs2_fromRs1_toRvfi _toAluInput2 _toAluInput1_toAluOp_toRd _toRs2Addr _toRs1Addr_toMemfromAlufromMemfromRs1fromRs2Control toAluInput1 toAluInput2toAluOptoRd toRs1Addr toRs2AddrPipe_control_wbRvfi_wbNRet_wbIR_meRvfi_meIR_exRvfi_exRs2_exRs1_exPC_exIR_dePC_fetchPCdeLoad exBranchingexLoad firstCycle meBranchingmeMemorymeRegFwdwbMemorywbRegFwd mkControlcontroldePCexIRexPCexRs1exRs2exRvfifetchPCmeIRmeRvfiwbIRwbNRetwbRvfimkPipe