1--------------------------------------------------------------------------- 2-- 3-- RISC-V Model 4-- Based on the MIPS specification by Anthony Fox, University of Cambridge 5-- 6-- Copyright (C) 2014, 2015 Anthony Fox, University of Cambridge 7-- Copyright (C) 2014, 2015 Alexandre Joannou, University of Cambridge 8-- Copyright (C) 2015, SRI International. 9-- 10-- This software was developed by SRI International and the University 11-- of Cambridge Computer Laboratory under DARPA/AFRL contract 12-- FA8750-11-C-0249 ("MRC2"), as part of the DARPA MRC research 13-- programme, and under DARPA/AFRL contract FA8750-10-C-0237 14-- ("CTSRD"), as part of the DARPA CRASH research programme. 15-- 16-- See the LICENSE file for details. 17-- 18-- For syntax highlighting, treat this file as Haskell source. 19--------------------------------------------------------------------------- 20 21 22--------------------------------------------------------------------------- 23-- Basic types 24--------------------------------------------------------------------------- 25 26type id = bits(8) -- max 256 cores 27type reg = bits(5) 28type creg = bits(12) 29 30type byte = bits(8) 31type half = bits(16) 32type word = bits(32) 33type dword = bits(64) 34 35type fprnd = bits(3) -- rounding mode 36type fpval = bits(64) 37 38type exc_code = bits(4) 39 40-- raw instructions 41construct rawInstType 42{ Half :: half 43 Word :: word 44} 45 46-- instruction fields 47type opcode = bits(7) 48type imm12 = bits(12) 49type imm20 = bits(20) 50type amo = bits(1) 51 52-- memory and caches 53 54construct accessType { Read, Write } 55construct fetchType { Instruction, Data } 56 57type permType = bits(4) -- memory permissions 58 59nat ASID_SIZE = 6 60nat PAGESIZE_BITS = 12 61nat LEVEL_BITS = 9 62 63type asidType = bits(6) 64 65-- RV64* base. 66 67type regType = dword 68type vAddr = dword 69type pAddr = dword 70 71type pAddrIdx = bits(61) -- raw index into physical memory 72 -- arranged in 8-byte blocks 73 74-- Miscellaneous 75exception UNDEFINED :: string 76exception INTERNAL_ERROR :: string 77 78--------------------------------------------------------------------------- 79-- Memory types for Load/Store instructions 80--------------------------------------------------------------------------- 81 82type memWidth = bits(3) 83 84memWidth BYTE = 0 85memWidth HALFWORD = 1 86memWidth WORD = 3 87memWidth DOUBLEWORD = 7 88 89--------------------------------------------------------------------------- 90-- Processor architecture 91--------------------------------------------------------------------------- 92 93type arch_base = bits(2) 94 95construct Architecture 96{ 97 RV32I, RV64I, RV128I 98} 99 100arch_base archBase(a::Architecture) = 101 match a 102 { case RV32I => 0 103 case RV64I => 2 104 case RV128I => 3 105 } 106 107Architecture architecture(ab::arch_base) = 108 match ab 109 { case 0 => RV32I 110 case 2 => RV64I 111 case 3 => RV128I 112 case _ => #UNDEFINED("Unknown architecture: " : [[ab] :: nat]) 113 } 114 115string archName(a::Architecture) = 116 match a 117 { case RV32I => "RV32I" 118 case RV64I => "RV64I" 119 case RV128I => "RV128I" 120 } 121 122--------------------------------------------------------------------------- 123-- Privilege levels 124--------------------------------------------------------------------------- 125 126type priv_level = bits(2) 127 128construct Privilege 129{ User 130, Supervisor 131, Hypervisor 132, Machine 133} 134 135priv_level privLevel(p::Privilege) = 136 match p 137 { case User => 0 138 case Supervisor => 1 139 case Hypervisor => 2 140 case Machine => 3 141 } 142 143Privilege privilege(p::priv_level) = 144 match p 145 { case 0 => User 146 case 1 => Supervisor 147 case 2 => Hypervisor 148 case 3 => Machine 149 } 150 151string privName(p::Privilege) = 152 match p 153 { case User => "U" 154 case Supervisor => "S" 155 case Hypervisor => "H" 156 case Machine => "M" 157 } 158 159--------------------------------------------------------------------------- 160-- Memory management and virtualization 161--------------------------------------------------------------------------- 162 163type vm_mode = bits(5) 164 165construct VM_Mode 166{ Mbare 167, Mbb 168, Mbbid 169, Sv32 170, Sv39 171, Sv48 172, Sv57 173, Sv64 174} 175 176VM_Mode vmType(vm::vm_mode) = 177 match vm 178 { case 0 => Mbare 179 case 1 => Mbb 180 case 2 => Mbbid 181 case 8 => Sv32 182 case 9 => Sv39 183 case 10 => Sv48 184 case 11 => Sv57 185 case 12 => Sv64 186 case _ => #UNDEFINED("Unknown address translation mode: " : [[vm]::nat]) 187 } 188 189bool isValidVM(vm::vm_mode) = 190 match vm 191 { case 0 or 1 or 2 or 8 or 9 or 10 or 11 or 12 => true 192 case _ => false 193 } 194 195vm_mode vmMode(vm::VM_Mode) = 196 match vm 197 { case Mbare => 0 198 case Mbb => 1 199 case Mbbid => 2 200 case Sv32 => 8 201 case Sv39 => 9 202 case Sv48 => 10 203 case Sv57 => 11 204 case Sv64 => 12 205 } 206 207string vmModeName(vm::VM_Mode) = 208 match vm 209 { case Mbare => "Mbare" 210 case Mbb => "Mbb" 211 case Mbbid => "Mbbid" 212 case Sv32 => "Sv32" 213 case Sv39 => "Sv39" 214 case Sv48 => "Sv48" 215 case Sv57 => "Sv57" 216 case Sv64 => "Sv64" 217 } 218 219--------------------------------------------------------------------------- 220-- Extension Context Status 221--------------------------------------------------------------------------- 222 223type ext_status = bits(2) 224 225construct ExtStatus 226{ Off 227, Initial 228, Clean 229, Dirty 230} 231 232ext_status ext_status(e::ExtStatus) = 233 match e 234 { case Off => 0 235 case Initial => 1 236 case Clean => 2 237 case Dirty => 3 238 } 239 240ExtStatus extStatus(e::ext_status) = 241 match e 242 { case 0 => Off 243 case 1 => Initial 244 case 2 => Clean 245 case 3 => Dirty 246 } 247 248string extStatusName(e::ExtStatus) = 249 match e 250 { case Off => "Off" 251 case Initial => "Initial" 252 case Clean => "Clean" 253 case Dirty => "Dirty" 254 } 255 256--------------------------------------------------------------------------- 257-- Exceptions and Interrupts 258--------------------------------------------------------------------------- 259 260construct Interrupt 261{ Software 262, Timer 263} 264 265exc_code interruptIndex(i::Interrupt) = 266 match i 267 { case Software => 0 268 case Timer => 1 269 } 270 271construct ExceptionType 272{ Fetch_Misaligned 273, Fetch_Fault 274, Illegal_Instr 275, Breakpoint 276, Load_Fault 277, AMO_Misaligned 278, Store_AMO_Fault 279, UMode_Env_Call 280, SMode_Env_Call 281, HMode_Env_Call 282, MMode_Env_Call 283} 284 285exc_code excCode(e::ExceptionType) = 286 match e 287 { case Fetch_Misaligned => 0x0 288 case Fetch_Fault => 0x1 289 case Illegal_Instr => 0x2 290 case Breakpoint => 0x3 291 292 case Load_Fault => 0x5 293 case AMO_Misaligned => 0x6 294 case Store_AMO_Fault => 0x7 295 296 case UMode_Env_Call => 0x8 297 case SMode_Env_Call => 0x9 298 case HMode_Env_Call => 0xA 299 case MMode_Env_Call => 0xB 300 } 301 302ExceptionType excType(e::exc_code) = 303 match e 304 { case 0x0 => Fetch_Misaligned 305 case 0x1 => Fetch_Fault 306 case 0x2 => Illegal_Instr 307 case 0x3 => Breakpoint 308 309 case 0x5 => Load_Fault 310 case 0x6 => AMO_Misaligned 311 case 0x7 => Store_AMO_Fault 312 313 case 0x8 => UMode_Env_Call 314 case 0x9 => SMode_Env_Call 315 case 0xA => HMode_Env_Call 316 case 0xB => MMode_Env_Call 317 318 case _ => #UNDEFINED("Unknown exception: " : [[e]::nat]) 319 } 320 321string excName(e::ExceptionType) = 322 match e 323 { case Fetch_Misaligned => "MISALIGNED_FETCH" 324 case Fetch_Fault => "FAULT_FETCH" 325 case Illegal_Instr => "ILLEGAL_INSTRUCTION" 326 case Breakpoint => "BREAKPOINT" 327 328 case Load_Fault => "FAULT_LOAD" 329 case AMO_Misaligned => "MISALIGNED_AMO" 330 case Store_AMO_Fault => "FAULT_STORE_AMO" 331 332 case UMode_Env_Call => "U-EnvCall" 333 case SMode_Env_Call => "S-EnvCall" 334 case HMode_Env_Call => "H-EnvCall" 335 case MMode_Env_Call => "M-EnvCall" 336 } 337 338--------------------------------------------------------------------------- 339-- Control and Status Registers (CSRs) 340--------------------------------------------------------------------------- 341 342-- Machine-Level CSRs 343 344register mcpuid :: regType 345{ 63-62 : ArchBase -- base architecture, machine mode on reset 346, 20 : U -- user-mode support 347, 18 : S -- supervisor-mode support 348, 12 : M -- integer multiply/divide support 349, 8 : I -- integer base ISA support (XXX: this seems unnecessary) 350} 351 352register mimpid :: regType 353{ 63-16 : RVImpl 354, 15-0 : RVSource 355} 356 357register mstatus :: regType 358{ 63 : MSD -- extended context dirty status 359, 21-17 : VM -- memory management and virtualization 360, 16 : MMPRV -- load/store memory privilege 361, 15-14 : MXS -- extension context status 362, 13-12 : MFS -- floating-point context status 363 -- privilege and global interrupt-enable stack 364, 11-10 : MPRV3 365, 9 : MIE3 366, 8-7 : MPRV2 367, 6 : MIE2 368, 5-4 : MPRV1 369, 3 : MIE1 370, 2-1 : MPRV 371, 0 : MIE 372} 373 374register mtdeleg :: regType 375{ 63-16 : Intr_deleg 376, 15-0 : Exc_deleg 377} 378 379register mip :: regType 380{ -- pending timer interrupts (read-only) 381 7 : MTIP 382, 6 : HTIP 383, 5 : STIP 384 -- pending software interrupts (read/write) 385, 3 : MSIP 386, 2 : HSIP 387, 1 : SSIP 388} 389 390register mie :: regType 391{ -- enable timer interrupts (read-only) 392 7 : MTIE 393, 6 : HTIE 394, 5 : STIE 395 -- enable software interrupts (read/write) 396, 3 : MSIE 397, 2 : HSIE 398, 1 : SSIE 399} 400 401register mcause :: regType 402{ 63 : Int -- Interrupt 403 3-0 : EC -- Exception Code 404} 405 406-- Timers and counters are stored as deltas from their system-values 407-- at each privilege level; the hardware motivation is explained in 408-- the specification. 409 410record MachineCSR 411{ mcpuid :: mcpuid -- information registers 412 mimpid :: mimpid 413 mhartid :: regType 414 415 mstatus :: mstatus -- trap setup 416 mtvec :: regType 417 mtdeleg :: mtdeleg 418 mie :: mie 419 mtimecmp :: regType 420 421 mtime_delta :: regType -- time wrt global clock 422 423 mscratch :: regType -- trap handling 424 mepc :: regType 425 mcause :: mcause 426 mbadaddr :: regType 427 mip :: mip 428 429 mbase :: regType -- protection and translation 430 mbound :: regType 431 mibase :: regType 432 mibound :: regType 433 mdbase :: regType 434 mdbound :: regType 435 436 -- host-target interface (berkeley extensions) 437 mtohost :: regType -- output register to host 438 mfromhost :: regType -- input register from host 439} 440 441-- Hypervisor-Level CSRs 442 443record HypervisorCSR 444{ hstatus :: mstatus -- trap setup 445 htvec :: regType 446 htdeleg :: mtdeleg 447 htimecmp :: regType 448 449 htime_delta :: regType -- time wrt to global clock 450 451 hscratch :: regType -- trap handling 452 hepc :: regType 453 hcause :: mcause 454 hbadaddr :: regType 455} 456 457-- Supervisor-Level CSRs 458 459register sstatus :: regType 460{ 63 : SSD -- extended context dirty status 461, 16 : SMPRV -- load/store memory privilege 462, 15-14 : SXS -- extension context status 463, 13-12 : SFS -- floating-point context status 464, 4 : SPS -- previous privilege level before entering supervisor mode 465, 3 : SPIE -- interrupt-enable before entering supervisor mode 466, 0 : SIE -- supervisor-level interrupt-enable 467} 468 469register sip :: regType 470{ 5 : STIP -- pending timer interrupt 471, 1 : SSIP -- pending software interrupt 472} 473 474register sie :: regType 475{ 5 : STIE -- enable timer interrupt 476, 1 : SSIE -- enable software interrupt 477} 478 479record SupervisorCSR 480{ -- sstatus :: sstatus is a projection of mstatus :: mstatus 481 stvec :: regType -- trap setup 482 -- sie :: sie is a projection of mie :: mie 483 stimecmp :: regType 484 485 stime_delta :: regType -- time wrt global clock 486 487 sscratch :: regType -- trap handling 488 sepc :: regType 489 scause :: mcause 490 sbadaddr :: regType 491 -- sip :: sip is a projection of mip :: mip 492 493 sptbr :: regType -- memory protection and translation 494 sasid :: regType 495} 496 497-- User-Level CSRs 498 499-- floating point control and status 500 501register FPCSR :: word -- 32-bit control register 502{ 7-5 : FRM -- dynamic rounding mode 503 -- exception flags 504, 4 : NV -- invalid operation 505, 3 : DZ -- divide by zero 506, 2 : OF -- overflow 507, 1 : UF -- underflow 508, 0 : NX -- inexact 509} 510 511record UserCSR 512{ cycle_delta :: regType -- timers and counters wrt base values 513 time_delta :: regType 514 instret_delta :: regType 515 fpcsr :: FPCSR 516} 517 518-- Machine state projections 519 520sip lift_mip_sip(mip::mip) = 521{ var sip = sip(0) 522; sip.STIP <- mip.STIP 523; sip.SSIP <- mip.SSIP 524; sip 525} 526 527sie lift_mie_sie(mie::mie) = 528{ var sie = sie(0) 529; sie.STIE <- mie.STIE 530; sie.SSIE <- mie.SSIE 531; sie 532} 533 534mip lower_sip_mip(sip::sip, mip::mip) = 535{ var m = mip 536; m.STIP <- sip.STIP 537; m.SSIP <- sip.SSIP 538; m 539} 540 541mie lower_sie_mie(sie::sie, mie::mie) = 542{ var m = mie 543; m.STIE <- sie.STIE 544; m.SSIE <- sie.SSIE 545; m 546} 547 548mstatus update_mstatus(orig::mstatus, v::mstatus) = 549{ var mt = orig 550-- update privilege stack 551; mt.MIE <- v.MIE 552; mt.MPRV <- v.MPRV 553; mt.MIE1 <- v.MIE1 554; mt.MPRV1 <- v.MPRV1 555; mt.MIE2 <- v.MIE2 556; mt.MPRV2 <- v.MPRV2 557; mt.MIE3 <- v.MIE3 558; mt.MPRV3 <- v.MPRV3 559 560-- ensure a valid address translation mode 561; when isValidVM(v.VM) 562 do mt.VM <- v.VM 563; mt.MMPRV <- v.MMPRV 564 565-- update extension context status 566; mt.MFS <- v.MFS 567; mt.MXS <- v.MXS 568; mt.MSD <- extStatus(v.MXS) == Dirty or extStatus(v.MFS) == Dirty 569 570; mt 571} 572 573sstatus lift_mstatus_sstatus(mst::mstatus) = 574{ var st = sstatus(0) 575; st.SMPRV <- mst.MMPRV 576 577-- shared state 578; st.SXS <- mst.MXS 579; st.SFS <- mst.MFS 580; st.SSD <- extStatus(mst.MXS) == Dirty or extStatus(mst.MFS) == Dirty 581 582-- projected state 583; st.SPS <- not (privilege(mst.MPRV1) == User) 584; st.SPIE <- mst.MIE1 585; st.SIE <- mst.MIE 586 587; st 588} 589 590mstatus lower_sstatus_mstatus(sst::sstatus, mst::mstatus) = 591{ var mt = mstatus(&mst) 592 593; mt.MMPRV <- sst.SMPRV 594; mt.MXS <- sst.SXS 595; mt.MFS <- sst.SFS 596 597; mt.MPRV1 <- privLevel(if sst.SPS then Supervisor else User) 598; mt.MIE1 <- sst.SPIE 599; mt.MIE <- sst.SIE 600 601; update_mstatus(mst, mt) 602} 603 604-- pop the privilege stack for ERET 605mstatus popPrivilegeStack(mst::mstatus) = 606{ var st = mst 607; st.MIE <- mst.MIE1 608; st.MPRV <- mst.MPRV1 609; st.MIE1 <- mst.MIE2 610; st.MPRV1 <- mst.MPRV2 611; st.MIE2 <- true 612; st.MPRV2 <- privLevel(User) 613; st 614} 615 616mstatus pushPrivilegeStack(mst::mstatus, p::Privilege) = 617{ var st = mst 618; st.MIE2 <- mst.MIE1 619; st.MPRV2 <- mst.MPRV1 620; st.MIE1 <- mst.MIE 621; st.MPRV1 <- mst.MPRV 622; st.MIE <- false 623; st.MPRV <- privLevel(p) 624; st 625} 626 627--------------------------------------------------------------------------- 628-- Instruction fetch control 629--------------------------------------------------------------------------- 630 631record SynchronousTrap 632{ trap :: ExceptionType 633 badaddr :: vAddr option 634} 635 636construct TransferControl 637{ Trap :: SynchronousTrap 638, BranchTo :: regType 639, Ereturn 640, Mrts 641} 642 643--------------------------------------------------------------------------- 644-- Register state space 645--------------------------------------------------------------------------- 646 647-- Each register state is local to a core. 648 649type RegFile = reg -> regType 650 651declare 652{ clock :: regType -- global clock and counters 653 654 c_instret :: id -> regType -- per-core counters 655 c_cycles :: id -> regType 656 657 c_gpr :: id -> RegFile -- general purpose registers 658 c_fpr :: id -> RegFile -- floating-point registers 659 660 c_PC :: id -> regType -- program counter 661 c_Skip :: id -> regType -- bytes to next instruction 662 663 c_UCSR :: id -> UserCSR -- user-level CSRs 664 c_SCSR :: id -> SupervisorCSR -- supervisor-level CSRs 665 c_HCSR :: id -> HypervisorCSR -- hypervisor-level CSRs 666 c_MCSR :: id -> MachineCSR -- machine-level CSRs 667 668 -- interpreter execution context 669 c_NextFetch :: id -> TransferControl option 670 c_ReserveLoad :: id -> vAddr option -- load reservation for LL/SC 671 c_ExitCode :: id -> regType -- derived from Berkeley HTIF 672} 673 674-- Number of cores 675declare totalCore :: nat 676 677-- ID of the core executing current instruction 678declare procID :: id 679 680unit scheduleCore(id :: nat) = 681 when id < totalCore 682 do procID <- [id] 683 684-- The following components provide read/write access to state of the 685-- core whose id equals procID. For example, writing "gpr(r)" refers 686-- general purpose register "r" in the core whose id equals procID. 687 688component gpr(n::reg) :: regType 689{ value = { m = c_gpr(procID); m(n) } 690 assign value = { var m = c_gpr(procID) 691 ; m(n) <- value 692 ; c_gpr(procID) <- m 693 } 694} 695 696component fcsr :: FPCSR 697{ value = c_UCSR(procID).fpcsr 698 assign value = { c_UCSR(procID).fpcsr <- value 699 ; c_MCSR(procID).mstatus.MFS <- ext_status(Dirty) 700 ; c_MCSR(procID).mstatus.MSD <- true 701 } 702} 703 704component fpr(n::reg) :: regType 705{ value = { m = c_fpr(procID); m(n) } 706 assign value = { var m = c_fpr(procID) 707 ; m(n) <- value 708 ; c_fpr(procID) <- m 709 } 710} 711 712component PC :: regType 713{ value = c_PC(procID) 714 assign value = c_PC(procID) <- value 715} 716 717component Skip :: regType 718{ value = c_Skip(procID) 719 assign value = c_Skip(procID) <- value 720} 721 722component UCSR :: UserCSR 723{ value = c_UCSR(procID) 724 assign value = c_UCSR(procID) <- value 725} 726 727component SCSR :: SupervisorCSR 728{ value = c_SCSR(procID) 729 assign value = c_SCSR(procID) <- value 730} 731 732component HCSR :: HypervisorCSR 733{ value = c_HCSR(procID) 734 assign value = c_HCSR(procID) <- value 735} 736 737component MCSR :: MachineCSR 738{ value = c_MCSR(procID) 739 assign value = c_MCSR(procID) <- value 740} 741 742component NextFetch :: TransferControl option 743{ value = c_NextFetch(procID) 744 assign value = c_NextFetch(procID) <- value 745} 746 747component ReserveLoad :: vAddr option 748{ value = c_ReserveLoad(procID) 749 assign value = c_ReserveLoad(procID) <- value 750} 751 752component ExitCode :: regType 753{ value = c_ExitCode(procID) 754 assign value = c_ExitCode(procID) <- value 755} 756 757-- machine state utilities 758 759Architecture curArch() = 760 architecture(MCSR.mcpuid.ArchBase) 761 762bool in32BitMode() = 763 curArch() == RV32I 764 765Privilege curPrivilege() = 766 privilege(MCSR.mstatus.MPRV) 767 768regType curEPC() = 769 match curPrivilege() 770 { case User => #INTERNAL_ERROR("No EPC in U-mode") 771 case Supervisor => SCSR.sepc 772 case Hypervisor => HCSR.hepc 773 case Machine => MCSR.mepc 774 } 775 776unit sendIPI(core::regType) = 777{ id = [core]::id 778; when [id]::nat < totalCore 779 do c_MCSR(id).mip.MSIP <- true 780} 781 782--------------------------------------------------------------------------- 783-- Floating Point 784--------------------------------------------------------------------------- 785 786 787-- Rounding 788 789construct Rounding 790{ RNE, RTZ, RDN, RUP, RMM, RDYN } 791 792-- instruction rounding mode 793Rounding option rnd_mode_static(rnd::fprnd) = 794 match rnd 795 { case 0 => Some(RNE) 796 case 1 => Some(RTZ) 797 case 2 => Some(RDN) 798 case 3 => Some(RUP) 799 case 4 => Some(RMM) 800 case 7 => Some(RDYN) -- from rounding mode register 801 case _ => None 802 } 803 804-- dynamic rounding mode 805Rounding option rnd_mode_dynamic(rnd::fprnd) = 806 match rnd 807 { case 0 => Some(RNE) 808 case 1 => Some(RTZ) 809 case 2 => Some(RDN) 810 case 3 => Some(RUP) 811 case 4 => Some(RMM) 812 case _ => None 813 } 814 815-- currently implemented rounding modes 816ieee_rounding option l3round(rnd::Rounding) = 817 match rnd 818 { case RNE => Some(roundTiesToEven) 819 case RTZ => Some(roundTowardZero) 820 case RDN => Some(roundTowardNegative) 821 case RUP => Some(roundTowardPositive) 822 case RMM => None -- roundTiesToMaxMagnitude not in L3 823 case RDYN => None -- invalid 824 } 825 826-- composed rounding mode 827ieee_rounding option round(rnd::fprnd) = 828 match rnd_mode_static(rnd) 829 { case Some(RDYN) => match rnd_mode_dynamic(fcsr.FRM) 830 { case Some(frm) => l3round(frm) 831 case None => None 832 } 833 case Some(frm) => l3round(frm) 834 case None => None 835 } 836 837-- NaNs 838 839bits(32) RV32_CanonicalNan = 0x7fc00000 840bits(64) RV64_CanonicalNan = 0x7ff8000000000000 841 842-- Classification 843 844bool FP32_IsSignalingNan(x::bits(32)) = 845 (x<30:23> == 0xff`8) and x<22> == false and (x<21:0> != 0x0`22) 846 847bool FP64_IsSignalingNan(x::bits(64)) = 848 (x<62:52> == 0x7ff`11) and x<51> == false and (x<50:0> != 0x0`51) 849 850bool FP32_Sign(x::bits(32)) = x<31> 851bool FP64_Sign(x::bits(64)) = x<63> 852 853-- setting exception flags 854 855unit setFP_Invalid() = 856 fcsr.NV <- true 857 858unit setFP_DivZero() = 859 fcsr.DZ <- true 860 861unit setFP_Overflow() = 862 fcsr.OF <- true 863 864unit setFP_Underflow() = 865 fcsr.OF <- true 866 867unit setFP_Inexact() = 868 fcsr.OF <- true 869 870--------------------------------------------------------------------------- 871-- CSR Register address map 872--------------------------------------------------------------------------- 873 874-- CSR access control 875 876type csrRW = bits(2) -- read/write check 877type csrPR = bits(2) -- privilege check 878 879csrRW csrRW(csr::creg) = csr<11:10> 880csrPR csrPR(csr::creg) = csr<9:8> 881 882-- this only checks register-level access. some registers have 883-- additional bit-specific read/write controls. 884bool check_CSR_access(rw::csrRW, pr::csrPR, p::Privilege, a::accessType) = 885 (a == Read or rw != 0b11) and (privLevel(p) >=+ pr) 886 887-- XXX: Revise this to handle absence of counter regs in RV32E. 888bool is_CSR_defined(csr::creg) = 889 -- user-mode 890 (csr >= 0x001 and csr <= 0x003) 891 or (csr >= 0xC00 and csr <= 0xC02) 892 or (csr >= 0xC80 and csr <= 0xC82 and in32BitMode()) 893 894 -- supervisor-mode 895 or (csr >= 0x100 and csr <= 0x101) 896 or csr == 0x104 or csr == 0x121 897 898 or csr == 0xD01 or (csr == 0xD81 and in32BitMode()) 899 900 or (csr >= 0x140 and csr <= 0x141) or csr == 0x144 901 or (csr >= 0xD42 and csr <= 0xD43) 902 903 or (csr >= 0x180 and csr <= 0x181) 904 905 or (csr >= 0x900 and csr <= 0x902) 906 or (csr >= 0x980 and csr <= 0x982 and in32BitMode()) 907 908 -- machine-mode 909 or (csr >= 0xF00 and csr <= 0xF01) or csr == 0xF10 910 or (csr >= 0x300 and csr <= 0x302) or csr == 0x304 or csr == 0x321 911 or csr == 0x701 or (csr == 0x741 and in32BitMode()) 912 or (csr >= 0x340 and csr <= 0x344) 913 or (csr >= 0x380 and csr <= 0x385) 914 or csr >= 0xB01 or (csr == 0xB81 and in32BitMode()) 915 or (csr >= 0x780 and csr <= 0x783 and csr != 0x782) 916 917--- XXX: the CSRMap below is broken in 32-bit mode, since we need to 918--- convert from 64-bit regType to 32-bit XLEN. 919component CSRMap(csr::creg) :: regType 920{ 921 value = 922 match csr 923 { -- user floating-point context 924 case 0x001 => ZeroExtend(c_UCSR(procID).&fpcsr<4:0>) 925 case 0x002 => ZeroExtend(c_UCSR(procID).fpcsr.FRM) 926 case 0x003 => ZeroExtend(c_UCSR(procID).&fpcsr<7:0>) 927 928 -- user counter/timers 929 case 0xC00 => c_cycles(procID) + c_UCSR(procID).cycle_delta 930 case 0xC01 => clock + c_UCSR(procID).time_delta 931 case 0xC02 => c_instret(procID) + c_UCSR(procID).instret_delta 932 case 0xC80 => SignExtend((c_cycles(procID) + c_UCSR(procID).cycle_delta)<63:32>) 933 case 0xC81 => SignExtend((clock + c_UCSR(procID).time_delta)<63:32>) 934 case 0xC82 => SignExtend((c_instret(procID) + c_UCSR(procID).instret_delta)<63:32>) 935 936 -- supervisor trap setup 937 case 0x100 => &lift_mstatus_sstatus(c_MCSR(procID).mstatus) 938 case 0x101 => c_SCSR(procID).stvec 939 case 0x104 => &lift_mie_sie(c_MCSR(procID).mie) 940 case 0x121 => c_SCSR(procID).stimecmp 941 942 -- supervisor timer 943 case 0xD01 => clock + c_SCSR(procID).stime_delta 944 case 0xD81 => SignExtend((clock + c_SCSR(procID).stime_delta)<63:32>) 945 946 -- supervisor trap handling 947 case 0x140 => c_SCSR(procID).sscratch 948 case 0x141 => c_SCSR(procID).sepc 949 case 0xD42 => c_SCSR(procID).&scause 950 case 0xD43 => c_SCSR(procID).sbadaddr 951 case 0x144 => &lift_mip_sip(c_MCSR(procID).mip) 952 953 -- supervisor protection and translation 954 case 0x180 => c_SCSR(procID).sptbr 955 case 0x181 => c_SCSR(procID).sasid 956 957 -- supervisor read/write shadow of user read-only registers 958 case 0x900 => c_cycles(procID) + c_UCSR(procID).cycle_delta 959 case 0x901 => clock + c_UCSR(procID).time_delta 960 case 0x902 => c_instret(procID) + c_UCSR(procID).instret_delta 961 case 0x980 => SignExtend((c_cycles(procID) + c_UCSR(procID).cycle_delta)<63:32>) 962 case 0x981 => SignExtend((clock + c_UCSR(procID).time_delta)<63:32>) 963 case 0x982 => SignExtend((c_instret(procID) + c_UCSR(procID).instret_delta)<63:32>) 964 965 -- hypervisor trap setup 966 case 0x200 => c_HCSR(procID).&hstatus 967 case 0x201 => c_HCSR(procID).htvec 968 case 0x202 => c_HCSR(procID).&htdeleg 969 case 0x221 => c_HCSR(procID).htimecmp 970 971 -- hypervisor timer 972 case 0xE01 => clock + c_HCSR(procID).htime_delta 973 case 0xE81 => SignExtend((clock + c_HCSR(procID).htime_delta)<63:32>) 974 975 -- hypervisor trap handling 976 case 0x240 => c_HCSR(procID).hscratch 977 case 0x241 => c_HCSR(procID).hepc 978 case 0x242 => c_HCSR(procID).&hcause 979 case 0x243 => c_HCSR(procID).hbadaddr 980 981 -- hypervisor read/write shadow of supervisor read-only registers 982 case 0xA01 => clock + c_SCSR(procID).stime_delta 983 case 0xA81 => SignExtend((clock + c_SCSR(procID).stime_delta)<63:32>) 984 985 -- machine information registers 986 case 0xF00 => c_MCSR(procID).&mcpuid 987 case 0xF01 => c_MCSR(procID).&mimpid 988 case 0xF10 => c_MCSR(procID).mhartid 989 990 -- machine trap setup 991 case 0x300 => c_MCSR(procID).&mstatus 992 case 0x301 => c_MCSR(procID).mtvec 993 case 0x302 => c_MCSR(procID).&mtdeleg 994 case 0x304 => c_MCSR(procID).&mie 995 case 0x321 => c_MCSR(procID).mtimecmp 996 997 -- machine timers and counters 998 case 0x701 => clock + c_MCSR(procID).mtime_delta 999 case 0x741 => SignExtend((clock + c_MCSR(procID).mtime_delta)<63:32>) 1000 1001 -- machine trap handling 1002 case 0x340 => c_MCSR(procID).mscratch 1003 case 0x341 => c_MCSR(procID).mepc 1004 case 0x342 => c_MCSR(procID).&mcause 1005 case 0x343 => c_MCSR(procID).mbadaddr 1006 case 0x344 => c_MCSR(procID).&mip 1007 1008 -- machine protection and translation 1009 case 0x380 => c_MCSR(procID).mbase 1010 case 0x381 => c_MCSR(procID).mbound 1011 case 0x382 => c_MCSR(procID).mibase 1012 case 0x383 => c_MCSR(procID).mibound 1013 case 0x384 => c_MCSR(procID).mdbase 1014 case 0x385 => c_MCSR(procID).mdbound 1015 1016 -- machine read-write shadow of hypervisor read-only registers 1017 case 0xB01 => clock + c_HCSR(procID).htime_delta 1018 case 0xB81 => SignExtend((clock + c_HCSR(procID).htime_delta)<63:32>) 1019 1020 -- machine host-target interface (berkeley extension) 1021 case 0x780 => c_MCSR(procID).mtohost 1022 case 0x781 => c_MCSR(procID).mfromhost 1023 case 0x783 => 0 1024 1025 case _ => #UNDEFINED("unexpected CSR read at " : [csr]) 1026 } 1027 1028 assign value = 1029 match csr 1030 { -- user floating-point context 1031 case 0x001 => { c_UCSR(procID).&fpcsr<4:0> <- value<4:0> 1032 ; c_MCSR(procID).mstatus.MFS <- ext_status(Dirty) 1033 ; c_MCSR(procID).mstatus.MSD <- true 1034 } 1035 case 0x002 => { c_UCSR(procID).fpcsr.FRM <- value<2:0> 1036 ; c_MCSR(procID).mstatus.MFS <- ext_status(Dirty) 1037 ; c_MCSR(procID).mstatus.MSD <- true 1038 } 1039 case 0x003 => { c_UCSR(procID).&fpcsr <- value<31:0> 1040 ; c_MCSR(procID).mstatus.MFS <- ext_status(Dirty) 1041 ; c_MCSR(procID).mstatus.MSD <- true 1042 } 1043 -- user counters/timers are URO 1044 1045 -- supervisor trap setup 1046 case 0x100 => c_MCSR(procID).mstatus <- lower_sstatus_mstatus(sstatus(value), 1047 c_MCSR(procID).mstatus) 1048 1049 case 0x101 => c_SCSR(procID).stvec <- value 1050 -- sie back-projects to mie 1051 case 0x104 => c_MCSR(procID).mie <- lower_sie_mie(sie(value), c_MCSR(procID).mie) 1052 case 0x121 => 1053 { c_SCSR(procID).stimecmp <- value 1054 ; c_MCSR(procID).mip.STIP <- false 1055 } 1056 1057 -- supervisor trap handling 1058 case 0x140 => c_SCSR(procID).sscratch <- value 1059 case 0x141 => c_SCSR(procID).sepc <- (value && SignExtend(0b100`3)) -- no 16-bit instr support 1060 -- scause, sbadaddr are SRO 1061 -- sip back-projects to mip 1062 case 0x144 => c_MCSR(procID).mip <- lower_sip_mip(sip(value), c_MCSR(procID).mip) 1063 1064 -- supervisor protection and translation 1065 case 0x180 => c_SCSR(procID).sptbr <- value 1066 case 0x181 => c_SCSR(procID).sasid <- value 1067 1068 -- supervisor read/write shadow of user read-only registers 1069 case 0x900 => c_UCSR(procID).cycle_delta <- value - c_cycles(procID) 1070 case 0x901 => c_UCSR(procID).time_delta <- value - clock 1071 case 0x902 => c_UCSR(procID).instret_delta <- value - c_instret(procID) 1072 1073 case 0x980 => c_UCSR(procID).cycle_delta<63:32> <- (value<31:0> - c_cycles(procID)<63:32>) << 32 1074 case 0x981 => c_UCSR(procID).time_delta<63:32> <- (value<31:0> - clock<63:32>) << 32 1075 case 0x982 => c_UCSR(procID).instret_delta<63:32> <- (value<31:0> - c_instret(procID)<63:32>) << 32 1076 1077 -- TODO: hypervisor register write support 1078 1079 -- machine information registers are MRO 1080 1081 -- machine trap setup 1082 case 0x300 => c_MCSR(procID).mstatus <- update_mstatus(c_MCSR(procID).mstatus, mstatus(value)) 1083 case 0x301 => c_MCSR(procID).mtvec <- value 1084 case 0x302 => c_MCSR(procID).mtdeleg <- mtdeleg(value) 1085 case 0x304 => c_MCSR(procID).mie <- mie(value) 1086 case 0x321 => 1087 { c_MCSR(procID).mtimecmp <- value 1088 ; c_MCSR(procID).mip.MTIP <- false 1089 } 1090 1091 -- machine timers and counters 1092 case 0x701 => c_MCSR(procID).mtime_delta <- value - clock 1093 case 0x741 => c_MCSR(procID).mtime_delta<63:32> <- (value<31:0> - clock<63:32>) << 32 1094 1095 -- machine trap handling 1096 case 0x340 => c_MCSR(procID).mscratch <- value 1097 case 0x341 => c_MCSR(procID).mepc <- (value && SignExtend(0b100`3)) -- no 16-bit instr support 1098 case 0x342 => c_MCSR(procID).mcause <- mcause(value) 1099 case 0x343 => c_MCSR(procID).mbadaddr <- value 1100 case 0x344 => c_MCSR(procID).mip <- mip(value) 1101 1102 -- machine protection and translation 1103 case 0x380 => c_MCSR(procID).mbase <- value 1104 case 0x381 => c_MCSR(procID).mbound <- value 1105 case 0x382 => c_MCSR(procID).mibase <- value 1106 case 0x383 => c_MCSR(procID).mibound <- value 1107 case 0x384 => c_MCSR(procID).mdbase <- value 1108 case 0x385 => c_MCSR(procID).mdbound <- value 1109 1110 -- machine read-write shadow of hypervisor read-only registers 1111 case 0xB01 => c_HCSR(procID).htime_delta <- value - clock 1112 case 0xB81 => c_HCSR(procID).htime_delta<63:32> <- (value<31:0> - clock<63:32>) << 32 1113 1114 -- machine host-target interface (berkeley extension) 1115 -- TODO: XXX: set I/O pending bit 1116 case 0x780 => 1117 { c_MCSR(procID).mtohost <- value } 1118 case 0x781 => 1119 { c_MCSR(procID).mfromhost <- value } 1120 case 0x783 => 1121 { sendIPI(value) } 1122 1123 case _ => #INTERNAL_ERROR("unexpected CSR write to " : [csr]) 1124 } 1125} 1126 1127string csrName(csr::creg) = 1128 match csr 1129 { -- user floating-point context 1130 case 0x001 => "fflags" 1131 case 0x002 => "frm" 1132 case 0x003 => "fcsr" 1133 1134 -- user counter/timers 1135 case 0xC00 => "cycle" 1136 case 0xC01 => "time" 1137 case 0xC02 => "instret" 1138 case 0xC80 => "cycleh" 1139 case 0xC81 => "timeh" 1140 case 0xC82 => "instreth" 1141 1142 -- supervisor trap setup 1143 case 0x100 => "sstatus" 1144 case 0x101 => "stvec" 1145 case 0x104 => "sie" 1146 case 0x121 => "stimecmp" 1147 1148 -- supervisor timer 1149 case 0xD01 => "stime" 1150 case 0xD81 => "stimeh" 1151 1152 -- supervisor trap handling 1153 case 0x140 => "sscratch" 1154 case 0x141 => "sepc" 1155 case 0xD42 => "scause" 1156 case 0xD43 => "sbadaddr" 1157 case 0x144 => "mip" 1158 1159 -- supervisor protection and translation 1160 case 0x180 => "sptbr" 1161 case 0x181 => "sasid" 1162 1163 -- supervisor read/write shadow of user read-only registers 1164 case 0x900 => "cycle" 1165 case 0x901 => "time" 1166 case 0x902 => "instret" 1167 case 0x980 => "cycleh" 1168 case 0x981 => "timeh" 1169 case 0x982 => "instreth" 1170 1171 -- hypervisor trap setup 1172 case 0x200 => "hstatus" 1173 case 0x201 => "htvec" 1174 case 0x202 => "htdeleg" 1175 case 0x221 => "htimecmp" 1176 1177 -- hypervisor timer 1178 case 0xE01 => "htime" 1179 case 0xE81 => "htimeh" 1180 1181 -- hypervisor trap handling 1182 case 0x240 => "hscratch" 1183 case 0x241 => "hepc" 1184 case 0x242 => "hcause" 1185 case 0x243 => "hbadaddr" 1186 1187 -- hypervisor read/write shadow of supervisor read-only registers 1188 case 0xA01 => "stime" 1189 case 0xA81 => "stimeh" 1190 1191 -- machine information registers 1192 case 0xF00 => "mcpuid" 1193 case 0xF01 => "mimpid" 1194 case 0xF10 => "mhartid" 1195 1196 -- machine trap setup 1197 case 0x300 => "mstatus" 1198 case 0x301 => "mtvec" 1199 case 0x302 => "mtdeleg" 1200 case 0x304 => "mie" 1201 case 0x321 => "mtimecmp" 1202 1203 -- machine timers and counters 1204 case 0x701 => "mtime" 1205 case 0x741 => "mtimeh" 1206 1207 -- machine trap handling 1208 case 0x340 => "mscratch" 1209 case 0x341 => "mepc" 1210 case 0x342 => "mcause" 1211 case 0x343 => "mbadaddr" 1212 case 0x344 => "mip" 1213 1214 -- machine protection and translation 1215 case 0x380 => "mbase" 1216 case 0x381 => "mbound" 1217 case 0x382 => "mibase" 1218 case 0x383 => "mibound" 1219 case 0x384 => "mdbase" 1220 case 0x385 => "mdbound" 1221 1222 -- machine read-write shadow of hypervisor read-only registers 1223 case 0xB01 => "htime" 1224 case 0xB81 => "htimeh" 1225 1226 -- machine host-target interface (berkeley extension) 1227 case 0x780 => "mtohost" 1228 case 0x781 => "mfromhost" 1229 1230 case 0x783 => "send_ipi" 1231 1232 case _ => "UNKNOWN" 1233 } 1234 1235--------------------------------------------------------------------------- 1236-- Tandem verification 1237--------------------------------------------------------------------------- 1238-- This describes the state update due to every retired instruction, 1239-- which can be verified against an external oracle. Currently, the 1240-- Cissr tool from Bluespec fills the role, and the record below is 1241-- designed against its API. 1242 1243record StateDelta 1244{ exc_taken :: bool -- whether an exception (interrupt/trap) was taken 1245 fetch_exc :: bool -- whether that exception occured on fetch 1246 -- if so, the retired instruction (rinstr) is undefined 1247 pc :: regType -- PC of retired instruction 1248 rinstr :: rawInstType -- the retired instruction 1249 1250 addr :: regType option -- address argument for instruction: 1251 -- new control flow target for jump, exception branch, ERET 1252 -- memory address for memory ops and AMOs 1253 -- CSR register address for CSR instructions 1254 1255 data1 :: regType option -- data result for instruction: 1256 -- new value for rd for ALU ops, LOAD, LOAD_FP, LR, SC, CSR ops 1257 -- new csr_status for exceptions and ERET 1258 1259 data2 :: regType option -- data argument for instruction: 1260 -- new csr_cause for exceptions 1261 -- new memory value for STORE, STORE_FP, SC, AMOs 1262 -- argument for CSR ops 1263 1264 fp_data :: fpval option -- floating point value 1265 1266 st_width :: word option -- width of store (optimization for sub-word store checks) 1267} 1268 1269declare c_update :: id -> StateDelta 1270 1271component Delta :: StateDelta 1272{ value = c_update(procID) 1273 assign value = c_update(procID) <- value 1274} 1275 1276inline unit setupDelta(pc::regType, instr::rawInstType) = 1277{ Delta.exc_taken <- false 1278; Delta.fetch_exc <- false 1279; Delta.pc <- pc 1280; Delta.rinstr <- instr 1281; Delta.addr <- None 1282; Delta.data1 <- None 1283; Delta.data2 <- None 1284; Delta.fp_data <- None 1285; Delta.st_width <- None 1286} 1287 1288inline unit recordLoad(addr::vAddr, val::regType) = 1289when not PROVER_EXPORT do 1290{ Delta.addr <- Some(addr) 1291; Delta.data1 <- Some(val) 1292} 1293 1294inline unit recordStore(addr::vAddr, val::regType, width::word) = 1295when not PROVER_EXPORT do 1296{ Delta.addr <- Some(addr) 1297; Delta.data2 <- Some(val) 1298; Delta.st_width <- Some(width) 1299} 1300 1301inline unit recordException() = 1302when not PROVER_EXPORT do 1303{ Delta.exc_taken <- true } 1304 1305inline unit recordFetchException(pc::regType) = 1306when not PROVER_EXPORT do 1307{ Delta.fetch_exc <- true 1308; Delta.pc <- pc 1309} 1310 1311--------------------------------------------------------------------------- 1312-- Logging 1313--------------------------------------------------------------------------- 1314string hex32(x::word) = PadLeft(#"0", 8, [x]) 1315string hex64(x::dword) = PadLeft(#"0", 16, [x]) 1316 1317string log_w_csr(csr::creg, data::regType) = 1318 "CSR (" : csrName(csr) : ") <- 0x" : hex64(data) 1319 1320string reg(r::reg) = 1321{ if r == 0 then "$0" 1322 else if r == 1 then "ra" 1323 else if r == 2 then "sp" 1324 else if r == 3 then "gp" 1325 else if r == 4 then "tp" 1326 else if r == 5 then "t0" 1327 else if r == 6 then "t1" 1328 else if r == 7 then "t2" 1329 else if r == 8 then "fp" 1330 else if r == 9 then "s1" 1331 else if r == 10 then "a0" 1332 else if r == 11 then "a1" 1333 else if r == 12 then "a2" 1334 else if r == 13 then "a3" 1335 else if r == 14 then "a4" 1336 else if r == 15 then "a5" 1337 else if r == 16 then "a6" 1338 else if r == 17 then "a7" 1339 else if r == 18 then "s2" 1340 else if r == 19 then "s3" 1341 else if r == 20 then "s4" 1342 else if r == 21 then "s5" 1343 else if r == 22 then "s6" 1344 else if r == 23 then "s7" 1345 else if r == 24 then "s8" 1346 else if r == 25 then "s9" 1347 else if r == 26 then "s10" 1348 else if r == 27 then "s11" 1349 else if r == 28 then "t3" 1350 else if r == 29 then "t4" 1351 else if r == 30 then "t5" 1352 else "t6" 1353} 1354 1355string fpreg(r::reg) = 1356{ if r == 0 then "fs0" 1357 else if r == 1 then "fs1" 1358 else if r == 2 then "fs2" 1359 else if r == 3 then "fs3" 1360 else if r == 4 then "fs4" 1361 else if r == 5 then "fs5" 1362 else if r == 6 then "fs6" 1363 else if r == 7 then "fs7" 1364 else if r == 8 then "fs8" 1365 else if r == 9 then "fs9" 1366 else if r == 10 then "fs10" 1367 else if r == 11 then "fs11" 1368 else if r == 12 then "fs12" 1369 else if r == 13 then "fs13" 1370 else if r == 14 then "fs14" 1371 else if r == 15 then "fs15" 1372 else if r == 16 then "fv0" 1373 else if r == 17 then "fv1" 1374 else if r == 18 then "fa0" 1375 else if r == 19 then "fa1" 1376 else if r == 20 then "fa2" 1377 else if r == 21 then "fa3" 1378 else if r == 22 then "fa4" 1379 else if r == 23 then "fa5" 1380 else if r == 24 then "fa6" 1381 else if r == 25 then "fa7" 1382 else if r == 26 then "ft0" 1383 else if r == 27 then "ft1" 1384 else if r == 28 then "ft2" 1385 else if r == 29 then "ft3" 1386 else if r == 30 then "ft4" 1387 else "ft5" 1388} 1389 1390string log_w_gpr(r::reg, data::regType) = 1391 "Reg " : reg(r) : " (" : [[r]::nat] : ") <- 0x" : hex64(data) 1392 1393string log_w_fprs(r::reg, data::word) = 1394 "FPR " : reg(r) : " (" : [[r]::nat] : ") <- 0x" : hex32(data) 1395 1396string log_w_fprd(r::reg, data::regType) = 1397 "FPR " : reg(r) : " (" : [[r]::nat] : ") <- 0x" : hex64(data) 1398 1399string log_w_mem_mask(pAddrIdx::pAddrIdx, vAddr::vAddr, mask::regType, 1400 data::regType, old::regType, new::regType) = 1401 "MEM[0x" : hex64([pAddrIdx]) : "/" : hex64(vAddr) : 1402 "] <- (data: 0x" : hex64(data) : ", mask: 0x" : hex64(mask) : 1403 ", old: 0x" : hex64(old) : ", new: 0x" : hex64(new) : ")" 1404 1405string log_w_mem_mask_misaligned(pAddrIdx::pAddrIdx, vAddr::vAddr, mask::regType, 1406 data::regType, align::nat, old::regType, new::regType) = 1407 "MEM[0x" : hex64([pAddrIdx]) : "/" : hex64(vAddr) : "/ misaligned@" : [align] : 1408 "] <- (data: 0x" : hex64(data) : ", mask: 0x" : hex64(mask) : 1409 ", old: 0x" : hex64(old) : ", new: 0x" : hex64(new) : ")" 1410 1411string log_w_mem(pAddrIdx::pAddrIdx, vAddr::vAddr, data::regType) = 1412 "MEM[0x" : hex64([pAddrIdx]) : "/" : hex64(vAddr) : 1413 "] <- (data: 0x" : hex64(data) : ")" 1414 1415string log_r_mem(pAddrIdx::pAddrIdx, vAddr::vAddr, data::regType) = 1416 "data <- MEM[0x" : PadLeft(#"0", 10, [pAddrIdx]) : "/" : hex64(vAddr) : 1417 "]: 0x" : hex64(data) 1418 1419string log_exc(e::ExceptionType) = 1420 " Exception " : excName(e) : " raised!" 1421 1422string log_tohost(tohost::regType) = 1423 "-> host: " : [[tohost<7:0>]::char] 1424 1425inline nat LOG_IO = 0 1426inline nat LOG_INSN = 1 1427inline nat LOG_REG = 2 1428inline nat LOG_MEM = 3 1429inline nat LOG_ADDRTR = 4 1430 1431declare log :: (nat * string) list 1432 1433inline unit mark_log(lvl::nat, s::string) = 1434 when not PROVER_EXPORT do log <- (lvl, s) @ log 1435 1436unit clear_logs() = log <- Nil 1437 1438--------------------------------------------------------------------------- 1439-- Exception and Interrupt processing 1440--------------------------------------------------------------------------- 1441 1442-- Signalled exceptions are recorded as traps. 1443 1444unit setTrap(e::ExceptionType, badaddr::vAddr option) = 1445{ var trap 1446; trap.trap <- e 1447; trap.badaddr <- badaddr 1448; NextFetch <- Some(Trap(trap)) 1449} 1450 1451unit signalException(e::ExceptionType) = 1452{ mark_log(LOG_INSN, "signalling exception " : excName(e)) 1453; setTrap(e, None) 1454; recordException() 1455} 1456 1457unit signalAddressException(e::ExceptionType, vAddr::vAddr) = 1458{ mark_log(LOG_INSN, "signalling address exception " : excName(e) : " at " : [vAddr]) 1459; setTrap(e, Some(vAddr)) 1460; recordException() 1461} 1462 1463unit signalEnvCall() = 1464{ e = match privilege(MCSR.mstatus.MPRV) 1465 { case User => UMode_Env_Call 1466 case Supervisor => SMode_Env_Call 1467 case Hypervisor => HMode_Env_Call 1468 case Machine => MMode_Env_Call 1469 } 1470; signalException(e) 1471} 1472 1473-- Delegation logic. 1474 1475Privilege checkDelegation(curPriv::Privilege, intr::bool, ec::exc_code) 1476 HOL "checkDelegation.sml" measure [curPriv] = 1477{ e = [ec]::nat 1478; match curPriv 1479 { case User => #INTERNAL_ERROR("No user-level delegation!") 1480 case Supervisor => #INTERNAL_ERROR("No supervisor-level delegation!") 1481 case Hypervisor => 1482 if ((intr and HCSR.htdeleg.Intr_deleg<e>) 1483 or (!intr and HCSR.htdeleg.Exc_deleg<e>)) 1484 then Supervisor else curPriv 1485 case Machine => 1486 if ((intr and MCSR.mtdeleg.Intr_deleg<e>) 1487 or (!intr and MCSR.mtdeleg.Exc_deleg<e>)) 1488 then checkDelegation(Hypervisor, intr, ec) else curPriv 1489 } 1490} 1491 1492-- The spec doesn't define a priority between a timer interrupt and a 1493-- software interrupt. We treat timer interrupts at higher priority. 1494 1495(Interrupt * Privilege) option checkPrivInterrupt(curPriv::Privilege) = 1496{ ip = MCSR.mip 1497; ie = MCSR.mie 1498; match curPriv 1499 { case User => #INTERNAL_ERROR("No user-level interrupts!") 1500 case Supervisor => if ip.STIP and ie.STIE then Some(Timer, curPriv) 1501 else if ip.SSIP and ie.SSIE then Some(Software, curPriv) 1502 else None 1503 case Hypervisor => if ip.HTIP and ie.HTIE then Some(Timer, curPriv) 1504 else if ip.HSIP and ie.HSIE then Some(Software, curPriv) 1505 else None 1506 case Machine => if ip.MTIP and ie.MTIE then Some(Timer, curPriv) 1507 else if ip.MSIP and ie.MSIE then Some(Software, curPriv) 1508 else None 1509 } 1510} 1511 1512-- The spec says: 1513-- 1514-- When a hart is running in a given privileged mode, interrupts 1515-- for higher privileged modes are always enabled while interrupts 1516-- for lower privileged modes are always disabled. 1517-- Higher-privilege-level code can use separate per-interrupt 1518-- enable bits to disable selected interrupts before ceding control 1519-- to a lower privilege level. 1520-- 1521-- This is critical to ensuring the monotonically non-decreasing 1522-- privilege levels in the privilege stack. 1523 1524(Interrupt * Privilege) option checkInterrupts() = 1525{ curIE = MCSR.mstatus.MIE -- if interrupts are enabled at curPrivilege 1526; p = curPrivilege() 1527; match p 1528 { case User or Supervisor => 1529 match checkPrivInterrupt(Machine) 1530 { case None => 1531 { match checkPrivInterrupt(Hypervisor) 1532 { case None => -- Always check S-mode interrupts in U-mode 1533 if p == User or curIE 1534 then checkPrivInterrupt(Supervisor) else None 1535 case i => i 1536 } 1537 } 1538 case i => i 1539 } 1540 case Hypervisor => 1541 match checkPrivInterrupt(Machine) 1542 { case None => if curIE then checkPrivInterrupt(Hypervisor) else None 1543 case i => i 1544 } 1545 case Machine => 1546 if curIE then checkPrivInterrupt(Machine) else None 1547 } 1548} 1549 1550unit takeTrap(intr::bool, ec::exc_code, epc::regType, badaddr::vAddr option, toPriv::Privilege) = 1551{ fromP = curPrivilege() 1552; mark_log(LOG_INSN, ["trapping from " : privName(fromP) : " to " : privName(toPriv) : 1553 " at pc " : [epc] : (if intr then " [intr] " else " [exc] ") : [[ec]::nat]]) 1554 1555; ReserveLoad <- None -- cancel any load reservation 1556; MCSR.mstatus.MMPRV <- false -- unset MPRV in each privilege level 1557 1558; MCSR.mstatus <- pushPrivilegeStack(MCSR.mstatus, toPriv) 1559 1560; match toPriv 1561 { case User => #INTERNAL_ERROR("Illegal trap to U-mode") 1562 case Supervisor => 1563 { SCSR.scause.Int <- intr 1564 ; SCSR.scause.EC <- ec 1565 ; SCSR.sepc <- epc 1566 ; when IsSome(badaddr) 1567 do SCSR.sbadaddr <- ValOf(badaddr) 1568 1569 ; PC <- SCSR.stvec 1570 } 1571 case Hypervisor => #INTERNAL_ERROR("Unsupported trap to H-mode") 1572 case Machine => 1573 { MCSR.mcause.Int <- intr 1574 ; MCSR.mcause.EC <- ec 1575 ; MCSR.mepc <- epc 1576 ; when IsSome(badaddr) 1577 do MCSR.mbadaddr <- ValOf(badaddr) 1578 1579 ; PC <- MCSR.mtvec + ([privLevel(fromP)]::regType) * 0x40 1580 } 1581 } 1582} 1583 1584--------------------------------------------------------------------------- 1585-- CSR access with logging 1586--------------------------------------------------------------------------- 1587 1588component CSR(n::creg) :: regType 1589{ value = CSRMap(n) 1590 assign value = { CSRMap(n) <- value 1591 ; mark_log(LOG_REG, log_w_csr(n, value)) 1592 } 1593} 1594 1595unit writeCSR(csr::creg, val::regType) = 1596{ CSR(csr) <- val; 1597 Delta.addr <- Some(ZeroExtend(csr)); 1598 Delta.data2 <- Some(CSR(csr)) -- Note that writes to CSR are intercepted 1599 -- and controlled by CSRMap, so we need to 1600 -- use what was finally written to the 1601 -- CSR, and not val itself. 1602} 1603 1604--------------------------------------------------------------------------- 1605-- GPR/FPR access with logging 1606--------------------------------------------------------------------------- 1607 1608component GPR(n::reg) :: regType 1609{ value = if n == 0 then 0 else gpr(n) 1610 assign value = when n <> 0 1611 do { gpr(n) <- value 1612 ; mark_log(LOG_REG, log_w_gpr(n, value)) 1613 } 1614} 1615 1616inline unit writeRD(rd::reg, val::regType) = 1617{ GPR(rd) <- val 1618; when not PROVER_EXPORT do Delta.data1 <- Some(val) 1619} 1620 1621component FPRS(n::reg) :: word 1622{ value = fpr(n)<31:0> 1623 assign value = { fpr(n)<31:0> <- value 1624 ; mark_log(LOG_REG, log_w_fprs(n, value)) 1625 } 1626} 1627 1628component FPRD(n::reg) :: regType 1629{ value = fpr(n) 1630 assign value = { fpr(n) <- value 1631 ; mark_log(LOG_REG, log_w_fprd(n, value)) 1632 } 1633} 1634 1635unit writeFPRS(rd::reg, val::word) = 1636{ FPRS(rd) <- val 1637; MCSR.mstatus.MFS <- ext_status(Dirty) 1638; MCSR.mstatus.MSD <- true 1639; Delta.data1 <- Some(ZeroExtend(val)) 1640} 1641 1642unit writeFPRD(rd::reg, val::regType) = 1643{ FPRD(rd) <- val 1644; MCSR.mstatus.MFS <- ext_status(Dirty) 1645; MCSR.mstatus.MSD <- true 1646; Delta.data1 <- Some(val) 1647} 1648 1649--------------------------------------------------------------------------- 1650-- Raw memory access 1651--------------------------------------------------------------------------- 1652 1653{- Original memory replaced by byte memory when exporting to HOL 1654declare MEM :: pAddrIdx -> regType -- raw memory, laid out in blocks 1655 -- of (|pAddr|-|pAddrIdx|) bits 1656 1657unit initMem(val::regType) = 1658 MEM <- InitMap(val) 1659-} 1660 1661declare MEM8 :: pAddr -> byte 1662 1663component MEM (a::pAddrIdx) :: regType 1664{ 1665 value = 1666 { b = [a] << 3 1667 ; ( MEM8 (b + 7) : MEM8 (b + 6) : MEM8 (b + 5) : MEM8 (b + 4) : 1668 MEM8 (b + 3) : MEM8 (b + 2) : MEM8 (b + 1) : MEM8 (b) ) 1669 } 1670 assign val = 1671 { b = [a] << 3 1672 ; MEM8 (b + 7) <- val<63:56> 1673 ; MEM8 (b + 6) <- val<55:48> 1674 ; MEM8 (b + 5) <- val<47:40> 1675 ; MEM8 (b + 4) <- val<39:32> 1676 ; MEM8 (b + 3) <- val<31:24> 1677 ; MEM8 (b + 2) <- val<23:16> 1678 ; MEM8 (b + 1) <- val<15:8 > 1679 ; MEM8 (b ) <- val<7 :0 > 1680 } 1681} 1682 1683regType rawReadData(pAddr::pAddr) = 1684{ pAddrIdx = pAddr<63:3> 1685; align = [pAddr<2:0>]::nat 1686; if align == 0 -- aligned read 1687 then { data = MEM(pAddrIdx) 1688 ; mark_log(LOG_MEM, log_r_mem(pAddrIdx, pAddr, data)) 1689 ; data 1690 } 1691 else { dw0 = MEM(pAddrIdx) 1692 ; dw1 = MEM(pAddrIdx+1) 1693 ; ddw = (dw1 : dw0) >> (align * 8) 1694 ; data = ddw<63:0> 1695 ; mark_log(LOG_MEM, log_r_mem(pAddrIdx, pAddr, dw0)) 1696 ; mark_log(LOG_MEM, log_r_mem(pAddrIdx+1, pAddr, dw1)) 1697 ; mark_log(LOG_MEM, log_r_mem(pAddrIdx, pAddr, data)) 1698 ; data 1699 } 1700} 1701 1702unit rawWriteData(pAddr::pAddr, data::regType, nbytes::nat) = 1703{ mask = ([ZeroExtend(1`1)::regType] << (nbytes * 8)) - 1 1704; pAddrIdx = pAddr<63:3> 1705; align = [pAddr<2:0>] :: nat 1706; old = MEM(pAddrIdx) 1707 1708; mark_log(LOG_MEM, log_r_mem(pAddrIdx, pAddr, old)) 1709 1710; if align == 0 -- aligned write 1711 then { new = old && ~mask || data && mask 1712 ; MEM(pAddrIdx) <- new 1713 ; mark_log(LOG_MEM, log_w_mem_mask(pAddrIdx, pAddr, mask, data, old, new)) 1714 } 1715 else { if align + nbytes <= Size(mask) div 8 -- write to a single regType-sized block 1716 then { new = old && ~(mask << (align * 8)) || (data && mask) << (align * 8) 1717 ; MEM(pAddrIdx) <- new 1718 ; mark_log(LOG_MEM, log_w_mem_mask_misaligned(pAddrIdx, pAddr, mask, data, align, old, new)) 1719 } 1720 -- write touching adjacent regType-sized blocks 1721 else { dw_old = MEM(pAddrIdx+1) : old 1722 ; dw_data = ZeroExtend(data) << (align*8) 1723 ; dw_mask = ZeroExtend(mask) << (align*8) 1724 ; dw_new = dw_old && ~dw_mask || dw_data && dw_mask 1725 ; MEM(pAddrIdx+1) <- dw_new<2*Size(data)-1:Size(data)> 1726 ; MEM(pAddrIdx) <- dw_new<Size(data)-1:0> 1727 } 1728 } 1729} 1730 1731half rawReadHalf(pAddr::pAddr) = 1732{ pAddrIdx = pAddr<63:3> 1733; data = MEM(pAddrIdx) 1734; mark_log(LOG_MEM, log_r_mem(pAddrIdx, pAddr, data)) 1735; match pAddr<2:1> 1736 { case '00' => data<63:48> 1737 case '01' => data<47:32> 1738 case '10' => data<31:16> 1739 case '11' => data<15:0> 1740 } 1741} 1742 1743rawInstType rawReadInst(pAddr::pAddr) = 1744{ h = MEM8 (pAddr) 1745; match h 1746 { case '_ 11' => { Skip <- 4 ; 1747 Word (MEM8 (pAddr + 3) : MEM8 (pAddr + 2) : 1748 MEM8 (pAddr + 1) : MEM8 (pAddr)) } 1749 case _ => { Skip <- 2 ; 1750 Half (MEM8 (pAddr + 1) : MEM8 (pAddr)) } 1751 } 1752} 1753 1754-- helper used to preload memory contents 1755unit rawWriteMem(pAddr::pAddr, data::regType) = 1756{ pAddrIdx = pAddr<63:3> 1757; MEM(pAddrIdx) <- data 1758; mark_log(LOG_MEM, log_w_mem(pAddrIdx, pAddr, data)) 1759} 1760 1761--------------------------------------------------------------------------- 1762-- Address Translation 1763--------------------------------------------------------------------------- 1764 1765-- memory permissions 1766 1767bool checkMemPermission(ft::fetchType, ac::accessType, priv::Privilege, perm::permType) = 1768 match perm 1769 { case 0 => #INTERNAL_ERROR("Checking perm on Page-Table pointer!") 1770 case 1 => #INTERNAL_ERROR("Checking perm on Page-Table pointer!") 1771 case 2 => if priv == User then ac != Write else (ac == Read and ft == Data) 1772 case 3 => if priv == User then true else ft != Instruction 1773 case 4 => ac == Read and ft == Data 1774 case 5 => ft != Instruction 1775 case 6 => ac != Write 1776 case 7 => true 1777 case 8 => priv != User and ac == Read and ft == Data 1778 case 9 => priv != User and ft != Instruction 1779 case 10 => priv != User and ac != Write 1780 case 11 => priv != User 1781 case 12 => priv != User and ac == Read and ft == Data 1782 case 13 => priv != User and ft != Instruction 1783 case 14 => priv != User and ac != Write 1784 case 15 => priv != User 1785 } 1786 1787bool isGlobal(perm::permType) = 1788 perm<3:2> == 3 1789 1790-- page table walking (currently 64-bit only) 1791 1792register SV_PTE :: regType 1793{ 47-10 : PTE_PPNi -- PPN[2,1,0] 1794 9-7 : PTE_SW -- reserved for software 1795 6 : PTE_D -- dirty bit 1796 5 : PTE_R -- referenced bit 1797 4-1 : PTE_T -- PTE type 1798 0 : PTE_V -- valid bit 1799} 1800 1801register SV_Vaddr :: regType 1802{ 47-12 : Sv_VPNi 1803 11-0 : Sv_PgOfs 1804} 1805 1806(pAddr * SV_PTE * nat * bool * pAddr) option 1807 walk64(vAddr::vAddr, ft::fetchType, ac::accessType, priv::Privilege, ptb::regType, level::nat) measure level = 1808{ va = SV_Vaddr(vAddr) 1809; pt_ofs = ZeroExtend((va.Sv_VPNi >>+ (level * LEVEL_BITS))<(LEVEL_BITS-1):0>) << 3 1810; pte_addr = ptb + pt_ofs 1811; pte = SV_PTE(rawReadData(pte_addr)) 1812; mark_log(LOG_ADDRTR, ["translate(vaddr=0x" : PadLeft(#"0", 16, [vAddr]) : "): level=" : [level] 1813 : " pt_base=0x" : PadLeft(#"0", 16, [ptb]) 1814 : " pt_ofs=" : [[pt_ofs]::nat] 1815 : " pte_addr=0x" : PadLeft(#"0", 16, [pte_addr]) 1816 : " pte=0x" : PadLeft(#"0", 16, [&pte])]) 1817; if not pte.PTE_V 1818 then { mark_log(LOG_ADDRTR, "addr_translate: invalid PTE") 1819 ; None 1820 } 1821 else { if pte.PTE_T == 0 or pte.PTE_T == 1 1822 then { -- ptr to next level table 1823 if level == 0 1824 then { mark_log(LOG_ADDRTR, "last-level pt contains a pointer PTE!") 1825 ; None 1826 } 1827 else walk64(vAddr, ft, ac, priv, ZeroExtend(pte.PTE_PPNi << PAGESIZE_BITS), level - 1) 1828 } 1829 else { -- leaf PTE 1830 if not checkMemPermission(ft, ac, priv, pte.PTE_T) 1831 then { mark_log(LOG_ADDRTR, "PTE permission check failure!") 1832 ; None 1833 } 1834 else { var pte_w = pte 1835 -- update referenced and dirty bits 1836 ; old_r = pte.PTE_R 1837 ; old_d = pte.PTE_D 1838 ; pte_w.PTE_R <- true 1839 ; when ac == Write 1840 do pte_w.PTE_D <- true 1841 ; when old_r != pte_w.PTE_R or old_d != pte_w.PTE_D 1842 do rawWriteData(pte_addr, &pte_w, 8) 1843 -- compute translated address 1844 ; ppn = if level > 0 1845 then ((ZeroExtend((pte.PTE_PPNi >>+ (level * LEVEL_BITS)) << (level * LEVEL_BITS))) 1846 || ZeroExtend(va.Sv_VPNi && ((1 << (level * LEVEL_BITS)) - 1))) 1847 else pte.PTE_PPNi 1848 ; Some(ZeroExtend(ppn : va.Sv_PgOfs), pte_w, level, isGlobal(pte.PTE_T), pte_addr) 1849 } 1850 } 1851 } 1852} 1853 1854-- TLB 1855--------------------------------------------------------------------------- 1856-- We maintain an internal model of a TLB. The spec leaves the TLB 1857-- unspecified, but we would like to capture the semantics of SFENCE. 1858-- The TLB also improves simulation speed. 1859 1860-- This implementation stores the global mapping bit from the PTE in 1861-- the TLB. This causes an asymmetry between TLB lookup and TLB 1862-- flush, due to the spec's treatment of an ASID=0 in SFENCE.VM: 1863-- 1864-- * in TLB lookup, the global bit is used to check for a global 1865-- match, and this global bit when set overrides the input ASID. 1866-- 1867-- * in TLB flush, an input ASID of 0 overrides the global bit when 1868-- checking if a TLB entry needs to be flushed. 1869 1870-- Each TLBEntry also stores the full PTE and its pAddr, so that it 1871-- can write back the PTE when its dirty bit needs to be updated. 1872 1873asidType curASID() = 1874 SCSR.sasid<ASID_SIZE-1:0> 1875 1876record TLBEntry 1877{ asid :: asidType 1878 global :: bool 1879 vAddr :: vAddr -- VPN 1880 vMatchMask :: vAddr -- matching mask for superpages 1881 1882 pAddr :: pAddr -- PPN 1883 vAddrMask :: vAddr -- selection mask for superpages 1884 1885 pte :: SV_PTE -- permissions and dirty bit writeback 1886 pteAddr :: pAddr 1887 1888 age :: regType -- derived from instret 1889} 1890 1891TLBEntry mkTLBEntry(asid::asidType, global::bool, vAddr::vAddr, pAddr::pAddr, 1892 pte::SV_PTE, i::nat, pteAddr::pAddr) = 1893{ var ent :: TLBEntry 1894; ent.asid <- asid 1895; ent.global <- global 1896; ent.pte <- pte 1897; ent.pteAddr <- pteAddr 1898; ent.vAddrMask <- ((1::vAddr) << ((LEVEL_BITS*i) + PAGESIZE_BITS)) - 1 1899; ent.vMatchMask <- (SignExtend('1')::vAddr) ?? ent.vAddrMask 1900; ent.vAddr <- vAddr && ent.vMatchMask 1901; ent.pAddr <- (pAddr >> (PAGESIZE_BITS + (LEVEL_BITS*i))) << (PAGESIZE_BITS + (LEVEL_BITS*i)) 1902; ent.age <- c_cycles(procID) 1903; ent 1904} 1905 1906nat TLBEntries = 16 1907type tlbIdx = bits(4) 1908type TLBMap = tlbIdx -> TLBEntry option 1909 1910(TLBEntry * tlbIdx) option lookupTLB(asid::asidType, vAddr::vAddr, tlb::TLBMap) = 1911{ var ent = None 1912; for i in 0 .. TLBEntries - 1 do 1913 { match tlb([i]) 1914 { case Some(e) => when ent == None and (e.global or e.asid == asid) 1915 and (e.vAddr == vAddr && e.vMatchMask) 1916 do ent <- Some(e, [i]) 1917 case None => () 1918 } 1919 } 1920; ent 1921} 1922 1923TLBMap addToTLB(asid::asidType, vAddr::vAddr, pAddr::pAddr, pte::SV_PTE, pteAddr::pAddr, 1924 i::nat, global::bool, curTLB::TLBMap) = 1925{ var ent = mkTLBEntry(asid, global, vAddr, pAddr, pte, i, pteAddr) 1926; var tlb = curTLB 1927; var oldest = SignExtend('1') 1928; var addIdx = 0 1929; var added = false 1930; for i in 0 .. TLBEntries - 1 do 1931 { match tlb([i]) 1932 { case Some(e) => when e.age <+ oldest 1933 do { oldest <- e.age 1934 ; addIdx <- i 1935 } 1936 case None => when not added 1937 do { tlb([i]) <- Some(ent) 1938 ; added <- true 1939 } 1940 } 1941 } 1942; when not added 1943 do tlb([addIdx]) <- Some(ent) 1944; tlb 1945} 1946 1947TLBMap flushTLB(asid::asidType, addr::vAddr option, curTLB::TLBMap) = 1948{ var tlb = curTLB 1949; for i in 0 .. TLBEntries - 1 do 1950 { match tlb([i]), addr 1951 { case Some(e), Some(va) => when (asid == 0 or (asid == e.asid and not e.global)) 1952 and (e.vAddr == va && e.vMatchMask) 1953 do tlb([i]) <- None 1954 case Some(e), None => when asid == 0 or (asid == e.asid and not e.global) 1955 do tlb([i]) <- None 1956 case None, _ => () 1957 } 1958 } 1959; tlb 1960} 1961 1962declare c_tlb :: id -> TLBMap 1963 1964component TLB :: TLBMap 1965{ value = c_tlb(procID) 1966 assign value = c_tlb(procID) <- value 1967} 1968 1969-- address translation 1970 1971pAddr option translate64(vAddr::regType, ft::fetchType, ac::accessType, priv::Privilege, level::nat) = 1972{ asid = curASID() 1973; match lookupTLB(asid, vAddr, TLB) 1974 { case Some(e, idx) => 1975 { if checkMemPermission(ft, ac, priv, e.pte.PTE_T) 1976 then { mark_log(LOG_ADDRTR, "TLB hit!") 1977 -- update dirty bit in page table and TLB if needed 1978 ; when ac == Write and not e.pte.PTE_D 1979 do { var ent = e 1980 ; ent.pte.PTE_D <- true 1981 ; rawWriteData(ent.pteAddr, ent.&pte, 8) 1982 ; var tlb = TLB 1983 ; tlb([idx]) <- Some(ent) 1984 ; TLB <- tlb 1985 } 1986 ; Some(e.pAddr || (vAddr && e.vAddrMask)) 1987 } 1988 else { mark_log(LOG_ADDRTR, "TLB permission check failure") 1989 ; None 1990 } 1991 } 1992 case None => 1993 { mark_log(LOG_ADDRTR, "TLB miss!") 1994 ; match walk64(vAddr, ft, ac, priv, SCSR.sptbr, level) 1995 { case Some(pAddr, pte, i, global, pteAddr) => 1996 { TLB <- addToTLB(asid, vAddr, pAddr, pte, pteAddr, i, global, TLB) 1997 ; Some(pAddr) 1998 } 1999 case None => None 2000 } 2001 } 2002 } 2003} 2004 2005pAddr option translateAddr(vAddr::regType, ft::fetchType, ac::accessType) = 2006{ priv = privilege(if MCSR.mstatus.MMPRV and ft == Data 2007 then MCSR.mstatus.MPRV1 else MCSR.mstatus.MPRV) 2008; match vmType(MCSR.mstatus.VM), priv 2009 { case Mbare, _ 2010 or _, Machine => Some(vAddr) -- no translation 2011 case Sv39, _ => translate64(vAddr, ft, ac, priv, 2) 2012 case Sv48, _ => translate64(vAddr, ft, ac, priv, 3) 2013 2014 {- Comment out base/bound modes since there are no tests for them. 2015 2016 case Mbb, Machine 2017 or Mbbid, Machine => Some(vAddr) 2018 2019 -} 2020 2021 case _, _ => None 2022 } 2023} 2024 2025--------------------------------------------------------------------------- 2026-- Load Reservation 2027--------------------------------------------------------------------------- 2028 2029bool matchLoadReservation(vAddr::vAddr) = 2030 IsSome(ReserveLoad) and ValOf(ReserveLoad) == vAddr 2031 2032--------------------------------------------------------------------------- 2033-- Control Flow 2034--------------------------------------------------------------------------- 2035 2036unit branchTo(newPC::regType) = 2037{ NextFetch <- Some(BranchTo(newPC)) 2038; when not PROVER_EXPORT do Delta.addr <- Some(newPC) 2039} 2040 2041inline unit noBranch(nextPC::regType) = 2042when not PROVER_EXPORT do { Delta.addr <- Some(nextPC) } 2043 2044--------------------------------------------------------------------------- 2045-- Integer Computational Instructions 2046--------------------------------------------------------------------------- 2047 2048-- Integer register-immediate 2049 2050----------------------------------- 2051-- ADDI rd, rs1, imm 2052----------------------------------- 2053define ArithI > ADDI(rd::reg, rs1::reg, imm::imm12) = 2054 writeRD(rd, GPR(rs1) + SignExtend(imm)) 2055 2056----------------------------------- 2057-- ADDIW rd, rs1, imm (RV64I) 2058----------------------------------- 2059define ArithI > ADDIW(rd::reg, rs1::reg, imm::imm12) = 2060 if in32BitMode() 2061 then signalException(Illegal_Instr) 2062 else { temp = GPR(rs1) + SignExtend(imm) 2063 ; writeRD(rd, SignExtend(temp<31:0>)) 2064 } 2065 2066----------------------------------- 2067-- SLTI rd, rs1, imm 2068----------------------------------- 2069define ArithI > SLTI(rd::reg, rs1::reg, imm::imm12) = 2070{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2071; writeRD(rd, [v1 < SignExtend(imm)]) 2072} 2073 2074----------------------------------- 2075-- SLTIU rd, rs1, imm 2076----------------------------------- 2077define ArithI > SLTIU(rd::reg, rs1::reg, imm::imm12) = 2078{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2079; writeRD(rd, [v1 <+ SignExtend(imm)]) 2080} 2081 2082----------------------------------- 2083-- ANDI rd, rs1, imm 2084----------------------------------- 2085define ArithI > ANDI(rd::reg, rs1::reg, imm::imm12) = 2086 writeRD(rd, GPR(rs1) && SignExtend(imm)) 2087 2088----------------------------------- 2089-- ORI rd, rs1, imm 2090----------------------------------- 2091define ArithI > ORI(rd::reg, rs1::reg, imm::imm12) = 2092 writeRD(rd, GPR(rs1) || SignExtend(imm)) 2093 2094----------------------------------- 2095-- XORI rd, rs1, imm 2096----------------------------------- 2097define ArithI > XORI(rd::reg, rs1::reg, imm::imm12) = 2098 writeRD(rd, GPR(rs1) ?? SignExtend(imm)) 2099 2100 2101----------------------------------- 2102-- SLLI rd, rs1, imm 2103----------------------------------- 2104define Shift > SLLI(rd::reg, rs1::reg, imm::bits(6)) = 2105 if in32BitMode() and imm<5> 2106 then signalException(Illegal_Instr) 2107 else writeRD(rd, GPR(rs1) << [imm]) 2108 2109----------------------------------- 2110-- SRLI rd, rs1, imm 2111----------------------------------- 2112define Shift > SRLI(rd::reg, rs1::reg, imm::bits(6)) = 2113 if in32BitMode() and imm<5> 2114 then signalException(Illegal_Instr) 2115 else { v1 = if in32BitMode() then ZeroExtend(GPR(rs1)<31:0>) else GPR(rs1) 2116 ; writeRD(rd, v1 >>+ [imm]) 2117 } 2118 2119----------------------------------- 2120-- SRAI rd, rs1, imm 2121----------------------------------- 2122define Shift > SRAI(rd::reg, rs1::reg, imm::bits(6)) = 2123 if in32BitMode() and imm<5> 2124 then signalException(Illegal_Instr) 2125 else { v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2126 ; writeRD(rd, v1 >> [imm]) 2127 } 2128 2129----------------------------------- 2130-- SLLIW rd, rs1, imm (RV64I) 2131----------------------------------- 2132define Shift > SLLIW(rd::reg, rs1::reg, imm::bits(5)) = 2133 if in32BitMode() 2134 then signalException(Illegal_Instr) 2135 else writeRD(rd, SignExtend(GPR(rs1)<31:0> << [imm])) 2136 2137----------------------------------- 2138-- SRLIW rd, rs1, imm (RV64I) 2139----------------------------------- 2140define Shift > SRLIW(rd::reg, rs1::reg, imm::bits(5)) = 2141 if in32BitMode() 2142 then signalException(Illegal_Instr) 2143 else writeRD(rd, SignExtend(GPR(rs1)<31:0> >>+ [imm])) 2144 2145----------------------------------- 2146-- SRAIW rd, rs1, imm (RV64I) 2147----------------------------------- 2148define Shift > SRAIW(rd::reg, rs1::reg, imm::bits(5)) = 2149 if in32BitMode() 2150 then signalException(Illegal_Instr) 2151 else writeRD(rd, SignExtend(GPR(rs1)<31:0> >> [imm])) 2152 2153----------------------------------- 2154-- LUI rd, imm 2155----------------------------------- 2156define ArithI > LUI(rd::reg, imm::imm20) = 2157 writeRD(rd, SignExtend(imm : 0`12)) 2158 2159----------------------------------- 2160-- AUIPC rd, imm 2161----------------------------------- 2162define ArithI > AUIPC(rd::reg, imm::imm20) = 2163 writeRD(rd, PC + SignExtend(imm : 0`12)) 2164 2165 2166-- Integer register-register 2167 2168----------------------------------- 2169-- ADD rd, rs1, rs2 2170----------------------------------- 2171define ArithR > ADD(rd::reg, rs1::reg, rs2::reg) = 2172 writeRD(rd, GPR(rs1) + GPR(rs2)) 2173 2174----------------------------------- 2175-- ADDW rd, rs1, rs2 (RV64I) 2176----------------------------------- 2177define ArithR > ADDW(rd::reg, rs1::reg, rs2::reg) = 2178 if in32BitMode() 2179 then signalException(Illegal_Instr) 2180 else writeRD(rd, SignExtend(GPR(rs1)<31:0> + GPR(rs2)<31:0>)) 2181 2182----------------------------------- 2183-- SUB rd, rs1, rs2 2184----------------------------------- 2185define ArithR > SUB(rd::reg, rs1::reg, rs2::reg) = 2186 writeRD(rd, GPR(rs1) - GPR(rs2)) 2187 2188----------------------------------- 2189-- SUBW rd, rs1, rs2 (RV64I) 2190----------------------------------- 2191define ArithR > SUBW(rd::reg, rs1::reg, rs2::reg) = 2192 if in32BitMode() 2193 then signalException(Illegal_Instr) 2194 else writeRD(rd, SignExtend(GPR(rs1)<31:0> - GPR(rs2)<31:0>)) 2195 2196----------------------------------- 2197-- SLT rd, rs1, rs2 2198----------------------------------- 2199define ArithR > SLT(rd::reg, rs1::reg, rs2::reg) = 2200{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2201; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2202; writeRD(rd, [v1 < v2]) 2203} 2204 2205----------------------------------- 2206-- SLTU rd, rs1, rs2 2207----------------------------------- 2208define ArithR > SLTU(rd::reg, rs1::reg, rs2::reg) = 2209{ v1 = if in32BitMode() then ZeroExtend(GPR(rs1)<31:0>) else GPR(rs1) 2210; v2 = if in32BitMode() then ZeroExtend(GPR(rs2)<31:0>) else GPR(rs2) 2211; writeRD(rd, [v1 <+ v2]) 2212} 2213 2214----------------------------------- 2215-- AND rd, rs1, rs2 2216----------------------------------- 2217define ArithR > AND(rd::reg, rs1::reg, rs2::reg) = 2218 writeRD(rd, GPR(rs1) && GPR(rs2)) 2219 2220----------------------------------- 2221-- OR rd, rs1, rs2 2222----------------------------------- 2223define ArithR > OR(rd::reg, rs1::reg, rs2::reg) = 2224 writeRD(rd, GPR(rs1) || GPR(rs2)) 2225 2226----------------------------------- 2227-- XOR rd, rs1, rs2 2228----------------------------------- 2229define ArithR > XOR(rd::reg, rs1::reg, rs2::reg) = 2230 writeRD(rd, GPR(rs1) ?? GPR(rs2)) 2231 2232----------------------------------- 2233-- SLL rd, rs1, rs2 2234----------------------------------- 2235define Shift > SLL(rd::reg, rs1::reg, rs2::reg) = 2236 if in32BitMode() 2237 then writeRD(rd, GPR(rs1) << ZeroExtend(GPR(rs2)<4:0>)) 2238 else writeRD(rd, GPR(rs1) << ZeroExtend(GPR(rs2)<5:0>)) 2239 2240----------------------------------- 2241-- SLLW rd, rs1, rs2 (RV64I) 2242----------------------------------- 2243define Shift > SLLW(rd::reg, rs1::reg, rs2::reg) = 2244 if in32BitMode() 2245 then signalException(Illegal_Instr) 2246 else writeRD(rd, SignExtend(GPR(rs1)<31:0> << ZeroExtend(GPR(rs2)<4:0>))) 2247 2248----------------------------------- 2249-- SRL rd, rs1, rs2 2250----------------------------------- 2251define Shift > SRL(rd::reg, rs1::reg, rs2::reg) = 2252 if in32BitMode() 2253 then writeRD(rd, ZeroExtend(GPR(rs1)<31:0> >>+ ZeroExtend(GPR(rs2)<4:0>))) 2254 else writeRD(rd, GPR(rs1) >>+ ZeroExtend(GPR(rs2)<5:0>)) 2255 2256----------------------------------- 2257-- SRLW rd, rs1, rs2 (RV64I) 2258----------------------------------- 2259define Shift > SRLW(rd::reg, rs1::reg, rs2::reg) = 2260 if in32BitMode() 2261 then signalException(Illegal_Instr) 2262 else writeRD(rd, SignExtend(GPR(rs1)<31:0> >>+ ZeroExtend(GPR(rs2)<4:0>))) 2263 2264----------------------------------- 2265-- SRA rd, rs1, rs2 2266----------------------------------- 2267define Shift > SRA(rd::reg, rs1::reg, rs2::reg) = 2268 if in32BitMode() 2269 then writeRD(rd, SignExtend(GPR(rs1)<31:0> >> ZeroExtend(GPR(rs2)<4:0>))) 2270 else writeRD(rd, GPR(rs1) >> ZeroExtend(GPR(rs2)<5:0>)) 2271 2272----------------------------------- 2273-- SRAW rd, rs1, rs2 (RV64I) 2274----------------------------------- 2275define Shift > SRAW(rd::reg, rs1::reg, rs2::reg) = 2276 if in32BitMode() 2277 then signalException(Illegal_Instr) 2278 else writeRD(rd, SignExtend(GPR(rs1)<31:0> >> ZeroExtend(GPR(rs2)<4:0>))) 2279 2280--------------------------------------------------------------------------- 2281-- Multiply and Divide 2282--------------------------------------------------------------------------- 2283 2284----------------------------------- 2285-- MUL rd, rs1, rs2 2286----------------------------------- 2287define MulDiv > MUL(rd::reg, rs1::reg, rs2::reg) = 2288 writeRD(rd, GPR(rs1) * GPR(rs2)) 2289 2290----------------------------------- 2291-- MULH rd, rs1, rs2 2292----------------------------------- 2293define MulDiv > MULH(rd::reg, rs1::reg, rs2::reg) = 2294{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2295; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2296; prod`128 = SignExtend(v1) * SignExtend(v2) 2297; res = if in32BitMode() then SignExtend(prod<63:32>) else SignExtend(prod<127:64>) 2298; writeRD(rd, res) 2299} 2300 2301----------------------------------- 2302-- MULHU rd, rs1, rs2 2303----------------------------------- 2304define MulDiv > MULHU(rd::reg, rs1::reg, rs2::reg) = 2305{ v1 = if in32BitMode() then ZeroExtend(GPR(rs1)<31:0>) else ZeroExtend(GPR(rs1)) 2306; v2 = if in32BitMode() then ZeroExtend(GPR(rs2)<31:0>) else ZeroExtend(GPR(rs2)) 2307; prod`128 = v1 * v2 2308; res = if in32BitMode() then ZeroExtend(prod<63:32>) else prod<127:64> 2309; writeRD(rd, res) 2310} 2311 2312----------------------------------- 2313-- MULHSU rd, rs1, rs2 2314----------------------------------- 2315define MulDiv > MULHSU(rd::reg, rs1::reg, rs2::reg) = 2316{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else SignExtend(GPR(rs1)) 2317; v2 = if in32BitMode() then ZeroExtend(GPR(rs2)<31:0>) else ZeroExtend(GPR(rs2)) 2318; prod`128 = v1 * v2 2319; res = if in32BitMode() then SignExtend(prod<63:32>) else prod<127:64> 2320; writeRD(rd, res) 2321} 2322 2323----------------------------------- 2324-- MULW rd, rs1, rs2 2325----------------------------------- 2326define MulDiv > MULW(rd::reg, rs1::reg, rs2::reg) = 2327 if in32BitMode() 2328 then signalException(Illegal_Instr) 2329 else { prod`64 = SignExtend(GPR(rs1)<31:0> * GPR(rs2)<31:0>) 2330 ; writeRD(rd, SignExtend(prod<31:0>)) 2331 } 2332 2333----------------------------------- 2334-- DIV rd, rs1, rs2 2335----------------------------------- 2336define MulDiv > DIV(rd::reg, rs1::reg, rs2::reg) = 2337 if GPR(rs2) == 0x0 2338 then writeRD(rd, SignExtend(1`1)) 2339 else writeRD(rd, GPR(rs1) quot GPR(rs2)) 2340 2341----------------------------------- 2342-- REM rd, rs1, rs2 2343----------------------------------- 2344define MulDiv > REM(rd::reg, rs1::reg, rs2::reg) = 2345 if GPR(rs2) == 0x0 2346 then writeRD(rd, GPR(rs1)) 2347 else writeRD(rd, GPR(rs1) rem GPR(rs2)) 2348 2349----------------------------------- 2350-- DIVU rd, rs1, rs2 2351----------------------------------- 2352define MulDiv > DIVU(rd::reg, rs1::reg, rs2::reg) = 2353{ v1 = if in32BitMode() then ZeroExtend(GPR(rs1)<31:0>) else GPR(rs1) 2354; v2 = if in32BitMode() then ZeroExtend(GPR(rs2)<31:0>) else GPR(rs2) 2355; if v2 == 0x0 2356 then writeRD(rd, SignExtend(1`1)) 2357 else writeRD(rd, v1 div v2) 2358} 2359 2360----------------------------------- 2361-- REMU rd, rs1, rs2 2362----------------------------------- 2363define MulDiv > REMU(rd::reg, rs1::reg, rs2::reg) = 2364 if GPR(rs2) == 0x0 2365 then writeRD(rd, GPR(rs1)) 2366 else writeRD(rd, GPR(rs1) mod GPR(rs2)) 2367 2368----------------------------------- 2369-- DIVW rd, rs1, rs2 2370----------------------------------- 2371define MulDiv > DIVW(rd::reg, rs1::reg, rs2::reg) = 2372 if in32BitMode() 2373 then signalException(Illegal_Instr) 2374 else { s1 = GPR(rs1)<31:0> 2375 ; s2 = GPR(rs2)<31:0> 2376 ; if s2 == 0x0 2377 then writeRD(rd, SignExtend(1`1)) 2378 else writeRD(rd, SignExtend(s1 quot s2)) 2379 } 2380 2381----------------------------------- 2382-- REMW rd, rs1, rs2 2383----------------------------------- 2384define MulDiv > REMW(rd::reg, rs1::reg, rs2::reg) = 2385 if in32BitMode() 2386 then signalException(Illegal_Instr) 2387 else { s1 = GPR(rs1)<31:0> 2388 ; s2 = GPR(rs2)<31:0> 2389 ; if s2 == 0x0 2390 then writeRD(rd, SignExtend(s1)) 2391 else writeRD(rd, SignExtend(s1 rem s2)) 2392 } 2393 2394----------------------------------- 2395-- DIVUW rd, rs1, rs2 2396----------------------------------- 2397define MulDiv > DIVUW(rd::reg, rs1::reg, rs2::reg) = 2398 if in32BitMode() 2399 then signalException(Illegal_Instr) 2400 else { s1 = GPR(rs1)<31:0> 2401 ; s2 = GPR(rs2)<31:0> 2402 ; if s2 == 0x0 2403 then writeRD(rd, SignExtend(1`1)) 2404 else writeRD(rd, SignExtend(s1 div s2)) 2405 } 2406 2407----------------------------------- 2408-- REMUW rd, rs1, rs2 2409----------------------------------- 2410define MulDiv > REMUW(rd::reg, rs1::reg, rs2::reg) = 2411 if in32BitMode() 2412 then signalException(Illegal_Instr) 2413 else { s1 = GPR(rs1)<31:0> 2414 ; s2 = GPR(rs2)<31:0> 2415 ; if s2 == 0x0 2416 then writeRD(rd, SignExtend(s1)) 2417 else writeRD(rd, SignExtend(s1 mod s2)) 2418 } 2419 2420--------------------------------------------------------------------------- 2421-- Control Transfer Instructions 2422--------------------------------------------------------------------------- 2423 2424-- Unconditional jumps 2425 2426----------------------------------- 2427-- JAL rd, offs 2428----------------------------------- 2429define Branch > JAL(rd::reg, imm::imm20) = 2430{ addr = PC + SignExtend(imm) << 1 2431; if addr<0> 2432 then signalAddressException(Fetch_Misaligned, addr) 2433 else { writeRD(rd, PC + Skip) 2434 ; branchTo(addr) 2435 } 2436} 2437 2438----------------------------------- 2439-- JALR rd, rs1, imm 2440----------------------------------- 2441define Branch > JALR(rd::reg, rs1::reg, imm::imm12) = 2442{ addr = (GPR(rs1) + SignExtend(imm)) && SignExtend('10') 2443; if addr<0> 2444 then signalAddressException(Fetch_Misaligned, addr) 2445 else { writeRD(rd, PC + Skip) 2446 ; branchTo(addr) 2447 } 2448} 2449 2450-- conditional branches 2451 2452----------------------------------- 2453-- BEQ rs1, rs2, offs 2454----------------------------------- 2455define Branch > BEQ(rs1::reg, rs2::reg, offs::imm12) = 2456{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2457; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2458; if v1 == v2 2459 then branchTo(PC + (SignExtend(offs) << 1)) 2460 else noBranch(PC + Skip) 2461} 2462 2463----------------------------------- 2464-- BNE rs1, rs2, offs 2465----------------------------------- 2466define Branch > BNE(rs1::reg, rs2::reg, offs::imm12) = 2467{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2468; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2469; if v1 <> v2 2470 then branchTo(PC + (SignExtend(offs) << 1)) 2471 else noBranch(PC + Skip) 2472} 2473 2474----------------------------------- 2475-- BLT rs1, rs2, offs 2476----------------------------------- 2477define Branch > BLT(rs1::reg, rs2::reg, offs::imm12) = 2478{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2479; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2480; if v1 < v2 2481 then branchTo(PC + (SignExtend(offs) << 1)) 2482 else noBranch(PC + Skip) 2483} 2484 2485----------------------------------- 2486-- BLTU rs1, rs2, offs 2487----------------------------------- 2488define Branch > BLTU(rs1::reg, rs2::reg, offs::imm12) = 2489{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2490; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2491; if v1 <+ v2 2492 then branchTo(PC + (SignExtend(offs) << 1)) 2493 else noBranch(PC + Skip) 2494} 2495 2496----------------------------------- 2497-- BGE rs1, rs2, offs 2498----------------------------------- 2499define Branch > BGE(rs1::reg, rs2::reg, offs::imm12) = 2500{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2501; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2502; if v1 >= v2 2503 then branchTo(PC + (SignExtend(offs) << 1)) 2504 else noBranch(PC + Skip) 2505} 2506 2507----------------------------------- 2508-- BGEU rs1, rs2, offs 2509----------------------------------- 2510define Branch > BGEU(rs1::reg, rs2::reg, offs::imm12) = 2511{ v1 = if in32BitMode() then SignExtend(GPR(rs1)<31:0>) else GPR(rs1) 2512; v2 = if in32BitMode() then SignExtend(GPR(rs2)<31:0>) else GPR(rs2) 2513; if v1 >=+ v2 2514 then branchTo(PC + (SignExtend(offs) << 1)) 2515 else noBranch(PC + Skip) 2516} 2517 2518--------------------------------------------------------------------------- 2519-- Load and Store Instructions 2520--------------------------------------------------------------------------- 2521 2522----------------------------------- 2523-- LW rd, rs1, offs 2524----------------------------------- 2525define Load > LW(rd::reg, rs1::reg, offs::imm12) = 2526{ vAddr = GPR(rs1) + SignExtend(offs) 2527; match translateAddr(vAddr, Data, Read) 2528 { case Some(pAddr) => { val = SignExtend(rawReadData(pAddr)<31:0>) 2529 ; GPR(rd) <- val 2530 ; recordLoad(vAddr, val) 2531 } 2532 case None => signalAddressException(Load_Fault, vAddr) 2533 } 2534} 2535 2536----------------------------------- 2537-- LWU rd, rs1, offs (RV64I) 2538----------------------------------- 2539define Load > LWU(rd::reg, rs1::reg, offs::imm12) = 2540{ if in32BitMode() 2541 then signalException(Illegal_Instr) 2542 else { vAddr = GPR(rs1) + SignExtend(offs) 2543 ; match translateAddr(vAddr, Data, Read) 2544 { case Some(pAddr) => { val = ZeroExtend(rawReadData(pAddr)<31:0>) 2545 ; GPR(rd) <- val 2546 ; recordLoad(vAddr, val) 2547 } 2548 case None => signalAddressException(Load_Fault, vAddr) 2549 } 2550 } 2551} 2552 2553----------------------------------- 2554-- LH rd, rs1, offs 2555----------------------------------- 2556define Load > LH(rd::reg, rs1::reg, offs::imm12) = 2557{ vAddr = GPR(rs1) + SignExtend(offs) 2558; match translateAddr(vAddr, Data, Read) 2559 { case Some(pAddr) => { val = SignExtend(rawReadData(pAddr)<15:0>) 2560 ; GPR(rd) <- val 2561 ; recordLoad(vAddr, val) 2562 } 2563 case None => signalAddressException(Load_Fault, vAddr) 2564 } 2565} 2566 2567----------------------------------- 2568-- LHU rd, rs1, offs 2569----------------------------------- 2570define Load > LHU(rd::reg, rs1::reg, offs::imm12) = 2571{ vAddr = GPR(rs1) + SignExtend(offs) 2572; match translateAddr(vAddr, Data, Read) 2573 { case Some(pAddr) => { val = ZeroExtend(rawReadData(pAddr)<15:0>) 2574 ; GPR(rd) <- val 2575 ; recordLoad(vAddr, val) 2576 } 2577 case None => signalAddressException(Load_Fault, vAddr) 2578 } 2579} 2580 2581----------------------------------- 2582-- LB rd, rs1, offs 2583----------------------------------- 2584define Load > LB(rd::reg, rs1::reg, offs::imm12) = 2585{ vAddr = GPR(rs1) + SignExtend(offs) 2586; match translateAddr(vAddr, Data, Read) 2587 { case Some(pAddr) => { val = SignExtend(rawReadData(pAddr)<7:0>) 2588 ; GPR(rd) <- val 2589 ; recordLoad(vAddr, val) 2590 } 2591 case None => signalAddressException(Load_Fault, vAddr) 2592 } 2593} 2594 2595----------------------------------- 2596-- LBU rd, rs1, offs 2597----------------------------------- 2598define Load > LBU(rd::reg, rs1::reg, offs::imm12) = 2599{ vAddr = GPR(rs1) + SignExtend(offs) 2600; match translateAddr(vAddr, Data, Read) 2601 { case Some(pAddr) => { val = ZeroExtend(rawReadData(pAddr)<7:0>) 2602 ; GPR(rd) <- val 2603 ; recordLoad(vAddr, val) 2604 } 2605 case None => signalAddressException(Load_Fault, vAddr) 2606 } 2607} 2608 2609----------------------------------- 2610-- LD rd, rs1, offs (RV64I) 2611----------------------------------- 2612define Load > LD(rd::reg, rs1::reg, offs::imm12) = 2613 if in32BitMode() 2614 then signalException(Illegal_Instr) 2615 else { vAddr = GPR(rs1) + SignExtend(offs) 2616 ; match translateAddr(vAddr, Data, Read) 2617 { case Some(pAddr) => { val = rawReadData(pAddr) 2618 ; GPR(rd) <- val 2619 ; recordLoad(vAddr, val) 2620 } 2621 case None => signalAddressException(Load_Fault, vAddr) 2622 } 2623 } 2624 2625----------------------------------- 2626-- SW rs1, rs2, offs 2627----------------------------------- 2628define Store > SW(rs1::reg, rs2::reg, offs::imm12) = 2629{ vAddr = GPR(rs1) + SignExtend(offs) 2630; match translateAddr(vAddr, Data, Write) 2631 { case Some(pAddr) => { data = GPR(rs2) 2632 ; rawWriteData(pAddr, data, 4) 2633 ; recordStore(vAddr, data, 4) 2634 } 2635 case None => signalAddressException(Store_AMO_Fault, vAddr) 2636 } 2637} 2638 2639----------------------------------- 2640-- SH rs1, rs2, offs 2641----------------------------------- 2642define Store > SH(rs1::reg, rs2::reg, offs::imm12) = 2643{ vAddr = GPR(rs1) + SignExtend(offs) 2644; match translateAddr(vAddr, Data, Write) 2645 { case Some(pAddr) => { data = GPR(rs2) 2646 ; rawWriteData(pAddr, data, 2) 2647 ; recordStore(vAddr, data, 2) 2648 } 2649 case None => signalAddressException(Store_AMO_Fault, vAddr) 2650 } 2651} 2652 2653----------------------------------- 2654-- SB rs1, rs2, offs 2655----------------------------------- 2656define Store > SB(rs1::reg, rs2::reg, offs::imm12) = 2657{ vAddr = GPR(rs1) + SignExtend(offs) 2658; match translateAddr(vAddr, Data, Write) 2659 { case Some(pAddr) => { data = GPR(rs2) 2660 ; rawWriteData(pAddr, data, 1) 2661 ; recordStore(vAddr, data, 1) 2662 } 2663 case None => signalAddressException(Store_AMO_Fault, vAddr) 2664 } 2665} 2666 2667----------------------------------- 2668-- SD rs1, rs2, offs (RV64I) 2669----------------------------------- 2670define Store > SD(rs1::reg, rs2::reg, offs::imm12) = 2671 if in32BitMode() 2672 then signalException(Illegal_Instr) 2673 else { vAddr = GPR(rs1) + SignExtend(offs) 2674 ; match translateAddr(vAddr, Data, Write) 2675 { case Some(pAddr) => { data = GPR(rs2) 2676 ; rawWriteData(pAddr, data, 8) 2677 ; recordStore(vAddr, data, 8) 2678 } 2679 case None => signalAddressException(Store_AMO_Fault, vAddr) 2680 } 2681 } 2682 2683--------------------------------------------------------------------------- 2684-- Memory model 2685--------------------------------------------------------------------------- 2686 2687----------------------------------- 2688-- FENCE rd, rs1, pred, succ 2689----------------------------------- 2690define FENCE(rd::reg, rs1::reg, pred::bits(4), succ::bits(4)) = nothing 2691 2692----------------------------------- 2693-- FENCE.I rd, rs1, imm 2694----------------------------------- 2695define FENCE_I(rd::reg, rs1::reg, imm::imm12) = nothing 2696 2697-- Atomics -- 2698 2699----------------------------------- 2700-- LR.W [aq,rl] rd, rs1 2701----------------------------------- 2702define AMO > LR_W(aq::amo, rl::amo, rd::reg, rs1::reg) = 2703{ vAddr = GPR(rs1) 2704; if vAddr<1:0> != 0 2705 then signalAddressException(AMO_Misaligned, vAddr) 2706 else match translateAddr(vAddr, Data, Read) 2707 { case Some(pAddr) => { writeRD(rd, SignExtend(rawReadData(pAddr)<31:0>)) 2708 ; ReserveLoad <- Some(vAddr) 2709 } 2710 case None => signalAddressException(Load_Fault, vAddr) 2711 } 2712} 2713 2714----------------------------------- 2715-- LR.D [aq,rl] rd, rs1 2716----------------------------------- 2717define AMO > LR_D(aq::amo, rl::amo, rd::reg, rs1::reg) = 2718 if in32BitMode() 2719 then signalException(Illegal_Instr) 2720 else { vAddr = GPR(rs1) 2721 ; if vAddr<2:0> != 0 2722 then signalAddressException(AMO_Misaligned, vAddr) 2723 else match translateAddr(vAddr, Data, Read) 2724 { case Some(pAddr) => { writeRD(rd, rawReadData(pAddr)) 2725 ; ReserveLoad <- Some(vAddr) 2726 } 2727 case None => signalAddressException(Load_Fault, vAddr) 2728 } 2729 } 2730 2731----------------------------------- 2732-- SC.W [aq,rl] rd, rs1, rs2 2733----------------------------------- 2734define AMO > SC_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2735{ vAddr = GPR(rs1) 2736; if vAddr<1:0> != 0 2737 then signalAddressException(AMO_Misaligned, vAddr) 2738 else if not matchLoadReservation(vAddr) 2739 then writeRD(rd, 1) 2740 else match translateAddr(vAddr, Data, Read) 2741 { case Some(pAddr) => { data = GPR(rs2) 2742 ; rawWriteData(pAddr, data, 4) 2743 ; recordStore(vAddr, data, 4) 2744 ; writeRD(rd, 0) 2745 ; ReserveLoad <- None 2746 } 2747 case None => signalAddressException(Store_AMO_Fault, vAddr) 2748 } 2749} 2750 2751----------------------------------- 2752-- SC.D [aq,rl] rd, rs1, rs2 2753----------------------------------- 2754define AMO > SC_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2755 if in32BitMode() 2756 then signalException(Illegal_Instr) 2757 else { vAddr = GPR(rs1) 2758 ; if vAddr<2:0> != 0 2759 then signalAddressException(AMO_Misaligned, vAddr) 2760 else if not matchLoadReservation(vAddr) 2761 then writeRD(rd, 1) 2762 else match translateAddr(vAddr, Data, Read) 2763 { case Some(pAddr) => { data = GPR(rs2) 2764 ; rawWriteData(pAddr, data, 8) 2765 ; recordStore(vAddr, data, 8) 2766 ; writeRD(rd, 0) 2767 ; ReserveLoad <- None 2768 } 2769 case None => signalAddressException(Store_AMO_Fault, vAddr) 2770 } 2771 } 2772 2773----------------------------------- 2774-- AMOSWAP.W [aq,rl] rd, rs1, rs2 2775----------------------------------- 2776define AMO > AMOSWAP_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2777{ vAddr = GPR(rs1) 2778; if vAddr<1:0> != 0 2779 then signalAddressException(AMO_Misaligned, vAddr) 2780 else match translateAddr(vAddr, Data, Write) 2781 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 2782 ; data = GPR(rs2) 2783 ; GPR(rd) <- memv 2784 ; rawWriteData(pAddr, data, 4) 2785 ; recordLoad(vAddr, memv) 2786 ; recordStore(vAddr, data, 4) 2787 } 2788 case None => signalAddressException(Store_AMO_Fault, vAddr) 2789 } 2790} 2791 2792----------------------------------- 2793-- AMOSWAP.D [aq,rl] rd, rs1, rs2 2794----------------------------------- 2795define AMO > AMOSWAP_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2796{ vAddr = GPR(rs1) 2797; if vAddr<2:0> != 0 2798 then signalAddressException(AMO_Misaligned, vAddr) 2799 else match translateAddr(vAddr, Data, Write) 2800 { case Some(pAddr) => { memv = rawReadData(pAddr) 2801 ; data = GPR(rs2) 2802 ; GPR(rd) <- memv 2803 ; rawWriteData(pAddr, data, 8) 2804 ; recordLoad(vAddr, memv) 2805 ; recordStore(vAddr, data, 8) 2806 } 2807 case None => signalAddressException(Store_AMO_Fault, vAddr) 2808 } 2809} 2810 2811----------------------------------- 2812-- AMOADD.W [aq,rl] rd, rs1, rs2 2813----------------------------------- 2814define AMO > AMOADD_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2815{ vAddr = GPR(rs1) 2816; if vAddr<1:0> != 0 2817 then signalAddressException(AMO_Misaligned, vAddr) 2818 else match translateAddr(vAddr, Data, Write) 2819 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 2820 ; data = GPR(rs2) 2821 ; GPR(rd) <- memv 2822 ; val = data + memv 2823 ; rawWriteData(pAddr, val, 4) 2824 ; recordLoad(vAddr, memv) 2825 ; recordStore(vAddr, val, 4) 2826 } 2827 case None => signalAddressException(Store_AMO_Fault, vAddr) 2828 } 2829} 2830 2831----------------------------------- 2832-- AMOADD.D [aq,rl] rd, rs1, rs2 2833----------------------------------- 2834define AMO > AMOADD_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2835{ vAddr = GPR(rs1) 2836; if vAddr<2:0> != 0 2837 then signalAddressException(AMO_Misaligned, vAddr) 2838 else match translateAddr(vAddr, Data, Write) 2839 { case Some(pAddr) => { memv = rawReadData(pAddr) 2840 ; data = GPR(rs2) 2841 ; GPR(rd) <- memv 2842 ; val = data + memv 2843 ; rawWriteData(pAddr, val, 8) 2844 ; recordLoad(vAddr, memv) 2845 ; recordStore(vAddr, val, 8) 2846 } 2847 case None => signalAddressException(Store_AMO_Fault, vAddr) 2848 } 2849} 2850 2851----------------------------------- 2852-- AMOXOR.W [aq,rl] rd, rs1, rs2 2853----------------------------------- 2854define AMO > AMOXOR_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2855{ vAddr = GPR(rs1) 2856; if vAddr<1:0> != 0 2857 then signalAddressException(AMO_Misaligned, vAddr) 2858 else match translateAddr(vAddr, Data, Write) 2859 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 2860 ; data = GPR(rs2) 2861 ; GPR(rd) <- memv 2862 ; val = data ?? memv 2863 ; rawWriteData(pAddr, val, 4) 2864 ; recordLoad(vAddr, memv) 2865 ; recordStore(vAddr, val, 4) 2866 } 2867 case None => signalAddressException(Store_AMO_Fault, vAddr) 2868 } 2869} 2870 2871----------------------------------- 2872-- AMOXOR.D [aq,rl] rd, rs1, rs2 2873----------------------------------- 2874define AMO > AMOXOR_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2875{ vAddr = GPR(rs1) 2876; if vAddr<2:0> != 0 2877 then signalAddressException(AMO_Misaligned, vAddr) 2878 else match translateAddr(vAddr, Data, Write) 2879 { case Some(pAddr) => { memv = rawReadData(pAddr) 2880 ; data = GPR(rs2) 2881 ; GPR(rd) <- memv 2882 ; val = data ?? memv 2883 ; rawWriteData(pAddr, val, 8) 2884 ; recordLoad(vAddr, memv) 2885 ; recordStore(vAddr, val, 8) 2886 } 2887 case None => signalAddressException(Store_AMO_Fault, vAddr) 2888 } 2889} 2890 2891----------------------------------- 2892-- AMOAND.W [aq,rl] rd, rs1, rs2 2893----------------------------------- 2894define AMO > AMOAND_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2895{ vAddr = GPR(rs1) 2896; if vAddr<1:0> != 0 2897 then signalAddressException(AMO_Misaligned, vAddr) 2898 else match translateAddr(vAddr, Data, Write) 2899 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 2900 ; data = GPR(rs2) 2901 ; GPR(rd) <- memv 2902 ; val = data && memv 2903 ; rawWriteData(pAddr, val, 4) 2904 ; recordLoad(vAddr, memv) 2905 ; recordStore(vAddr, val, 4) 2906 } 2907 case None => signalAddressException(Store_AMO_Fault, vAddr) 2908 } 2909} 2910 2911----------------------------------- 2912-- AMOAND.D [aq,rl] rd, rs1, rs2 2913----------------------------------- 2914define AMO > AMOAND_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2915{ vAddr = GPR(rs1) 2916; if vAddr<2:0> != 0 2917 then signalAddressException(AMO_Misaligned, vAddr) 2918 else match translateAddr(vAddr, Data, Write) 2919 { case Some(pAddr) => { memv = rawReadData(pAddr) 2920 ; data = GPR(rs2) 2921 ; GPR(rd) <- memv 2922 ; val = data && memv 2923 ; rawWriteData(pAddr, val, 8) 2924 ; recordLoad(vAddr, memv) 2925 ; recordStore(vAddr, val, 8) 2926 } 2927 case None => signalAddressException(Store_AMO_Fault, vAddr) 2928 } 2929} 2930 2931----------------------------------- 2932-- AMOOR.W [aq,rl] rd, rs1, rs2 2933----------------------------------- 2934define AMO > AMOOR_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2935{ vAddr = GPR(rs1) 2936; if vAddr<1:0> != 0 2937 then signalAddressException(AMO_Misaligned, vAddr) 2938 else match translateAddr(vAddr, Data, Write) 2939 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 2940 ; data = GPR(rs2) 2941 ; GPR(rd) <- memv 2942 ; val = data || memv 2943 ; rawWriteData(pAddr, val, 4) 2944 ; recordLoad(vAddr, memv) 2945 ; recordStore(vAddr, val, 4) 2946 } 2947 case None => signalAddressException(Store_AMO_Fault, vAddr) 2948 } 2949} 2950 2951----------------------------------- 2952-- AMOOR.D [aq,rl] rd, rs1, rs2 2953----------------------------------- 2954define AMO > AMOOR_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2955{ vAddr = GPR(rs1) 2956; if vAddr<2:0> != 0 2957 then signalAddressException(AMO_Misaligned, vAddr) 2958 else match translateAddr(vAddr, Data, Write) 2959 { case Some(pAddr) => { memv = rawReadData(pAddr) 2960 ; data = GPR(rs2) 2961 ; GPR(rd) <- memv 2962 ; val = data || memv 2963 ; rawWriteData(pAddr, val, 8) 2964 ; recordLoad(vAddr, memv) 2965 ; recordStore(vAddr, val, 8) 2966 } 2967 case None => signalAddressException(Store_AMO_Fault, vAddr) 2968 } 2969} 2970 2971----------------------------------- 2972-- AMOMIN.W [aq,rl] rd, rs1, rs2 2973----------------------------------- 2974define AMO > AMOMIN_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2975{ vAddr = GPR(rs1) 2976; if vAddr<1:0> != 0 2977 then signalAddressException(AMO_Misaligned, vAddr) 2978 else match translateAddr(vAddr, Data, Write) 2979 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 2980 ; data = GPR(rs2) 2981 ; GPR(rd) <- memv 2982 ; val = SignedMin(data, memv) 2983 ; rawWriteData(pAddr, val, 4) 2984 ; recordLoad(vAddr, memv) 2985 ; recordStore(vAddr, val, 4) 2986 } 2987 case None => signalAddressException(Store_AMO_Fault, vAddr) 2988 } 2989} 2990 2991----------------------------------- 2992-- AMOMIN.D [aq,rl] rd, rs1, rs2 2993----------------------------------- 2994define AMO > AMOMIN_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 2995{ vAddr = GPR(rs1) 2996; if vAddr<2:0> != 0 2997 then signalAddressException(AMO_Misaligned, vAddr) 2998 else match translateAddr(vAddr, Data, Write) 2999 { case Some(pAddr) => { memv = rawReadData(pAddr) 3000 ; data = GPR(rs2) 3001 ; GPR(rd) <- memv 3002 ; val = SignedMin(data, memv) 3003 ; rawWriteData(pAddr, val, 8) 3004 ; recordLoad(vAddr, memv) 3005 ; recordStore(vAddr, val, 8) 3006 } 3007 case None => signalAddressException(Store_AMO_Fault, vAddr) 3008 } 3009} 3010 3011----------------------------------- 3012-- AMOMAX.W [aq,rl] rd, rs1, rs2 3013----------------------------------- 3014define AMO > AMOMAX_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 3015{ vAddr = GPR(rs1) 3016; if vAddr<1:0> != 0 3017 then signalAddressException(AMO_Misaligned, vAddr) 3018 else match translateAddr(vAddr, Data, Write) 3019 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 3020 ; data = GPR(rs2) 3021 ; GPR(rd) <- memv 3022 ; val = SignedMax(data, memv) 3023 ; rawWriteData(pAddr, val, 4) 3024 ; recordLoad(vAddr, memv) 3025 ; recordStore(vAddr, val, 4) 3026 } 3027 case None => signalAddressException(Store_AMO_Fault, vAddr) 3028 } 3029} 3030 3031----------------------------------- 3032-- AMOMAX.D [aq,rl] rd, rs1, rs2 3033----------------------------------- 3034define AMO > AMOMAX_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 3035{ vAddr = GPR(rs1) 3036; if vAddr<2:0> != 0 3037 then signalAddressException(AMO_Misaligned, vAddr) 3038 else match translateAddr(vAddr, Data, Write) 3039 { case Some(pAddr) => { memv = rawReadData(pAddr) 3040 ; data = GPR(rs2) 3041 ; GPR(rd) <- memv 3042 ; val = SignedMax(data, memv) 3043 ; rawWriteData(pAddr, val, 8) 3044 ; recordLoad(vAddr, memv) 3045 ; recordStore(vAddr, val, 8) 3046 } 3047 case None => signalAddressException(Store_AMO_Fault, vAddr) 3048 } 3049} 3050 3051----------------------------------- 3052-- AMOMINU.W [aq,rl] rd, rs1, rs2 3053----------------------------------- 3054define AMO > AMOMINU_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 3055{ vAddr = GPR(rs1) 3056; if vAddr<1:0> != 0 3057 then signalAddressException(AMO_Misaligned, vAddr) 3058 else match translateAddr(vAddr, Data, Write) 3059 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 3060 ; data = GPR(rs2) 3061 ; GPR(rd) <- memv 3062 ; val = Min(data, memv) 3063 ; rawWriteData(pAddr, val, 4) 3064 ; recordLoad(vAddr, memv) 3065 ; recordStore(vAddr, val, 4) 3066 } 3067 case None => signalAddressException(Store_AMO_Fault, vAddr) 3068 } 3069} 3070 3071----------------------------------- 3072-- AMOMINU.D [aq,rl] rd, rs1, rs2 3073----------------------------------- 3074define AMO > AMOMINU_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 3075{ vAddr = GPR(rs1) 3076; if vAddr<2:0> != 0 3077 then signalAddressException(AMO_Misaligned, vAddr) 3078 else match translateAddr(vAddr, Data, Write) 3079 { case Some(pAddr) => { memv = rawReadData(pAddr) 3080 ; data = GPR(rs2) 3081 ; GPR(rd) <- memv 3082 ; val = Min(data, memv) 3083 ; rawWriteData(pAddr, val, 8) 3084 ; recordLoad(vAddr, memv) 3085 ; recordStore(vAddr, val, 8) 3086 } 3087 case None => signalAddressException(Store_AMO_Fault, vAddr) 3088 } 3089} 3090 3091----------------------------------- 3092-- AMOMAXU.W [aq,rl] rd, rs1, rs2 3093----------------------------------- 3094define AMO > AMOMAXU_W(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 3095{ vAddr = GPR(rs1) 3096; if vAddr<1:0> != 0 3097 then signalAddressException(AMO_Misaligned, vAddr) 3098 else match translateAddr(vAddr, Data, Write) 3099 { case Some(pAddr) => { memv = SignExtend(rawReadData(pAddr)<31:0>) 3100 ; data = GPR(rs2) 3101 ; GPR(rd) <- memv 3102 ; val = Max(data, memv) 3103 ; rawWriteData(pAddr, val, 4) 3104 ; recordLoad(vAddr, memv) 3105 ; recordStore(vAddr, val, 4) 3106 } 3107 case None => signalAddressException(Store_AMO_Fault, vAddr) 3108 } 3109} 3110 3111----------------------------------- 3112-- AMOMAXU.D [aq,rl] rd, rs1, rs2 3113----------------------------------- 3114define AMO > AMOMAXU_D(aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 3115{ vAddr = GPR(rs1) 3116; if vAddr<2:0> != 0 3117 then signalAddressException(AMO_Misaligned, vAddr) 3118 else match translateAddr(vAddr, Data, Write) 3119 { case Some(pAddr) => { memv = rawReadData(pAddr) 3120 ; data = GPR(rs2) 3121 ; GPR(rd) <- memv 3122 ; val = Max(data, memv) 3123 ; rawWriteData(pAddr, val, 8) 3124 ; recordLoad(vAddr, memv) 3125 ; recordStore(vAddr, val, 8) 3126 } 3127 case None => signalAddressException(Store_AMO_Fault, vAddr) 3128 } 3129} 3130 3131 3132--------------------------------------------------------------------------- 3133-- Floating Point Instructions (Single Precision) 3134--------------------------------------------------------------------------- 3135 3136-- Load/Store 3137 3138----------------------------------- 3139-- FLW rd, rs2, offs 3140----------------------------------- 3141 3142define FPLoad > FLW(rd::reg, rs1::reg, offs::imm12) = 3143{ vAddr = GPR(rs1) + SignExtend(offs) 3144; match translateAddr(vAddr, Data, Read) 3145 { case Some(pAddr) => { val = rawReadData(pAddr)<31:0> 3146 ; FPRS(rd) <- val 3147 ; recordLoad(vAddr, ZeroExtend(val)) 3148 } 3149 case None => signalAddressException(Load_Fault, vAddr) 3150 } 3151} 3152 3153----------------------------------- 3154-- FSW rs1, rs2, offs 3155----------------------------------- 3156 3157define FPStore > FSW(rs1::reg, rs2::reg, offs::imm12) = 3158{ vAddr = GPR(rs1) + SignExtend(offs) 3159; match translateAddr(vAddr, Data, Write) 3160 { case Some(pAddr) => { data = FPRS(rs2) 3161 ; rawWriteData(pAddr, ZeroExtend(data), 4) 3162 ; recordStore(vAddr, ZeroExtend(data), 4) 3163 } 3164 case None => signalAddressException(Store_AMO_Fault, vAddr) 3165 } 3166} 3167 3168-- Computational 3169 3170-- TODO: Check for underflow after all rounding 3171 3172----------------------------------- 3173-- FADD.S rd, rs1, rs2 3174----------------------------------- 3175 3176define FArith > FADD_S(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3177{ match round(fprnd) 3178 { case Some(r) => writeFPRS(rd, FP32_Add(r, FPRS(rs1), FPRS(rs2))) 3179 case None => signalException(Illegal_Instr) 3180 } 3181} 3182 3183----------------------------------- 3184-- FSUB.S rd, rs1, rs2 3185----------------------------------- 3186 3187define FArith > FSUB_S(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3188{ match round(fprnd) 3189 { case Some(r) => writeFPRS(rd, FP32_Sub(r, FPRS(rs1), FPRS(rs2))) 3190 case None => signalException(Illegal_Instr) 3191 } 3192} 3193 3194----------------------------------- 3195-- FMUL.S rd, rs1, rs2 3196----------------------------------- 3197 3198define FArith > FMUL_S(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3199{ match round(fprnd) 3200 { case Some(r) => writeFPRS(rd, FP32_Mul(r, FPRS(rs1), FPRS(rs2))) 3201 case None => signalException(Illegal_Instr) 3202 } 3203} 3204 3205----------------------------------- 3206-- FDIV.S rd, rs1, rs2 3207----------------------------------- 3208 3209define FArith > FDIV_S(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3210{ match round(fprnd) 3211 { case Some(r) => writeFPRS(rd, FP32_Div(r, FPRS(rs1), FPRS(rs2))) 3212 case None => signalException(Illegal_Instr) 3213 } 3214} 3215 3216----------------------------------- 3217-- FSQRT.S rd, rs 3218----------------------------------- 3219 3220define FArith > FSQRT_S(rd::reg, rs::reg, fprnd::fprnd) = 3221{ match round(fprnd) 3222 { case Some(r) => writeFPRS(rd, FP32_Sqrt(r, FPRS(rs))) 3223 case None => signalException(Illegal_Instr) 3224 } 3225} 3226 3227----------------------------------- 3228-- FMIN.S rd, rs1, rs2 3229----------------------------------- 3230define FArith > FMIN_S(rd::reg, rs1::reg, rs2::reg) = 3231{ f1 = FPRS(rs1) 3232; f2 = FPRS(rs2) 3233; res = match FP32_Compare(f1, f2) 3234 { case FP_LT => f1 3235 case FP_EQ => f1 3236 case FP_GT => f2 3237 case FP_UN => if ( (FP32_IsSignalingNan(f1) or FP32_IsSignalingNan(f2)) 3238 or (f1 == RV32_CanonicalNan and f2 == RV32_CanonicalNan)) 3239 then RV32_CanonicalNan 3240 else -- either f1 or f2 should be a quiet NaN 3241 if f1 == RV32_CanonicalNan then f2 else f1 3242 } 3243; writeFPRS(rd, res) 3244} 3245 3246----------------------------------- 3247-- FMAX.S rd, rs1, rs2 3248----------------------------------- 3249define FArith > FMAX_S(rd::reg, rs1::reg, rs2::reg) = 3250{ f1 = FPRS(rs1) 3251; f2 = FPRS(rs2) 3252; res = match FP32_Compare(f1, f2) 3253 { case FP_LT => f2 3254 case FP_EQ => f2 3255 case FP_GT => f1 3256 case FP_UN => if ( (FP32_IsSignalingNan(f1) or FP32_IsSignalingNan(f2)) 3257 or (f1 == RV32_CanonicalNan and f2 == RV32_CanonicalNan)) 3258 then RV32_CanonicalNan 3259 else -- either f1 or f2 should be a quiet NaN 3260 if f1 == RV32_CanonicalNan then f2 else f1 3261 } 3262; writeFPRS(rd, res) 3263} 3264 3265----------------------------------- 3266-- FMADD.S rd, rs1, rs2, rs3 3267----------------------------------- 3268 3269define FArith > FMADD_S(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3270{ match round(fprnd) 3271 { case Some(r) => writeFPRS(rd, FP32_Add(r, FP32_Mul(r, FPRS(rs1), FPRS(rs2)), FPRS(rs3))) 3272 case None => signalException(Illegal_Instr) 3273 } 3274} 3275 3276----------------------------------- 3277-- FMSUB.S rd, rs1, rs2, rs3 3278----------------------------------- 3279 3280define FArith > FMSUB_S(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3281{ match round(fprnd) 3282 { case Some(r) => writeFPRS(rd, FP32_Sub(r, FP32_Mul(r, FPRS(rs1), FPRS(rs2)), FPRS(rs3))) 3283 case None => signalException(Illegal_Instr) 3284 } 3285} 3286 3287----------------------------------- 3288-- FNMADD.S rd, rs1, rs2, rs3 3289----------------------------------- 3290 3291define FArith > FNMADD_S(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3292{ match round(fprnd) 3293 { case Some(r) => writeFPRS(rd, FP32_Neg(FP32_Add(r, FP32_Mul(r, FPRS(rs1), FPRS(rs2)), FPRS(rs3)))) 3294 case None => signalException(Illegal_Instr) 3295 } 3296} 3297 3298----------------------------------- 3299-- FNMSUB.S rd, rs1, rs2, rs3 3300----------------------------------- 3301 3302define FArith > FNMSUB_S(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3303{ match round(fprnd) 3304 { case Some(r) => writeFPRS(rd, FP32_Neg(FP32_Sub(r, FP32_Mul(r, FPRS(rs1), FPRS(rs2)), FPRS(rs3)))) 3305 case None => signalException(Illegal_Instr) 3306 } 3307} 3308 3309-- Conversions 3310 3311----------------------------------- 3312-- FCVT.S.W rd, rs 3313----------------------------------- 3314 3315define FConv > FCVT_S_W(rd::reg, rs::reg, fprnd::fprnd) = 3316{ match round(fprnd) 3317 { case Some(r) => writeFPRS(rd, FP32_FromInt(r, [GPR(rs)<31:0>]::int)) 3318 case None => signalException(Illegal_Instr) 3319 } 3320} 3321 3322----------------------------------- 3323-- FCVT.S.WU rd, rs 3324----------------------------------- 3325 3326define FConv > FCVT_S_WU(rd::reg, rs::reg, fprnd::fprnd) = 3327{ match round(fprnd) 3328 { case Some(r) => writeFPRS(rd, FP32_FromInt(r, [0`1 : GPR(rs)<31:0>]::int)) 3329 case None => signalException(Illegal_Instr) 3330 } 3331} 3332 3333----------------------------------- 3334-- FCVT.W.S rd, rs 3335----------------------------------- 3336 3337define FConv > FCVT_W_S(rd::reg, rs::reg, fprnd::fprnd) = 3338{ match round(fprnd) 3339 { case Some(r) => { inp = FPRS(rs) 3340 ; val = ValOf(FP32_ToInt(r, inp)) 3341 ; res = if FP32_IsNan(inp) or inp == FP32_PosInf 3342 then [0n2 ** 31 - 1] 3343 else if inp == FP32_NegInf 3344 then -[0n2 ** 31] 3345 else if val > 2 ** 31 - 1 3346 then [0n2 ** 31 - 1] 3347 else if val < -2 ** 31 3348 then -[0n2 ** 31] 3349 else [val] 3350 ; writeRD(rd, res) 3351 } 3352 case None => signalException(Illegal_Instr) 3353 } 3354} 3355 3356----------------------------------- 3357-- FCVT.WU.S rd, rs 3358----------------------------------- 3359 3360define FConv > FCVT_WU_S(rd::reg, rs::reg, fprnd::fprnd) = 3361{ match round(fprnd) 3362 { case Some(r) => { inp = FPRS(rs) 3363 ; val = ValOf(FP32_ToInt(r, inp)) 3364 ; res = if FP32_IsNan(inp) or inp == FP32_PosInf 3365 then [0n2 ** 32 - 1] 3366 else if inp == FP32_NegInf 3367 then 0x0 3368 else if val > 2 ** 32 - 1 3369 then [0n2 ** 32 - 1] 3370 else if val < 0 3371 then 0x0 3372 else [val] 3373 ; writeRD(rd, res) 3374 } 3375 case None => signalException(Illegal_Instr) 3376 } 3377} 3378 3379----------------------------------- 3380-- FCVT.S.L rd, rs 3381----------------------------------- 3382 3383define FConv > FCVT_S_L(rd::reg, rs::reg, fprnd::fprnd) = 3384{ match round(fprnd) 3385 { case Some(r) => writeFPRS(rd, FP32_FromInt(r, [GPR(rs)]::int)) 3386 case None => signalException(Illegal_Instr) 3387 } 3388} 3389 3390----------------------------------- 3391-- FCVT.S.LU rd, rs 3392----------------------------------- 3393 3394define FConv > FCVT_S_LU(rd::reg, rs::reg, fprnd::fprnd) = 3395{ match round(fprnd) 3396 { case Some(r) => writeFPRS(rd, FP32_FromInt(r, [0`1 : GPR(rs)]::int)) 3397 case None => signalException(Illegal_Instr) 3398 } 3399} 3400 3401----------------------------------- 3402-- FCVT.L.S rd, rs 3403----------------------------------- 3404 3405define FConv > FCVT_L_S(rd::reg, rs::reg, fprnd::fprnd) = 3406{ match round(fprnd) 3407 { case Some(r) => { inp = FPRS(rs) 3408 ; val = ValOf(FP32_ToInt(r, inp)) 3409 ; res = if FP32_IsNan(inp) or inp == FP32_PosInf 3410 then [0n2 ** 63 - 1] 3411 else if inp == FP32_NegInf 3412 then -[0n2 ** 63] 3413 else if val > 2 ** 63 - 1 3414 then [0n2 ** 63 - 1] 3415 else if val < -2 ** 63 3416 then -[0n2 ** 63] 3417 else [val] 3418 ; writeRD(rd, res) 3419 } 3420 case None => signalException(Illegal_Instr) 3421 } 3422} 3423 3424----------------------------------- 3425-- FCVT.LU.S rd, rs 3426----------------------------------- 3427 3428define FConv > FCVT_LU_S(rd::reg, rs::reg, fprnd::fprnd) = 3429{ match round(fprnd) 3430 { case Some(r) => { inp = FPRS(rs) 3431 ; val = ValOf(FP32_ToInt(r, inp)) 3432 ; res = if FP32_IsNan(inp) or inp == FP32_PosInf 3433 then [0n2 ** 64 - 1] 3434 else if inp == FP32_NegInf 3435 then 0x0 3436 else if val > 2 ** 64 - 1 3437 then [0n2 ** 64 - 1] 3438 else if val < 0 3439 then 0x0 3440 else [val] 3441 ; writeRD(rd, res) 3442 } 3443 case None => signalException(Illegal_Instr) 3444 } 3445} 3446 3447-- Sign injection 3448 3449----------------------------------- 3450-- FSGNJ.S rd, rs 3451----------------------------------- 3452 3453define FConv > FSGNJ_S(rd::reg, rs1::reg, rs2::reg) = 3454{ f1 = FPRS(rs1) 3455; f2 = FPRS(rs2) 3456; writeFPRS(rd, ([FP32_Sign(f2)]::bits(1)):f1<30:0>) 3457} 3458 3459----------------------------------- 3460-- FSGNJN.S rd, rs 3461----------------------------------- 3462 3463define FConv > FSGNJN_S(rd::reg, rs1::reg, rs2::reg) = 3464{ f1 = FPRS(rs1) 3465; f2 = FPRS(rs2) 3466; writeFPRS(rd, ([!FP32_Sign(f2)]::bits(1)):f1<30:0>) 3467} 3468 3469----------------------------------- 3470-- FSGNJX.S rd, rs 3471----------------------------------- 3472 3473define FConv > FSGNJX_S(rd::reg, rs1::reg, rs2::reg) = 3474{ f1 = FPRS(rs1) 3475; f2 = FPRS(rs2) 3476; writeFPRS(rd, ([FP32_Sign(f2)]::bits(1) ?? [FP32_Sign(f1)]::bits(1)) : f1<30:0>) 3477} 3478 3479-- Movement 3480 3481----------------------------------- 3482-- FMV.X.S rd, rs 3483----------------------------------- 3484 3485define FConv > FMV_X_S(rd::reg, rs::reg) = 3486 GPR(rd) <- SignExtend(FPRS(rs)) 3487 3488----------------------------------- 3489-- FMV.S.X rd, rs 3490----------------------------------- 3491 3492define FConv > FMV_S_X(rd::reg, rs::reg) = 3493 writeFPRS(rd, GPR(rs)<31:0>) 3494 3495-- Comparisons 3496 3497----------------------------------- 3498-- FEQ.S rd, rs 3499----------------------------------- 3500 3501define FArith > FEQ_S(rd::reg, rs1::reg, rs2::reg) = 3502{ f1 = FPRS(rs1) 3503; f2 = FPRS(rs2) 3504; if FP32_IsSignalingNan(f1) or FP32_IsSignalingNan(f2) 3505 then { writeRD(rd, 0x0) 3506 ; setFP_Invalid() 3507 } 3508 else { res = match FP32_Compare(f1, f2) 3509 { case FP_LT => 0x0 3510 case FP_EQ => 0x1 3511 case FP_GT => 0x0 3512 case FP_UN => 0x0 3513 } 3514 ; writeRD(rd, res) 3515 } 3516} 3517 3518----------------------------------- 3519-- FLT.S rd, rs 3520----------------------------------- 3521 3522define FArith > FLT_S(rd::reg, rs1::reg, rs2::reg) = 3523{ f1 = FPRS(rs1) 3524; f2 = FPRS(rs2) 3525; if FP32_IsNan(f1) or FP32_IsNan(f2) 3526 then { writeRD(rd, 0x0) 3527 ; setFP_Invalid() 3528 } 3529 else { res = match FP32_Compare(f1, f2) 3530 { case FP_LT => 0x1 3531 case FP_EQ => 0x0 3532 case FP_GT => 0x0 3533 case FP_UN => 0x0 3534 } 3535 ; writeRD(rd, res) 3536 } 3537 } 3538 3539----------------------------------- 3540-- FLE.S rd, rs 3541----------------------------------- 3542 3543define FArith > FLE_S(rd::reg, rs1::reg, rs2::reg) = 3544{ f1 = FPRS(rs1) 3545; f2 = FPRS(rs2) 3546; if FP32_IsNan(f1) or FP32_IsNan(f2) 3547 then { writeRD(rd, 0x0) 3548 ; setFP_Invalid() 3549 } 3550 else { res = match FP32_Compare(f1, f2) 3551 { case FP_LT => 0x1 3552 case FP_EQ => 0x1 3553 case FP_GT => 0x0 3554 case FP_UN => 0x0 3555 } 3556 ; writeRD(rd, res) 3557 } 3558} 3559 3560-- Classification 3561 3562----------------------------------- 3563-- FCLASS.S rd, rs 3564----------------------------------- 3565 3566define FConv > FCLASS_S(rd::reg, rs::reg) = 3567{ var ret = 0x0`10 3568; val = FPRS(rs) 3569; ret<0> <- val == FP32_NegInf 3570; ret<1> <- FP32_Sign(val) and FP32_IsNormal(val) 3571; ret<2> <- FP32_Sign(val) and FP32_IsSubnormal(val) 3572; ret<3> <- val == FP32_NegZero 3573; ret<4> <- val == FP32_PosZero 3574; ret<5> <- !FP32_Sign(val) and FP32_IsSubnormal(val) 3575; ret<6> <- !FP32_Sign(val) and FP32_IsNormal(val) 3576; ret<7> <- val == FP32_PosInf 3577; ret<8> <- FP32_IsSignalingNan(val) 3578; ret<9> <- val == RV32_CanonicalNan 3579; writeRD(rd, ZeroExtend(ret)) 3580} 3581 3582--------------------------------------------------------------------------- 3583-- Floating Point Instructions (Double Precision) 3584--------------------------------------------------------------------------- 3585 3586-- Load/Store 3587 3588----------------------------------- 3589-- FLD rd, rs2, offs 3590----------------------------------- 3591 3592define FPLoad > FLD(rd::reg, rs1::reg, offs::imm12) = 3593{ vAddr = GPR(rs1) + SignExtend(offs) 3594; match translateAddr(vAddr, Data, Read) 3595 { case Some(pAddr) => { val = rawReadData(pAddr) 3596 ; FPRD(rd) <- val 3597 ; recordLoad(vAddr, val) 3598 } 3599 case None => signalAddressException(Load_Fault, vAddr) 3600 } 3601} 3602 3603----------------------------------- 3604-- FSD rs1, rs2, offs 3605----------------------------------- 3606 3607define FPStore > FSD(rs1::reg, rs2::reg, offs::imm12) = 3608{ vAddr = GPR(rs1) + SignExtend(offs) 3609; match translateAddr(vAddr, Data, Write) 3610 { case Some(pAddr) => { data = FPRD(rs2) 3611 ; rawWriteData(pAddr, data, 8) 3612 ; recordStore(vAddr, data, 8) 3613 } 3614 case None => signalAddressException(Store_AMO_Fault, vAddr) 3615 } 3616} 3617 3618-- Computational 3619 3620-- TODO: Check for underflow after all rounding 3621 3622----------------------------------- 3623-- FADD.D rd, rs1, rs2 3624----------------------------------- 3625 3626define FArith > FADD_D(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3627{ match round(fprnd) 3628 { case Some(r) => writeFPRD(rd, FP64_Add(r, FPRD(rs1), FPRD(rs2))) 3629 case None => signalException(Illegal_Instr) 3630 } 3631} 3632 3633----------------------------------- 3634-- FSUB.D rd, rs1, rs2 3635----------------------------------- 3636 3637define FArith > FSUB_D(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3638{ match round(fprnd) 3639 { case Some(r) => writeFPRD(rd, FP64_Sub(r, FPRD(rs1), FPRD(rs2))) 3640 case None => signalException(Illegal_Instr) 3641 } 3642} 3643 3644----------------------------------- 3645-- FMUL.D rd, rs1, rs2 3646----------------------------------- 3647 3648define FArith > FMUL_D(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3649{ match round(fprnd) 3650 { case Some(r) => writeFPRD(rd, FP64_Mul(r, FPRD(rs1), FPRD(rs2))) 3651 case None => signalException(Illegal_Instr) 3652 } 3653} 3654 3655----------------------------------- 3656-- FDIV.D rd, rs1, rs2 3657----------------------------------- 3658 3659define FArith > FDIV_D(rd::reg, rs1::reg, rs2::reg, fprnd::fprnd) = 3660{ match round(fprnd) 3661 { case Some(r) => writeFPRD(rd, FP64_Div(r, FPRD(rs1), FPRD(rs2))) 3662 case None => signalException(Illegal_Instr) 3663 } 3664} 3665 3666----------------------------------- 3667-- FSQRT.D rd, rs 3668----------------------------------- 3669 3670define FArith > FSQRT_D(rd::reg, rs::reg, fprnd::fprnd) = 3671{ match round(fprnd) 3672 { case Some(r) => writeFPRD(rd, FP64_Sqrt(r, FPRD(rs))) 3673 case None => signalException(Illegal_Instr) 3674 } 3675} 3676 3677----------------------------------- 3678-- FMIN.D rd, rs1, rs2 3679----------------------------------- 3680define FArith > FMIN_D(rd::reg, rs1::reg, rs2::reg) = 3681{ f1 = FPRD(rs1) 3682; f2 = FPRD(rs2) 3683; res = match FP64_Compare(f1, f2) 3684 { case FP_LT => f1 3685 case FP_EQ => f1 3686 case FP_GT => f2 3687 case FP_UN => if ( (FP64_IsSignalingNan(f1) or FP64_IsSignalingNan(f2)) 3688 or (f1 == RV64_CanonicalNan and f2 == RV64_CanonicalNan)) 3689 then RV64_CanonicalNan 3690 else -- either f1 or f2 should be a quiet NaN 3691 if f1 == RV64_CanonicalNan then f2 else f1 3692 3693 } 3694; writeFPRD(rd, res) 3695} 3696 3697----------------------------------- 3698-- FMAX.D rd, rs1, rs2 3699----------------------------------- 3700define FArith > FMAX_D(rd::reg, rs1::reg, rs2::reg) = 3701{ f1 = FPRD(rs1) 3702; f2 = FPRD(rs2) 3703; res = match FP64_Compare(f1, f2) 3704 { case FP_LT => f2 3705 case FP_EQ => f2 3706 case FP_GT => f1 3707 case FP_UN => if ( (FP64_IsSignalingNan(f1) or FP64_IsSignalingNan(f2)) 3708 or (f1 == RV64_CanonicalNan and f2 == RV64_CanonicalNan)) 3709 then RV64_CanonicalNan 3710 else -- either f1 or f2 should be a quiet NaN 3711 if f1 == RV64_CanonicalNan then f2 else f1 3712 } 3713; writeFPRD(rd, res) 3714} 3715 3716----------------------------------- 3717-- FMADD.D rd, rs1, rs2, rs3 3718----------------------------------- 3719 3720define FArith > FMADD_D(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3721{ match round(fprnd) 3722 { case Some(r) => writeFPRD(rd, FP64_Add(r, FP64_Mul(r, FPRD(rs1), FPRD(rs2)), FPRD(rs3))) 3723 case None => signalException(Illegal_Instr) 3724 } 3725} 3726 3727----------------------------------- 3728-- FMSUB.D rd, rs1, rs2, rs3 3729----------------------------------- 3730 3731define FArith > FMSUB_D(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3732{ match round(fprnd) 3733 { case Some(r) => writeFPRD(rd, FP64_Sub(r, FP64_Mul(r, FPRD(rs1), FPRD(rs2)), FPRD(rs3))) 3734 case None => signalException(Illegal_Instr) 3735 } 3736} 3737 3738----------------------------------- 3739-- FNMADD.D rd, rs1, rs2, rs3 3740----------------------------------- 3741 3742define FArith > FNMADD_D(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3743{ match round(fprnd) 3744 { case Some(r) => writeFPRD(rd, FP64_Neg(FP64_Add(r, FP64_Mul(r, FPRD(rs1), FPRD(rs2)), FPRD(rs3)))) 3745 case None => signalException(Illegal_Instr) 3746 } 3747} 3748 3749----------------------------------- 3750-- FNMSUB.D rd, rs1, rs2, rs3 3751----------------------------------- 3752 3753define FArith > FNMSUB_D(rd::reg, rs1::reg, rs2::reg, rs3::reg, fprnd::fprnd) = 3754{ match round(fprnd) 3755 { case Some(r) => writeFPRD(rd, FP64_Neg(FP64_Sub(r, FP64_Mul(r, FPRD(rs1), FPRD(rs2)), FPRD(rs3)))) 3756 case None => signalException(Illegal_Instr) 3757 } 3758} 3759 3760-- Conversions 3761 3762----------------------------------- 3763-- FCVT.D.W rd, rs 3764----------------------------------- 3765 3766define FConv > FCVT_D_W(rd::reg, rs::reg, fprnd::fprnd) = 3767{ match round(fprnd) 3768 { case Some(r) => writeFPRD(rd, FP64_FromInt(r, [GPR(rs)<31:0>]::int)) 3769 case None => signalException(Illegal_Instr) 3770 } 3771} 3772 3773----------------------------------- 3774-- FCVT.D.WU rd, rs 3775----------------------------------- 3776 3777define FConv > FCVT_D_WU(rd::reg, rs::reg, fprnd::fprnd) = 3778{ match round(fprnd) 3779 { case Some(r) => writeFPRD(rd, FP64_FromInt(r, [0`1 : GPR(rs)<31:0>]::int)) 3780 case None => signalException(Illegal_Instr) 3781 } 3782} 3783 3784----------------------------------- 3785-- FCVT.W.D rd, rs 3786----------------------------------- 3787 3788define FConv > FCVT_W_D(rd::reg, rs::reg, fprnd::fprnd) = 3789{ match round(fprnd) 3790 { case Some(r) => { inp = FPRD(rs) 3791 ; val = ValOf(FP64_ToInt(r, inp)) 3792 ; res = if FP64_IsNan(inp) or inp == FP64_PosInf 3793 then [0n2 ** 31 - 1] 3794 else if inp == FP64_NegInf 3795 then -[0n2 ** 31] 3796 else if val > 2 ** 31 - 1 3797 then [0n2 ** 31 - 1] 3798 else if val < -2 ** 31 3799 then -[0n2 ** 31] 3800 else [val] 3801 ; writeRD(rd, res) 3802 } 3803 case None => signalException(Illegal_Instr) 3804 } 3805} 3806 3807----------------------------------- 3808-- FCVT.WU.D rd, rs 3809----------------------------------- 3810 3811define FConv > FCVT_WU_D(rd::reg, rs::reg, fprnd::fprnd) = 3812{ match round(fprnd) 3813 { case Some(r) => { inp = FPRD(rs) 3814 ; val = ValOf(FP64_ToInt(r, inp)) 3815 ; res = if FP64_IsNan(inp) or inp == FP64_PosInf 3816 then [0n2 ** 32 - 1] 3817 else if inp == FP64_NegInf 3818 then 0x0 3819 else if val > 2 ** 32 - 1 3820 then [0n2 ** 32 - 1] 3821 else if val < 0 3822 then 0x0 3823 else [val] 3824 ; writeRD(rd, res) 3825 } 3826 case None => signalException(Illegal_Instr) 3827 } 3828} 3829 3830----------------------------------- 3831-- FCVT.D.L rd, rs 3832----------------------------------- 3833 3834define FConv > FCVT_D_L(rd::reg, rs::reg, fprnd::fprnd) = 3835{ match round(fprnd) 3836 { case Some(r) => writeFPRD(rd, FP64_FromInt(r, [GPR(rs)]::int)) 3837 case None => signalException(Illegal_Instr) 3838 } 3839} 3840 3841----------------------------------- 3842-- FCVT.D.LU rd, rs 3843----------------------------------- 3844 3845define FConv > FCVT_D_LU(rd::reg, rs::reg, fprnd::fprnd) = 3846{ match round(fprnd) 3847 { case Some(r) => writeFPRD(rd, FP64_FromInt(r, [0`1 : GPR(rs)]::int)) 3848 case None => signalException(Illegal_Instr) 3849 } 3850} 3851 3852----------------------------------- 3853-- FCVT.L.D rd, rs 3854----------------------------------- 3855 3856define FConv > FCVT_L_D(rd::reg, rs::reg, fprnd::fprnd) = 3857{ match round(fprnd) 3858 { case Some(r) => { inp = FPRD(rs) 3859 ; val = ValOf(FP64_ToInt(r, inp)) 3860 ; res = if FP64_IsNan(inp) or inp == FP64_PosInf 3861 then [0n2 ** 63 - 1] 3862 else if inp == FP64_NegInf 3863 then -[0n2 ** 63] 3864 else if val > 2 ** 63 - 1 3865 then [0n2 ** 63 - 1] 3866 else if val < -2 ** 63 3867 then -[0n2 ** 63] 3868 else [val] 3869 ; writeRD(rd, res) 3870 } 3871 case None => signalException(Illegal_Instr) 3872 } 3873} 3874 3875----------------------------------- 3876-- FCVT.LU.D rd, rs 3877----------------------------------- 3878 3879define FConv > FCVT_LU_D(rd::reg, rs::reg, fprnd::fprnd) = 3880{ match round(fprnd) 3881 { case Some(r) => { inp = FPRD(rs) 3882 ; val = ValOf(FP64_ToInt(r, inp)) 3883 ; res = if FP64_IsNan(inp) or inp == FP64_PosInf 3884 then [0n2 ** 64 - 1] 3885 else if inp == FP64_NegInf 3886 then 0x0 3887 else if val > 2 ** 64 - 1 3888 then [0n2 ** 64 - 1] 3889 else if val < 0 3890 then 0x0 3891 else [val] 3892 ; writeRD(rd, res) 3893 } 3894 case None => signalException(Illegal_Instr) 3895 } 3896} 3897 3898----------------------------------- 3899-- FCVT.S.D rd, rs 3900----------------------------------- 3901 3902define FConv > FCVT_S_D(rd::reg, rs::reg, fprnd::fprnd) = 3903{ match round(fprnd) 3904 { case Some(r) => writeFPRS(rd, FP64_ToFP32(r, FPRD(rs))) 3905 case None => signalException(Illegal_Instr) 3906 } 3907} 3908 3909----------------------------------- 3910-- FCVT.D.S rd, rs 3911----------------------------------- 3912 3913define FConv > FCVT_D_S(rd::reg, rs::reg, fprnd::fprnd) = 3914{ match round(fprnd) 3915 { case Some(r) => writeFPRD(rd, FP32_ToFP64(FPRS(rs))) 3916 case None => signalException(Illegal_Instr) 3917 } 3918} 3919 3920-- Sign injection 3921 3922----------------------------------- 3923-- FSGNJ.D rd, rs 3924----------------------------------- 3925 3926define FConv > FSGNJ_D(rd::reg, rs1::reg, rs2::reg) = 3927{ f1 = FPRD(rs1) 3928; f2 = FPRD(rs2) 3929; writeFPRD(rd, ([FP64_Sign(f2)]::bits(1)):f1<62:0>) 3930} 3931 3932----------------------------------- 3933-- FSGNJN.D rd, rs 3934----------------------------------- 3935 3936define FConv > FSGNJN_D(rd::reg, rs1::reg, rs2::reg) = 3937{ f1 = FPRD(rs1) 3938; f2 = FPRD(rs2) 3939; writeFPRD(rd, ([!FP64_Sign(f2)]::bits(1)):f1<62:0>) 3940} 3941 3942----------------------------------- 3943-- FSGNJX.D rd, rs 3944----------------------------------- 3945 3946define FConv > FSGNJX_D(rd::reg, rs1::reg, rs2::reg) = 3947{ f1 = FPRD(rs1) 3948; f2 = FPRD(rs2) 3949; writeFPRD(rd, ([FP64_Sign(f2)]::bits(1) ?? [FP64_Sign(f1)]::bits(1)) : f1<62:0>) 3950} 3951 3952-- Movement 3953 3954----------------------------------- 3955-- FMV.X.D rd, rs 3956----------------------------------- 3957 3958define FConv > FMV_X_D(rd::reg, rs::reg) = 3959 GPR(rd) <- SignExtend(FPRD(rs)) 3960 3961----------------------------------- 3962-- FMV.D.X rd, rs 3963----------------------------------- 3964 3965define FConv > FMV_D_X(rd::reg, rs::reg) = 3966 writeFPRD(rd, GPR(rs)) 3967 3968-- Comparisons 3969 3970----------------------------------- 3971-- FEQ.D rd, rs 3972----------------------------------- 3973 3974define FArith > FEQ_D(rd::reg, rs1::reg, rs2::reg) = 3975{ f1 = FPRD(rs1) 3976; f2 = FPRD(rs2) 3977; if FP64_IsSignalingNan(f1) or FP64_IsSignalingNan(f2) 3978 then { writeRD(rd, 0x0) 3979 ; setFP_Invalid() 3980 } 3981 else { res = match FP64_Compare(f1, f2) 3982 { case FP_LT => 0x0 3983 case FP_EQ => 0x1 3984 case FP_GT => 0x0 3985 case FP_UN => 0x0 3986 } 3987 ; writeRD(rd, res) 3988 } 3989} 3990 3991----------------------------------- 3992-- FLT.D rd, rs 3993----------------------------------- 3994 3995define FArith > FLT_D(rd::reg, rs1::reg, rs2::reg) = 3996{ f1 = FPRD(rs1) 3997; f2 = FPRD(rs2) 3998; if FP64_IsNan(f1) or FP64_IsNan(f2) 3999 then { writeRD(rd, 0x0) 4000 ; setFP_Invalid() 4001 } 4002 else { res = match FP64_Compare(f1, f2) 4003 { case FP_LT => 0x1 4004 case FP_EQ => 0x0 4005 case FP_GT => 0x0 4006 case FP_UN => 0x0 4007 } 4008 ; writeRD(rd, res) 4009 } 4010} 4011 4012----------------------------------- 4013-- FLE.D rd, rs 4014----------------------------------- 4015 4016define FArith > FLE_D(rd::reg, rs1::reg, rs2::reg) = 4017{ f1 = FPRD(rs1) 4018; f2 = FPRD(rs2) 4019; if FP64_IsNan(f1) or FP64_IsNan(f2) 4020 then { writeRD(rd, 0x0) 4021 ; setFP_Invalid() 4022 } 4023 else { res = match FP64_Compare(f1, f2) 4024 { case FP_LT => 0x1 4025 case FP_EQ => 0x1 4026 case FP_GT => 0x0 4027 case FP_UN => 0x0 4028 } 4029 ; writeRD(rd, res) 4030 } 4031} 4032 4033-- Classification 4034 4035----------------------------------- 4036-- FCLASS.D rd, rs 4037----------------------------------- 4038 4039define FConv > FCLASS_D(rd::reg, rs::reg) = 4040{ var ret = 0x0`10 4041; val = FPRD(rs) 4042; ret<0> <- val == FP64_NegInf 4043; ret<1> <- FP64_Sign(val) and FP64_IsNormal(val) 4044; ret<2> <- FP64_Sign(val) and FP64_IsSubnormal(val) 4045; ret<3> <- val == FP64_NegZero 4046; ret<4> <- val == FP64_PosZero 4047; ret<5> <- !FP64_Sign(val) and FP64_IsSubnormal(val) 4048; ret<6> <- !FP64_Sign(val) and FP64_IsNormal(val) 4049; ret<7> <- val == FP64_PosInf 4050; ret<8> <- FP64_IsSignalingNan(val) 4051; ret<9> <- val == RV64_CanonicalNan 4052; writeRD(rd, ZeroExtend(ret)) 4053} 4054 4055--------------------------------------------------------------------------- 4056-- System Instructions 4057--------------------------------------------------------------------------- 4058 4059----------------------------------- 4060-- ECALL 4061----------------------------------- 4062define System > ECALL = signalEnvCall() 4063 4064----------------------------------- 4065-- EBREAK 4066----------------------------------- 4067 4068define System > EBREAK = signalException(Breakpoint) 4069 4070----------------------------------- 4071-- ERET 4072----------------------------------- 4073define System > ERET = 4074 NextFetch <- Some(Ereturn) 4075 4076----------------------------------- 4077-- MRTS 4078----------------------------------- 4079define System > MRTS = 4080{ SCSR.scause <- MCSR.mcause 4081; SCSR.sbadaddr <- MCSR.mbadaddr 4082; SCSR.sepc <- MCSR.mepc 4083 4084; MCSR.mstatus.MPRV <- privLevel(Supervisor) 4085 4086; NextFetch <- Some(Mrts) 4087} 4088 4089----------------------------------- 4090-- WFI 4091----------------------------------- 4092define System > WFI = nothing 4093 4094-- Control and Status Registers 4095 4096bool checkCSROp(csr::imm12, rs1::reg, a::accessType) = 4097 is_CSR_defined(csr) and check_CSR_access(csrRW(csr), csrPR(csr), curPrivilege(), a) 4098 4099----------------------------------- 4100-- CSRRW rd, rs1, imm 4101----------------------------------- 4102define System > CSRRW(rd::reg, rs1::reg, csr::imm12) = 4103 if checkCSROp(csr, rs1, Write) 4104 then { val = CSR(csr) 4105 ; writeCSR(csr, GPR(rs1)) 4106 ; writeRD(rd, val) 4107 } 4108 else signalException(Illegal_Instr) 4109 4110----------------------------------- 4111-- CSRRS rd, rs1, imm 4112----------------------------------- 4113define System > CSRRS(rd::reg, rs1::reg, csr::imm12) = 4114 if checkCSROp(csr, rs1, if rs1 == 0 then Read else Write) 4115 then { val = CSR(csr) 4116 ; when rs1 != 0 4117 do writeCSR(csr, val || GPR(rs1)) 4118 ; writeRD(rd, val) 4119 } 4120 else signalException(Illegal_Instr) 4121 4122----------------------------------- 4123-- CSRRC rd, rs1, imm 4124----------------------------------- 4125define System > CSRRC(rd::reg, rs1::reg, csr::imm12) = 4126 if checkCSROp(csr, rs1, if rs1 == 0 then Read else Write) 4127 then { val = CSR(csr) 4128 ; when rs1 != 0 4129 do writeCSR(csr, val && ~GPR(rs1)) 4130 ; writeRD(rd, val) 4131 } 4132 else signalException(Illegal_Instr) 4133 4134----------------------------------- 4135-- CSRRWI rd, rs1, imm 4136----------------------------------- 4137define System > CSRRWI(rd::reg, zimm::reg, csr::imm12) = 4138 if checkCSROp(csr, zimm, if zimm == 0 then Read else Write) 4139 then { val = CSR(csr) 4140 ; when zimm != 0 4141 do writeCSR(csr, ZeroExtend(zimm)) 4142 ; writeRD(rd, val) 4143 } 4144 else signalException(Illegal_Instr) 4145 4146----------------------------------- 4147-- CSRRSI rd, rs1, imm 4148----------------------------------- 4149define System > CSRRSI(rd::reg, zimm::reg, csr::imm12) = 4150 if checkCSROp(csr, zimm, if zimm == 0 then Read else Write) 4151 then { val = CSR(csr) 4152 ; when zimm != 0 4153 do writeCSR(csr, val || ZeroExtend(zimm)) 4154 ; writeRD(rd, val) 4155 } 4156 else signalException(Illegal_Instr) 4157 4158----------------------------------- 4159-- CSRRCI rd, rs1, imm 4160----------------------------------- 4161define System > CSRRCI(rd::reg, zimm::reg, csr::imm12) = 4162 if checkCSROp(csr, zimm, if zimm == 0 then Read else Write) 4163 then { val = CSR(csr) 4164 ; when zimm != 0 4165 do writeCSR(csr, val && ~ZeroExtend(zimm)) 4166 ; writeRD(rd, val) 4167 } 4168 else signalException(Illegal_Instr) 4169 4170-- Address translation cache flush 4171 4172----------------------------------- 4173-- SFENCE.VM 4174----------------------------------- 4175define System > SFENCE_VM(rs1::reg) = 4176{ addr = if rs1 == 0 then None else Some(GPR(rs1)) 4177; TLB <- flushTLB(curASID(), addr, TLB) 4178} 4179 4180----------------------------------- 4181-- Unsupported instructions 4182----------------------------------- 4183define UnknownInstruction = 4184 signalException(Illegal_Instr) 4185 4186----------------------------------- 4187-- Internal pseudo-instructions 4188----------------------------------- 4189 4190-- The argument is the value from the PC. 4191 4192define Internal > FETCH_MISALIGNED(addr::regType) = 4193{ signalAddressException(Fetch_Misaligned, [addr]) 4194; recordFetchException(addr) 4195} 4196 4197define Internal > FETCH_FAULT(addr::regType) = 4198{ signalAddressException(Fetch_Fault, [addr]) 4199; recordFetchException(addr) 4200} 4201 4202define Run 4203 4204-------------------------------------------------- 4205-- Instruction fetch 4206-------------------------------------------------- 4207 4208construct FetchResult 4209{ F_Error :: instruction 4210, F_Result :: rawInstType 4211} 4212 4213FetchResult Fetch() = 4214{ vPC = PC 4215; if vPC<0> 4216 then F_Error(Internal(FETCH_MISALIGNED(vPC))) 4217 else match translateAddr(vPC, Instruction, Read) 4218 { case Some(pPC) => { instw = rawReadInst(pPC) 4219 ; setupDelta(vPC, instw) 4220 ; F_Result(instw) 4221 } 4222 case None => F_Error(Internal(FETCH_FAULT(vPC))) 4223 } 4224} 4225 4226--------------------------------------------------------------------------- 4227-- Instruction decoding 4228--------------------------------------------------------------------------- 4229 4230-- helpers to assemble various immediates from their pieces 4231imm12 asImm12(imm12::bits(1), imm11::bits(1), immhi::bits(6), immlo::bits(4)) = 4232 imm12 : imm11 : immhi : immlo 4233 4234imm20 asImm20(imm20::bits(1), immhi::bits(8), imm11::bits(1), immlo::bits(10)) = 4235 imm20 : immhi : imm11 : immlo 4236 4237imm12 asSImm12(immhi::bits(7), immlo::bits(5)) = immhi : immlo 4238 4239instruction Decode(w::word) = 4240 match w 4241 { case 'i12 ihi rs2 rs1 000 ilo i11 11000 11' => Branch( BEQ(rs1, rs2, asImm12(i12, i11, ihi, ilo))) 4242 case 'i12 ihi rs2 rs1 001 ilo i11 11000 11' => Branch( BNE(rs1, rs2, asImm12(i12, i11, ihi, ilo))) 4243 case 'i12 ihi rs2 rs1 100 ilo i11 11000 11' => Branch( BLT(rs1, rs2, asImm12(i12, i11, ihi, ilo))) 4244 case 'i12 ihi rs2 rs1 101 ilo i11 11000 11' => Branch( BGE(rs1, rs2, asImm12(i12, i11, ihi, ilo))) 4245 case 'i12 ihi rs2 rs1 110 ilo i11 11000 11' => Branch(BLTU(rs1, rs2, asImm12(i12, i11, ihi, ilo))) 4246 case 'i12 ihi rs2 rs1 111 ilo i11 11000 11' => Branch(BGEU(rs1, rs2, asImm12(i12, i11, ihi, ilo))) 4247 4248 case 'imm rs1 000 rd 11001 11' => Branch( JALR(rd, rs1, imm)) 4249 case 'i20 ilo i11 ihi rd 11011 11' => Branch( JAL(rd, asImm20(i20, ihi, i11, ilo))) 4250 4251 case 'imm rd 01101 11' => ArithI( LUI(rd, imm)) 4252 case 'imm rd 00101 11' => ArithI(AUIPC(rd, imm)) 4253 4254 case 'imm rs1 000 rd 00100 11' => ArithI( ADDI(rd, rs1, imm)) 4255 case '000000 shamt rs1 001 rd 00100 11' => Shift( SLLI(rd, rs1, shamt)) 4256 case 'imm rs1 010 rd 00100 11' => ArithI( SLTI(rd, rs1, imm)) 4257 case 'imm rs1 011 rd 00100 11' => ArithI(SLTIU(rd, rs1, imm)) 4258 case 'imm rs1 100 rd 00100 11' => ArithI( XORI(rd, rs1, imm)) 4259 case '000000 shamt rs1 101 rd 00100 11' => Shift( SRLI(rd, rs1, shamt)) 4260 case '010000 shamt rs1 101 rd 00100 11' => Shift( SRAI(rd, rs1, shamt)) 4261 case 'imm rs1 110 rd 00100 11' => ArithI( ORI(rd, rs1, imm)) 4262 case 'imm rs1 111 rd 00100 11' => ArithI( ANDI(rd, rs1, imm)) 4263 4264 case '0000000 rs2 rs1 000 rd 01100 11' => ArithR( ADD(rd, rs1, rs2)) 4265 case '0100000 rs2 rs1 000 rd 01100 11' => ArithR( SUB(rd, rs1, rs2)) 4266 case '0000000 rs2 rs1 001 rd 01100 11' => Shift( SLL(rd, rs1, rs2)) 4267 case '0000000 rs2 rs1 010 rd 01100 11' => ArithR( SLT(rd, rs1, rs2)) 4268 case '0000000 rs2 rs1 011 rd 01100 11' => ArithR( SLTU(rd, rs1, rs2)) 4269 case '0000000 rs2 rs1 100 rd 01100 11' => ArithR( XOR(rd, rs1, rs2)) 4270 case '0000000 rs2 rs1 101 rd 01100 11' => Shift( SRL(rd, rs1, rs2)) 4271 case '0100000 rs2 rs1 101 rd 01100 11' => Shift( SRA(rd, rs1, rs2)) 4272 case '0000000 rs2 rs1 110 rd 01100 11' => ArithR( OR(rd, rs1, rs2)) 4273 case '0000000 rs2 rs1 111 rd 01100 11' => ArithR( AND(rd, rs1, rs2)) 4274 4275 case 'imm rs1 000 rd 00110 11' => ArithI(ADDIW(rd, rs1, imm)) 4276 case '0000000 shamt rs1 001 rd 00110 11' => Shift(SLLIW(rd, rs1, shamt)) 4277 case '0000000 shamt rs1 101 rd 00110 11' => Shift(SRLIW(rd, rs1, shamt)) 4278 case '0100000 shamt rs1 101 rd 00110 11' => Shift(SRAIW(rd, rs1, shamt)) 4279 4280 case '0000000 rs2 rs1 000 rd 01110 11' => ArithR( ADDW(rd, rs1, rs2)) 4281 case '0100000 rs2 rs1 000 rd 01110 11' => ArithR( SUBW(rd, rs1, rs2)) 4282 case '0000000 rs2 rs1 001 rd 01110 11' => Shift( SLLW(rd, rs1, rs2)) 4283 case '0000000 rs2 rs1 101 rd 01110 11' => Shift( SRLW(rd, rs1, rs2)) 4284 case '0100000 rs2 rs1 101 rd 01110 11' => Shift( SRAW(rd, rs1, rs2)) 4285 4286 case '0000001 rs2 rs1 000 rd 01100 11' => MulDiv( MUL(rd, rs1, rs2)) 4287 case '0000001 rs2 rs1 001 rd 01100 11' => MulDiv( MULH(rd, rs1, rs2)) 4288 case '0000001 rs2 rs1 010 rd 01100 11' => MulDiv(MULHSU(rd, rs1, rs2)) 4289 case '0000001 rs2 rs1 011 rd 01100 11' => MulDiv( MULHU(rd, rs1, rs2)) 4290 case '0000001 rs2 rs1 100 rd 01100 11' => MulDiv( DIV(rd, rs1, rs2)) 4291 case '0000001 rs2 rs1 101 rd 01100 11' => MulDiv( DIVU(rd, rs1, rs2)) 4292 case '0000001 rs2 rs1 110 rd 01100 11' => MulDiv( REM(rd, rs1, rs2)) 4293 case '0000001 rs2 rs1 111 rd 01100 11' => MulDiv( REMU(rd, rs1, rs2)) 4294 4295 case '0000001 rs2 rs1 000 rd 01110 11' => MulDiv( MULW(rd, rs1, rs2)) 4296 case '0000001 rs2 rs1 100 rd 01110 11' => MulDiv( DIVW(rd, rs1, rs2)) 4297 case '0000001 rs2 rs1 101 rd 01110 11' => MulDiv( DIVUW(rd, rs1, rs2)) 4298 case '0000001 rs2 rs1 110 rd 01110 11' => MulDiv( REMW(rd, rs1, rs2)) 4299 case '0000001 rs2 rs1 111 rd 01110 11' => MulDiv( REMUW(rd, rs1, rs2)) 4300 4301 case 'imm rs1 000 rd 00000 11' => Load( LB(rd, rs1, imm)) 4302 case 'imm rs1 001 rd 00000 11' => Load( LH(rd, rs1, imm)) 4303 case 'imm rs1 010 rd 00000 11' => Load( LW(rd, rs1, imm)) 4304 case 'imm rs1 011 rd 00000 11' => Load( LD(rd, rs1, imm)) 4305 case 'imm rs1 100 rd 00000 11' => Load( LBU(rd, rs1, imm)) 4306 case 'imm rs1 101 rd 00000 11' => Load( LHU(rd, rs1, imm)) 4307 case 'imm rs1 110 rd 00000 11' => Load( LWU(rd, rs1, imm)) 4308 4309 case 'ihi rs2 rs1 000 ilo 01000 11' => Store( SB(rs1, rs2, asSImm12(ihi, ilo))) 4310 case 'ihi rs2 rs1 001 ilo 01000 11' => Store( SH(rs1, rs2, asSImm12(ihi, ilo))) 4311 case 'ihi rs2 rs1 010 ilo 01000 11' => Store( SW(rs1, rs2, asSImm12(ihi, ilo))) 4312 case 'ihi rs2 rs1 011 ilo 01000 11' => Store( SD(rs1, rs2, asSImm12(ihi, ilo))) 4313 4314 case '_`4 pred succ rs1 000 rd 00011 11' => FENCE(rd, rs1, pred, succ) 4315 case 'imm rs1 001 rd 00011 11' => FENCE_I(rd, rs1, imm) 4316 4317 case 'rs3 00 rs2 rs1 frm rd 10000 11' => FArith( FMADD_S(rd, rs1, rs2, rs3, frm)) 4318 case 'rs3 00 rs2 rs1 frm rd 10001 11' => FArith( FMSUB_S(rd, rs1, rs2, rs3, frm)) 4319 case 'rs3 00 rs2 rs1 frm rd 10010 11' => FArith( FNMSUB_S(rd, rs1, rs2, rs3, frm)) 4320 case 'rs3 00 rs2 rs1 frm rd 10011 11' => FArith( FNMADD_S(rd, rs1, rs2, rs3, frm)) 4321 4322 case '0000000 rs2 rs1 frm rd 10100 11' => FArith( FADD_S(rd, rs1, rs2, frm)) 4323 case '0000100 rs2 rs1 frm rd 10100 11' => FArith( FSUB_S(rd, rs1, rs2, frm)) 4324 case '0001000 rs2 rs1 frm rd 10100 11' => FArith( FMUL_S(rd, rs1, rs2, frm)) 4325 case '0001100 rs2 rs1 frm rd 10100 11' => FArith( FDIV_S(rd, rs1, rs2, frm)) 4326 case '0101100 00000 rs1 frm rd 10100 11' => FArith( FSQRT_S(rd, rs1, frm)) 4327 4328 case '0010100 rs2 rs1 000 rd 10100 11' => FArith( FMIN_S(rd, rs1, rs2)) 4329 case '0010100 rs2 rs1 001 rd 10100 11' => FArith( FMAX_S(rd, rs1, rs2)) 4330 case '1010000 rs2 rs1 010 rd 10100 11' => FArith( FEQ_S(rd, rs1, rs2)) 4331 case '1010000 rs2 rs1 001 rd 10100 11' => FArith( FLT_S(rd, rs1, rs2)) 4332 case '1010000 rs2 rs1 000 rd 10100 11' => FArith( FLE_S(rd, rs1, rs2)) 4333 4334 case '0010000 rs2 rs1 000 rd 10100 11' => FConv ( FSGNJ_S(rd, rs1, rs2)) 4335 case '0010000 rs2 rs1 001 rd 10100 11' => FConv ( FSGNJN_S(rd, rs1, rs2)) 4336 case '0010000 rs2 rs1 010 rd 10100 11' => FConv ( FSGNJX_S(rd, rs1, rs2)) 4337 4338 case '1100000 00000 rs1 frm rd 10100 11' => FConv( FCVT_W_S(rd, rs1, frm)) 4339 case '1100000 00001 rs1 frm rd 10100 11' => FConv( FCVT_WU_S(rd, rs1, frm)) 4340 case '1110000 00000 rs1 000 rd 10100 11' => FConv( FMV_X_S(rd, rs1)) 4341 case '1110000 00000 rs1 001 rd 10100 11' => FConv( FCLASS_S(rd, rs1)) 4342 case '1101000 00000 rs1 frm rd 10100 11' => FConv( FCVT_S_W(rd, rs1, frm)) 4343 case '1101000 00001 rs1 frm rd 10100 11' => FConv( FCVT_S_WU(rd, rs1, frm)) 4344 case '1111000 00000 rs1 000 rd 10100 11' => FConv( FMV_S_X(rd, rs1)) 4345 4346 case 'rs3 01 rs2 rs1 frm rd 10000 11' => FArith( FMADD_D(rd, rs1, rs2, rs3, frm)) 4347 case 'rs3 01 rs2 rs1 frm rd 10001 11' => FArith( FMSUB_D(rd, rs1, rs2, rs3, frm)) 4348 case 'rs3 01 rs2 rs1 frm rd 10010 11' => FArith( FNMSUB_D(rd, rs1, rs2, rs3, frm)) 4349 case 'rs3 01 rs2 rs1 frm rd 10011 11' => FArith( FNMADD_D(rd, rs1, rs2, rs3, frm)) 4350 4351 case '0000001 rs2 rs1 frm rd 10100 11' => FArith( FADD_D(rd, rs1, rs2, frm)) 4352 case '0000101 rs2 rs1 frm rd 10100 11' => FArith( FSUB_D(rd, rs1, rs2, frm)) 4353 case '0001001 rs2 rs1 frm rd 10100 11' => FArith( FMUL_D(rd, rs1, rs2, frm)) 4354 case '0001101 rs2 rs1 frm rd 10100 11' => FArith( FDIV_D(rd, rs1, rs2, frm)) 4355 case '0101101 00000 rs1 frm rd 10100 11' => FArith( FSQRT_D(rd, rs1, frm)) 4356 4357 case '0010101 rs2 rs1 000 rd 10100 11' => FArith( FMIN_D(rd, rs1, rs2)) 4358 case '0010101 rs2 rs1 001 rd 10100 11' => FArith( FMAX_D(rd, rs1, rs2)) 4359 case '1010001 rs2 rs1 010 rd 10100 11' => FArith( FEQ_D(rd, rs1, rs2)) 4360 case '1010001 rs2 rs1 001 rd 10100 11' => FArith( FLT_D(rd, rs1, rs2)) 4361 case '1010001 rs2 rs1 000 rd 10100 11' => FArith( FLE_D(rd, rs1, rs2)) 4362 4363 case '0010001 rs2 rs1 000 rd 10100 11' => FConv ( FSGNJ_D(rd, rs1, rs2)) 4364 case '0010001 rs2 rs1 001 rd 10100 11' => FConv ( FSGNJN_D(rd, rs1, rs2)) 4365 case '0010001 rs2 rs1 010 rd 10100 11' => FConv ( FSGNJX_D(rd, rs1, rs2)) 4366 4367 case '1100001 00000 rs1 frm rd 10100 11' => FConv( FCVT_W_D(rd, rs1, frm)) 4368 case '1100001 00001 rs1 frm rd 10100 11' => FConv( FCVT_WU_D(rd, rs1, frm)) 4369 case '1110001 00000 rs1 001 rd 10100 11' => FConv( FCLASS_D(rd, rs1)) 4370 case '1101001 00000 rs1 frm rd 10100 11' => FConv( FCVT_D_W(rd, rs1, frm)) 4371 case '1101001 00001 rs1 frm rd 10100 11' => FConv( FCVT_D_WU(rd, rs1, frm)) 4372 4373 case '1100000 00010 rs1 frm rd 10100 11' => FConv( FCVT_L_S(rd, rs1, frm)) 4374 case '1100000 00011 rs1 frm rd 10100 11' => FConv( FCVT_LU_S(rd, rs1, frm)) 4375 case '1101000 00010 rs1 frm rd 10100 11' => FConv( FCVT_S_L(rd, rs1, frm)) 4376 case '1101000 00011 rs1 frm rd 10100 11' => FConv( FCVT_S_LU(rd, rs1, frm)) 4377 4378 case '1100001 00010 rs1 frm rd 10100 11' => FConv( FCVT_L_D(rd, rs1, frm)) 4379 case '1100001 00011 rs1 frm rd 10100 11' => FConv( FCVT_LU_D(rd, rs1, frm)) 4380 case '1101001 00010 rs1 frm rd 10100 11' => FConv( FCVT_D_L(rd, rs1, frm)) 4381 case '1101001 00011 rs1 frm rd 10100 11' => FConv( FCVT_D_LU(rd, rs1, frm)) 4382 case '1110001 00000 rs1 000 rd 10100 11' => FConv( FMV_X_D(rd, rs1)) 4383 case '1111001 00000 rs1 000 rd 10100 11' => FConv( FMV_D_X(rd, rs1)) 4384 4385 case '0100000 00001 rs1 frm rd 10100 11' => FConv( FCVT_S_D(rd, rs1, frm)) 4386 case '0100001 00000 rs1 frm rd 10100 11' => FConv( FCVT_D_S(rd, rs1, frm)) 4387 4388 case 'imm rs1 010 rd 00001 11' => FPLoad( FLW(rd, rs1, imm)) 4389 case 'imm rs1 011 rd 00001 11' => FPLoad( FLD(rd, rs1, imm)) 4390 case 'ihi rs2 rs1 010 ilo 01001 11' => FPStore( FSW(rs1, rs2, asSImm12(ihi, ilo))) 4391 case 'ihi rs2 rs1 011 ilo 01001 11' => FPStore( FSD(rs1, rs2, asSImm12(ihi, ilo))) 4392 4393 case '00010 aq rl 00000 rs1 010 rd 01011 11' => AMO( LR_W(aq, rl, rd, rs1)) 4394 case '00010 aq rl 00000 rs1 011 rd 01011 11' => AMO( LR_D(aq, rl, rd, rs1)) 4395 case '00011 aq rl rs2 rs1 010 rd 01011 11' => AMO( SC_W(aq, rl, rd, rs1, rs2)) 4396 case '00011 aq rl rs2 rs1 011 rd 01011 11' => AMO( SC_D(aq, rl, rd, rs1, rs2)) 4397 4398 case '00001 aq rl rs2 rs1 010 rd 01011 11' => AMO(AMOSWAP_W(aq, rl, rd, rs1, rs2)) 4399 case '00000 aq rl rs2 rs1 010 rd 01011 11' => AMO( AMOADD_W(aq, rl, rd, rs1, rs2)) 4400 case '00100 aq rl rs2 rs1 010 rd 01011 11' => AMO( AMOXOR_W(aq, rl, rd, rs1, rs2)) 4401 case '01100 aq rl rs2 rs1 010 rd 01011 11' => AMO( AMOAND_W(aq, rl, rd, rs1, rs2)) 4402 case '01000 aq rl rs2 rs1 010 rd 01011 11' => AMO( AMOOR_W(aq, rl, rd, rs1, rs2)) 4403 case '10000 aq rl rs2 rs1 010 rd 01011 11' => AMO( AMOMIN_W(aq, rl, rd, rs1, rs2)) 4404 case '10100 aq rl rs2 rs1 010 rd 01011 11' => AMO( AMOMAX_W(aq, rl, rd, rs1, rs2)) 4405 case '11000 aq rl rs2 rs1 010 rd 01011 11' => AMO(AMOMINU_W(aq, rl, rd, rs1, rs2)) 4406 case '11100 aq rl rs2 rs1 010 rd 01011 11' => AMO(AMOMAXU_W(aq, rl, rd, rs1, rs2)) 4407 4408 case '00001 aq rl rs2 rs1 011 rd 01011 11' => AMO(AMOSWAP_D(aq, rl, rd, rs1, rs2)) 4409 case '00000 aq rl rs2 rs1 011 rd 01011 11' => AMO( AMOADD_D(aq, rl, rd, rs1, rs2)) 4410 case '00100 aq rl rs2 rs1 011 rd 01011 11' => AMO( AMOXOR_D(aq, rl, rd, rs1, rs2)) 4411 case '01100 aq rl rs2 rs1 011 rd 01011 11' => AMO( AMOAND_D(aq, rl, rd, rs1, rs2)) 4412 case '01000 aq rl rs2 rs1 011 rd 01011 11' => AMO( AMOOR_D(aq, rl, rd, rs1, rs2)) 4413 case '10000 aq rl rs2 rs1 011 rd 01011 11' => AMO( AMOMIN_D(aq, rl, rd, rs1, rs2)) 4414 case '10100 aq rl rs2 rs1 011 rd 01011 11' => AMO( AMOMAX_D(aq, rl, rd, rs1, rs2)) 4415 case '11000 aq rl rs2 rs1 011 rd 01011 11' => AMO(AMOMINU_D(aq, rl, rd, rs1, rs2)) 4416 case '11100 aq rl rs2 rs1 011 rd 01011 11' => AMO(AMOMAXU_D(aq, rl, rd, rs1, rs2)) 4417 4418 case 'csr rs1 001 rd 11100 11' => System( CSRRW(rd, rs1, csr)) 4419 case 'csr rs1 010 rd 11100 11' => System( CSRRS(rd, rs1, csr)) 4420 case 'csr rs1 011 rd 11100 11' => System( CSRRC(rd, rs1, csr)) 4421 case 'csr imm 101 rd 11100 11' => System(CSRRWI(rd, imm, csr)) 4422 case 'csr imm 110 rd 11100 11' => System(CSRRSI(rd, imm, csr)) 4423 case 'csr imm 111 rd 11100 11' => System(CSRRCI(rd, imm, csr)) 4424 4425 case '000000000000 00000 000 00000 11100 11' => System( ECALL) 4426 case '000000000001 00000 000 00000 11100 11' => System(EBREAK) 4427 case '000100000000 00000 000 00000 11100 11' => System( ERET) 4428 case '001100000101 00000 000 00000 11100 11' => System( MRTS) 4429 case '000100000010 00000 000 00000 11100 11' => System( WFI) 4430 4431 case '000100000001 rs1 000 00000 11100 11' => System(SFENCE_VM(rs1)) 4432 4433 -- unsupported instructions 4434 case _ => UnknownInstruction 4435 } 4436 4437-- instruction printer 4438 4439string imm(i::bits(N)) = "0x" : [i] 4440string instr(o::string) = PadRight(#" ", 12, o) 4441 4442string amotype(aq::amo, rl::amo) = 4443 match aq, rl 4444 { case 0, 0 => "" 4445 case 1, 0 => ".aq" 4446 case 0, 1 => ".rl" 4447 case 1, 1 => ".sc" 4448 } 4449 4450string pRtype(o::string, rd::reg, rs1::reg, rs2::reg) = 4451 instr(o) : " " : reg(rd) : ", " : reg(rs1) : ", " : reg(rs2) 4452 4453string pARtype(o::string, aq::amo, rl::amo, rd::reg, rs1::reg, rs2::reg) = 4454 pRtype([o : amotype(aq, rl)], rd, rs1, rs2) 4455 4456string pLRtype(o::string, aq::amo, rl::amo, rd::reg, rs1::reg) = 4457 instr([o : amotype(aq, rl)]) : " " : reg(rd) : ", " : reg(rs1) 4458 4459string pItype(o::string, rd::reg, rs1::reg, i::bits(N)) = 4460 instr(o) : " " : reg(rd) : ", " : reg(rs1) : ", " : imm(i) 4461 4462string pCSRtype(o::string, rd::reg, rs1::reg, csr::creg) = 4463 instr(o) : " " : reg(rd) : ", " : reg(rs1) : ", " : csrName(csr) 4464 4465string pCSRItype(o::string, rd::reg, i::bits(N), csr::creg) = 4466 instr(o) : " " : reg(rd) : ", " : imm(i) : ", " : csrName(csr) 4467 4468string pStype(o::string, rs1::reg, rs2::reg, i::bits(N)) = 4469 instr(o) : " " : reg(rs2) : ", " : reg(rs1) : ", " : imm(i) 4470 4471string pSBtype(o::string, rs1::reg, rs2::reg, i::bits(N)) = 4472 instr(o) : " " : reg(rs1) : ", " : reg(rs2) : ", " : imm(i<<1) 4473 4474string pUtype(o::string, rd::reg, i::bits(N)) = 4475 instr(o) : " " : reg(rd) : ", " : imm(i) 4476 4477string pUJtype(o::string, rd::reg, i::bits(N)) = 4478 instr(o) : " " : reg(rd) : ", " : imm(i<<1) 4479 4480string pN0type(o::string) = 4481 instr(o) 4482 4483string pN1type(o::string, r::reg) = 4484 instr(o) : " " : reg(r) 4485 4486string pFRtype(o::string, rd::reg, rs1::reg, rs2::reg) = 4487 instr(o) : " " : fpreg(rd) : ", " : fpreg(rs1) : ", " : fpreg(rs2) 4488 4489string pFR1type(o::string, rd::reg, rs::reg) = 4490 instr(o) : " " : fpreg(rd) : ", " : fpreg(rs) 4491 4492string pFR3type(o::string, rd::reg, rs1::reg, rs2::reg, rs3::reg) = 4493 instr(o) : " " : fpreg(rd) : ", " : fpreg(rs1) : ", " : fpreg(rs2) : ", " : fpreg(rs3) 4494 4495string pFItype(o::string, rd::reg, rs1::reg, i::bits(N)) = 4496 instr(o) : " " : fpreg(rd) : ", " : reg(rs1) : ", " : imm(i) 4497 4498string pFStype(o::string, rs1::reg, rs2::reg, i::bits(N)) = 4499 instr(o) : " " : fpreg(rs2) : ", " : reg(rs1) : ", " : imm(i) 4500 4501string pCFItype(o::string, rd::reg, rs::reg) = 4502 instr(o) : " " : fpreg(rd) : ", " : reg(rs) 4503 4504string pCIFtype(o::string, rd::reg, rs::reg) = 4505 instr(o) : " " : reg(rd) : ", " : fpreg(rs) 4506 4507string instructionToString(i::instruction) = 4508 match i 4509 { case Branch( BEQ(rs1, rs2, imm)) => pSBtype("BEQ", rs1, rs2, imm) 4510 case Branch( BNE(rs1, rs2, imm)) => pSBtype("BNE", rs1, rs2, imm) 4511 case Branch( BLT(rs1, rs2, imm)) => pSBtype("BLT", rs1, rs2, imm) 4512 case Branch( BGE(rs1, rs2, imm)) => pSBtype("BGE", rs1, rs2, imm) 4513 case Branch( BLTU(rs1, rs2, imm)) => pSBtype("BLTU", rs1, rs2, imm) 4514 case Branch( BGEU(rs1, rs2, imm)) => pSBtype("BGEU", rs1, rs2, imm) 4515 4516 case Branch( JALR(rd, rs1, imm)) => pItype("JALR", rd, rs1, imm) 4517 case Branch( JAL(rd, imm)) => pUJtype("JAL", rd, imm) 4518 4519 case ArithI( LUI(rd, imm)) => pUtype("LUI", rd, imm) 4520 case ArithI(AUIPC(rd, imm)) => pUtype("AUIPC", rd, imm) 4521 4522 case ArithI( ADDI(rd, rs1, imm)) => pItype("ADDI", rd, rs1, imm) 4523 case Shift( SLLI(rd, rs1, imm)) => pItype("SLLI", rd, rs1, imm) 4524 case ArithI( SLTI(rd, rs1, imm)) => pItype("SLTI", rd, rs1, imm) 4525 case ArithI(SLTIU(rd, rs1, imm)) => pItype("SLTIU", rd, rs1, imm) 4526 case ArithI( XORI(rd, rs1, imm)) => pItype("XORI", rd, rs1, imm) 4527 case Shift( SRLI(rd, rs1, imm)) => pItype("SRLI", rd, rs1, imm) 4528 case Shift( SRAI(rd, rs1, imm)) => pItype("SRAI", rd, rs1, imm) 4529 case ArithI( ORI(rd, rs1, imm)) => pItype("ORI", rd, rs1, imm) 4530 case ArithI( ANDI(rd, rs1, imm)) => pItype("ANDI", rd, rs1, imm) 4531 4532 case ArithR( ADD(rd, rs1, rs2)) => pRtype("ADD", rd, rs1, rs2) 4533 case ArithR( SUB(rd, rs1, rs2)) => pRtype("SUB", rd, rs1, rs2) 4534 case Shift( SLL(rd, rs1, rs2)) => pRtype("SLL", rd, rs1, rs2) 4535 case ArithR( SLT(rd, rs1, rs2)) => pRtype("SLT", rd, rs1, rs2) 4536 case ArithR( SLTU(rd, rs1, rs2)) => pRtype("SLTU", rd, rs1, rs2) 4537 case ArithR( XOR(rd, rs1, rs2)) => pRtype("XOR", rd, rs1, rs2) 4538 case Shift( SRL(rd, rs1, rs2)) => pRtype("SRL", rd, rs1, rs2) 4539 case Shift( SRA(rd, rs1, rs2)) => pRtype("SRA", rd, rs1, rs2) 4540 case ArithR( OR(rd, rs1, rs2)) => pRtype("OR", rd, rs1, rs2) 4541 case ArithR( AND(rd, rs1, rs2)) => pRtype("AND", rd, rs1, rs2) 4542 4543 case ArithI(ADDIW(rd, rs1, imm)) => pItype("ADDIW", rd, rs1, imm) 4544 case Shift(SLLIW(rd, rs1, imm)) => pItype("SLLIW", rd, rs1, imm) 4545 case Shift(SRLIW(rd, rs1, imm)) => pItype("SRLIW", rd, rs1, imm) 4546 case Shift(SRAIW(rd, rs1, imm)) => pItype("SRAIW", rd, rs1, imm) 4547 4548 case ArithR( ADDW(rd, rs1, rs2)) => pRtype("ADDW", rd, rs1, rs2) 4549 case ArithR( SUBW(rd, rs1, rs2)) => pRtype("SUBW", rd, rs1, rs2) 4550 case Shift( SLLW(rd, rs1, rs2)) => pRtype("SLLW", rd, rs1, rs2) 4551 case Shift( SRLW(rd, rs1, rs2)) => pRtype("SRLW", rd, rs1, rs2) 4552 case Shift( SRAW(rd, rs1, rs2)) => pRtype("SRAW", rd, rs1, rs2) 4553 4554 case MulDiv( MUL(rd, rs1, rs2)) => pRtype("MUL", rd, rs1, rs2) 4555 case MulDiv( MULH(rd, rs1, rs2)) => pRtype("MULH", rd, rs1, rs2) 4556 case MulDiv( MULHSU(rd, rs1, rs2)) => pRtype("MULHSU", rd, rs1, rs2) 4557 case MulDiv( MULHU(rd, rs1, rs2)) => pRtype("MULHU", rd, rs1, rs2) 4558 case MulDiv( DIV(rd, rs1, rs2)) => pRtype("DIV", rd, rs1, rs2) 4559 case MulDiv( DIVU(rd, rs1, rs2)) => pRtype("DIVU", rd, rs1, rs2) 4560 case MulDiv( REM(rd, rs1, rs2)) => pRtype("REM", rd, rs1, rs2) 4561 case MulDiv( REMU(rd, rs1, rs2)) => pRtype("REMU", rd, rs1, rs2) 4562 4563 case MulDiv( MULW(rd, rs1, rs2)) => pRtype("MULW", rd, rs1, rs2) 4564 case MulDiv( DIVW(rd, rs1, rs2)) => pRtype("DIVW", rd, rs1, rs2) 4565 case MulDiv( DIVUW(rd, rs1, rs2)) => pRtype("DIVUW", rd, rs1, rs2) 4566 case MulDiv( REMW(rd, rs1, rs2)) => pRtype("REMW", rd, rs1, rs2) 4567 case MulDiv( REMUW(rd, rs1, rs2)) => pRtype("REMUW", rd, rs1, rs2) 4568 4569 case Load( LB(rd, rs1, imm)) => pItype("LB", rd, rs1, imm) 4570 case Load( LH(rd, rs1, imm)) => pItype("LH", rd, rs1, imm) 4571 case Load( LW(rd, rs1, imm)) => pItype("LW", rd, rs1, imm) 4572 case Load( LD(rd, rs1, imm)) => pItype("LD", rd, rs1, imm) 4573 case Load( LBU(rd, rs1, imm)) => pItype("LBU", rd, rs1, imm) 4574 case Load( LHU(rd, rs1, imm)) => pItype("LHU", rd, rs1, imm) 4575 case Load( LWU(rd, rs1, imm)) => pItype("LWU", rd, rs1, imm) 4576 4577 case Store( SB(rs1, rs2, imm)) => pStype("SB", rs1, rs2, imm) 4578 case Store( SH(rs1, rs2, imm)) => pStype("SH", rs1, rs2, imm) 4579 case Store( SW(rs1, rs2, imm)) => pStype("SW", rs1, rs2, imm) 4580 case Store( SD(rs1, rs2, imm)) => pStype("SD", rs1, rs2, imm) 4581 4582 case FENCE(rd, rs1, pred, succ) => pN0type("FENCE") 4583 case FENCE_I(rd, rs1, imm) => pN0type("FENCE.I") 4584 4585 case FArith( FADD_S(rd, rs1, rs2, frm)) => pFRtype("FADD.S", rd, rs1, rs2) 4586 case FArith( FSUB_S(rd, rs1, rs2, frm)) => pFRtype("FSUB.S", rd, rs1, rs2) 4587 case FArith( FMUL_S(rd, rs1, rs2, frm)) => pFRtype("FMUL.S", rd, rs1, rs2) 4588 case FArith( FDIV_S(rd, rs1, rs2, frm)) => pFRtype("FDIV.S", rd, rs1, rs2) 4589 4590 case FArith( FSQRT_S(rd, rs, frm)) => pFR1type("FSQRT.S", rd, rs) 4591 4592 case FArith( FMIN_S(rd, rs1, rs2)) => pFRtype("FMIN.S", rd, rs1, rs2) 4593 case FArith( FMAX_S(rd, rs1, rs2)) => pFRtype("FMAX.S", rd, rs1, rs2) 4594 case FArith( FEQ_S(rd, rs1, rs2)) => pFRtype("FEQ.S", rd, rs1, rs2) 4595 case FArith( FLT_S(rd, rs1, rs2)) => pFRtype("FLT.S", rd, rs1, rs2) 4596 case FArith( FLE_S(rd, rs1, rs2)) => pFRtype("FLE.S", rd, rs1, rs2) 4597 4598 case FArith( FMADD_S(rd, rs1, rs2, rs3, frm)) => pFR3type("FMADD.S", rd, rs1, rs2, rs3) 4599 case FArith( FMSUB_S(rd, rs1, rs2, rs3, frm)) => pFR3type("FMSUB.S", rd, rs1, rs2, rs3) 4600 case FArith(FNMADD_S(rd, rs1, rs2, rs3, frm)) => pFR3type("FNMADD.S", rd, rs1, rs2, rs3) 4601 case FArith(FNMSUB_S(rd, rs1, rs2, rs3, frm)) => pFR3type("FNMSUB.S", rd, rs1, rs2, rs3) 4602 4603 case FArith( FADD_D(rd, rs1, rs2, frm)) => pFRtype("FADD.D", rd, rs1, rs2) 4604 case FArith( FSUB_D(rd, rs1, rs2, frm)) => pFRtype("FSUB.D", rd, rs1, rs2) 4605 case FArith( FMUL_D(rd, rs1, rs2, frm)) => pFRtype("FMUL.D", rd, rs1, rs2) 4606 case FArith( FDIV_D(rd, rs1, rs2, frm)) => pFRtype("FDIV.D", rd, rs1, rs2) 4607 4608 case FArith( FSQRT_D(rd, rs, frm)) => pFR1type("FSQRT.D", rd, rs) 4609 4610 case FArith( FMIN_D(rd, rs1, rs2)) => pFRtype("FMIN.D", rd, rs1, rs2) 4611 case FArith( FMAX_D(rd, rs1, rs2)) => pFRtype("FMAX.D", rd, rs1, rs2) 4612 case FArith( FEQ_D(rd, rs1, rs2)) => pFRtype("FEQ.D", rd, rs1, rs2) 4613 case FArith( FLT_D(rd, rs1, rs2)) => pFRtype("FLT.D", rd, rs1, rs2) 4614 case FArith( FLE_D(rd, rs1, rs2)) => pFRtype("FLE.D", rd, rs1, rs2) 4615 4616 case FArith( FMADD_D(rd, rs1, rs2, rs3, frm)) => pFR3type("FMADD.D", rd, rs1, rs2, rs3) 4617 case FArith( FMSUB_D(rd, rs1, rs2, rs3, frm)) => pFR3type("FMSUB.D", rd, rs1, rs2, rs3) 4618 case FArith(FNMADD_D(rd, rs1, rs2, rs3, frm)) => pFR3type("FNMADD.D", rd, rs1, rs2, rs3) 4619 case FArith(FNMSUB_D(rd, rs1, rs2, rs3, frm)) => pFR3type("FNMSUB.D", rd, rs1, rs2, rs3) 4620 4621 case FConv( FSGNJ_S(rd, rs1, rs2)) => pFRtype("FSGNJ.S", rd, rs1, rs2) 4622 case FConv( FSGNJN_S(rd, rs1, rs2)) => pFRtype("FSGNJN.S", rd, rs1, rs2) 4623 case FConv( FSGNJX_S(rd, rs1, rs2)) => pFRtype("FSGNJX.S", rd, rs1, rs2) 4624 4625 case FConv( FCVT_W_S(rd, rs, frm)) => pCIFtype("FCVT.W.S", rd, rs) 4626 case FConv(FCVT_WU_S(rd, rs, frm)) => pCIFtype("FCVT.WU.S", rd, rs) 4627 case FConv( FMV_X_S(rd, rs)) => pCIFtype("FMV.X.S", rd, rs) 4628 case FConv( FCLASS_S(rd, rs)) => pCIFtype("FCLASS.S", rd, rs) 4629 case FConv( FCVT_S_W(rd, rs, frm)) => pCFItype("FCVT.S.W", rd, rs) 4630 case FConv(FCVT_S_WU(rd, rs, frm)) => pCFItype("FCVT.S.WU", rd, rs) 4631 case FConv( FMV_S_X(rd, rs)) => pCFItype("FMV.S.X", rd, rs) 4632 4633 case FConv( FSGNJ_D(rd, rs1, rs2)) => pFRtype("FSGNJ.D", rd, rs1, rs2) 4634 case FConv( FSGNJN_D(rd, rs1, rs2)) => pFRtype("FSGNJN.D", rd, rs1, rs2) 4635 case FConv( FSGNJX_D(rd, rs1, rs2)) => pFRtype("FSGNJX.D", rd, rs1, rs2) 4636 4637 case FConv( FCVT_W_D(rd, rs, frm)) => pCIFtype("FCVT.W.D", rd, rs) 4638 case FConv(FCVT_WU_D(rd, rs, frm)) => pCIFtype("FCVT.WU.D", rd, rs) 4639 case FConv( FCLASS_D(rd, rs)) => pCIFtype("FCLASS.D", rd, rs) 4640 case FConv( FCVT_D_W(rd, rs, frm)) => pCFItype("FCVT.D.W", rd, rs) 4641 case FConv(FCVT_D_WU(rd, rs, frm)) => pCFItype("FCVT.D.WU", rd, rs) 4642 4643 case FConv( FCVT_L_S(rd, rs, frm)) => pCIFtype("FCVT.L.S", rd, rs) 4644 case FConv(FCVT_LU_S(rd, rs, frm)) => pCIFtype("FCVT.LU.S", rd, rs) 4645 case FConv( FCVT_S_L(rd, rs, frm)) => pCFItype("FCVT.S.L", rd, rs) 4646 case FConv(FCVT_S_LU(rd, rs, frm)) => pCFItype("FCVT.S.LU", rd, rs) 4647 case FConv( FCVT_L_D(rd, rs, frm)) => pCIFtype("FCVT.L.D", rd, rs) 4648 case FConv(FCVT_LU_D(rd, rs, frm)) => pCIFtype("FCVT.LU.D", rd, rs) 4649 case FConv( FMV_X_D(rd, rs)) => pCIFtype("FMV.X.D", rd, rs) 4650 case FConv( FCVT_D_L(rd, rs, frm)) => pCFItype("FCVT.D.L", rd, rs) 4651 case FConv(FCVT_D_LU(rd, rs, frm)) => pCFItype("FCVT.D.LU", rd, rs) 4652 case FConv( FMV_D_X(rd, rs)) => pCFItype("FMV.D.X", rd, rs) 4653 case FConv( FCVT_D_S(rd, rs, frm)) => pCFItype("FCVT.D.S", rd, rs) 4654 case FConv( FCVT_S_D(rd, rs, frm)) => pCFItype("FCVT.S.D", rd, rs) 4655 4656 case FPLoad( FLW(rd, rs1, imm)) => pFItype("FLW", rd, rs1, imm) 4657 case FPLoad( FLD(rd, rs1, imm)) => pFItype("FLD", rd, rs1, imm) 4658 case FPStore( FSW(rs1, rs2, imm)) => pFStype("FSW", rs1, rs2, imm) 4659 case FPStore( FSD(rs1, rs2, imm)) => pFStype("FSD", rs1, rs2, imm) 4660 4661 case AMO( LR_W(aq, rl, rd, rs1)) => pLRtype("LR.W", aq, rl, rd, rs1) 4662 case AMO( LR_D(aq, rl, rd, rs1)) => pLRtype("LR.D", aq, rl, rd, rs1) 4663 case AMO( SC_W(aq, rl, rd, rs1, rs2)) => pARtype("SC.W", aq, rl, rd, rs1, rs2) 4664 case AMO( SC_D(aq, rl, rd, rs1, rs2)) => pARtype("SC.D", aq, rl, rd, rs1, rs2) 4665 4666 case AMO(AMOSWAP_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOSWAP.W", aq, rl, rd, rs1, rs2) 4667 case AMO( AMOADD_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOADD.W", aq, rl, rd, rs1, rs2) 4668 case AMO( AMOXOR_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOXOR.W", aq, rl, rd, rs1, rs2) 4669 case AMO( AMOAND_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOAND.W", aq, rl, rd, rs1, rs2) 4670 case AMO( AMOOR_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOOR.W", aq, rl, rd, rs1, rs2) 4671 case AMO( AMOMIN_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOMIN.W", aq, rl, rd, rs1, rs2) 4672 case AMO( AMOMAX_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOMAX.W", aq, rl, rd, rs1, rs2) 4673 case AMO(AMOMINU_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOMINU.W", aq, rl, rd, rs1, rs2) 4674 case AMO(AMOMAXU_W(aq, rl, rd, rs1, rs2)) => pARtype("AMOMAXU.W", aq, rl, rd, rs1, rs2) 4675 4676 case AMO(AMOSWAP_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOSWAP.D", aq, rl, rd, rs1, rs2) 4677 case AMO( AMOADD_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOADD.D", aq, rl, rd, rs1, rs2) 4678 case AMO( AMOXOR_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOXOR.D", aq, rl, rd, rs1, rs2) 4679 case AMO( AMOAND_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOAND.D", aq, rl, rd, rs1, rs2) 4680 case AMO( AMOOR_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOOR.D", aq, rl, rd, rs1, rs2) 4681 case AMO( AMOMIN_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOMIN.D", aq, rl, rd, rs1, rs2) 4682 case AMO( AMOMAX_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOMAX.D", aq, rl, rd, rs1, rs2) 4683 case AMO(AMOMINU_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOMINU.D", aq, rl, rd, rs1, rs2) 4684 case AMO(AMOMAXU_D(aq, rl, rd, rs1, rs2)) => pARtype("AMOMAXU.D", aq, rl, rd, rs1, rs2) 4685 4686 case System( ECALL) => pN0type("ECALL") 4687 case System(EBREAK) => pN0type("EBREAK") 4688 case System( ERET) => pN0type("ERET") 4689 case System( MRTS) => pN0type("MRTS") 4690 case System( WFI) => pN0type("WFI") 4691 4692 case System( CSRRW(rd, rs1, csr)) => pCSRtype("CSRRW", rd, rs1, csr) 4693 case System( CSRRS(rd, rs1, csr)) => pCSRtype("CSRRS", rd, rs1, csr) 4694 case System( CSRRC(rd, rs1, csr)) => pCSRtype("CSRRC", rd, rs1, csr) 4695 case System(CSRRWI(rd, imm, csr)) => pCSRItype("CSRRWI", rd, imm, csr) 4696 case System(CSRRSI(rd, imm, csr)) => pCSRItype("CSRRSI", rd, imm, csr) 4697 case System(CSRRCI(rd, imm, csr)) => pCSRItype("CSRRCI", rd, imm, csr) 4698 4699 case System(SFENCE_VM(rs1)) => pN1type("SFENCE.VM", rs1) 4700 4701 case UnknownInstruction => pN0type("UNKNOWN") 4702 4703 case Internal(FETCH_MISALIGNED(_)) => pN0type("FETCH_MISALIGNED") 4704 case Internal(FETCH_FAULT(_)) => pN0type("FETCH_FAULT") 4705 } 4706 4707 4708word Rtype(o::opcode, f3::bits(3), rd::reg, rs1::reg, rs2::reg, f7::bits(7)) = 4709 f7 : rs2 : rs1 : f3 : rd : o 4710 4711word R4type(o::opcode, f3::bits(3), rd::reg, rs1::reg, rs2::reg, rs3::reg, f2::bits(2)) = 4712 rs3 : f2 : rs2 : rs1 : f3 : rd : o 4713 4714word Itype(o::opcode, f3::bits(3), rd::reg, rs1::reg, imm::imm12) = 4715 imm : rs1 : f3 : rd : o 4716 4717word Stype(o::opcode, f3::bits(3), rs1::reg, rs2::reg, imm::imm12) = 4718 imm<11:5> : rs2 : rs1 : f3 : imm<4:0> : o 4719 4720word SBtype(o::opcode, f3::bits(3), rs1::reg, rs2::reg, imm::imm12) = 4721 [imm<11>]::bits(1) : imm<9:4> : rs2 : rs1 : f3 : imm<3:0> : [imm<10>]::bits(1) : o 4722 4723word Utype(o::opcode, rd::reg, imm::imm20) = 4724 imm : rd : o 4725 4726word UJtype(o::opcode, rd::reg, imm::imm20) = 4727 [imm<19>]::bits(1) : imm<9:0> : [imm<10>]::bits(1) : imm<18:11> : rd : o 4728 4729opcode opc(code::bits(8)) = code<4:0> : '11' 4730 4731bits(7) amofunc(code::bits(5), aq::amo, rl::amo) = 4732 code : aq : rl 4733 4734word Encode(i::instruction) = 4735 match i 4736 { case Branch( BEQ(rs1, rs2, imm)) => SBtype(opc(0x18), 0, rs1, rs2, imm) 4737 case Branch( BNE(rs1, rs2, imm)) => SBtype(opc(0x18), 1, rs1, rs2, imm) 4738 case Branch( BLT(rs1, rs2, imm)) => SBtype(opc(0x18), 4, rs1, rs2, imm) 4739 case Branch( BGE(rs1, rs2, imm)) => SBtype(opc(0x18), 5, rs1, rs2, imm) 4740 case Branch( BLTU(rs1, rs2, imm)) => SBtype(opc(0x18), 6, rs1, rs2, imm) 4741 case Branch( BGEU(rs1, rs2, imm)) => SBtype(opc(0x18), 7, rs1, rs2, imm) 4742 4743 case Branch( JALR(rd, rs1, imm)) => Itype(opc(0x19), 0, rd, rs1, imm) 4744 case Branch( JAL(rd, imm)) => UJtype(opc(0x1b), rd, imm) 4745 4746 case ArithI( LUI(rd, imm)) => Utype(opc(0x0D), rd, imm) 4747 case ArithI(AUIPC(rd, imm)) => Utype(opc(0x05), rd, imm) 4748 4749 case ArithI( ADDI(rd, rs1, imm)) => Itype(opc(0x04), 0, rd, rs1, imm) 4750 case Shift( SLLI(rd, rs1, imm)) => Itype(opc(0x04), 1, rd, rs1, '000000' : imm) 4751 case ArithI( SLTI(rd, rs1, imm)) => Itype(opc(0x04), 2, rd, rs1, imm) 4752 case ArithI(SLTIU(rd, rs1, imm)) => Itype(opc(0x04), 3, rd, rs1, imm) 4753 case ArithI( XORI(rd, rs1, imm)) => Itype(opc(0x04), 4, rd, rs1, imm) 4754 case Shift( SRLI(rd, rs1, imm)) => Itype(opc(0x04), 5, rd, rs1, '000000' : imm) 4755 case Shift( SRAI(rd, rs1, imm)) => Itype(opc(0x04), 5, rd, rs1, '010000' : imm) 4756 case ArithI( ORI(rd, rs1, imm)) => Itype(opc(0x04), 6, rd, rs1, imm) 4757 case ArithI( ANDI(rd, rs1, imm)) => Itype(opc(0x04), 7, rd, rs1, imm) 4758 4759 case ArithR( ADD(rd, rs1, rs2)) => Rtype(opc(0x0C), 0, rd, rs1, rs2, 0) 4760 case ArithR( SUB(rd, rs1, rs2)) => Rtype(opc(0x0C), 0, rd, rs1, rs2, 0x20) 4761 case Shift( SLL(rd, rs1, rs2)) => Rtype(opc(0x0C), 1, rd, rs1, rs2, 0) 4762 case ArithR( SLT(rd, rs1, rs2)) => Rtype(opc(0x0C), 2, rd, rs1, rs2, 0) 4763 case ArithR( SLTU(rd, rs1, rs2)) => Rtype(opc(0x0C), 3, rd, rs1, rs2, 0) 4764 case ArithR( XOR(rd, rs1, rs2)) => Rtype(opc(0x0C), 4, rd, rs1, rs2, 0) 4765 case Shift( SRL(rd, rs1, rs2)) => Rtype(opc(0x0C), 5, rd, rs1, rs2, 0) 4766 case Shift( SRA(rd, rs1, rs2)) => Rtype(opc(0x0C), 5, rd, rs1, rs2, 0x20) 4767 case ArithR( OR(rd, rs1, rs2)) => Rtype(opc(0x0C), 6, rd, rs1, rs2, 0) 4768 case ArithR( AND(rd, rs1, rs2)) => Rtype(opc(0x0C), 7, rd, rs1, rs2, 0) 4769 4770 case ArithI(ADDIW(rd, rs1, imm)) => Itype(opc(0x06), 0, rd, rs1, imm) 4771 case Shift(SLLIW(rd, rs1, imm)) => Itype(opc(0x06), 1, rd, rs1, '0000000' : imm) 4772 case Shift(SRLIW(rd, rs1, imm)) => Itype(opc(0x06), 5, rd, rs1, '0000000' : imm) 4773 case Shift(SRAIW(rd, rs1, imm)) => Itype(opc(0x06), 5, rd, rs1, '0100000' : imm) 4774 4775 case ArithR( ADDW(rd, rs1, rs2)) => Rtype(opc(0x0E), 0, rd, rs1, rs2, '0000000') 4776 case ArithR( SUBW(rd, rs1, rs2)) => Rtype(opc(0x0E), 0, rd, rs1, rs2, '0100000') 4777 case Shift( SLLW(rd, rs1, rs2)) => Rtype(opc(0x0E), 1, rd, rs1, rs2, '0000000') 4778 case Shift( SRLW(rd, rs1, rs2)) => Rtype(opc(0x0E), 5, rd, rs1, rs2, '0000000') 4779 case Shift( SRAW(rd, rs1, rs2)) => Rtype(opc(0x0E), 5, rd, rs1, rs2, '0100000') 4780 4781 case MulDiv( MUL(rd, rs1, rs2)) => Rtype(opc(0x0C), 0, rd, rs1, rs2, '0000001') 4782 case MulDiv( MULH(rd, rs1, rs2)) => Rtype(opc(0x0C), 1, rd, rs1, rs2, '0000001') 4783 case MulDiv( MULHSU(rd, rs1, rs2)) => Rtype(opc(0x0C), 2, rd, rs1, rs2, '0000001') 4784 case MulDiv( MULHU(rd, rs1, rs2)) => Rtype(opc(0x0C), 3, rd, rs1, rs2, '0000001') 4785 case MulDiv( DIV(rd, rs1, rs2)) => Rtype(opc(0x0C), 4, rd, rs1, rs2, '0000001') 4786 case MulDiv( DIVU(rd, rs1, rs2)) => Rtype(opc(0x0C), 5, rd, rs1, rs2, '0000001') 4787 case MulDiv( REM(rd, rs1, rs2)) => Rtype(opc(0x0C), 6, rd, rs1, rs2, '0000001') 4788 case MulDiv( REMU(rd, rs1, rs2)) => Rtype(opc(0x0C), 7, rd, rs1, rs2, '0000001') 4789 4790 case MulDiv( MULW(rd, rs1, rs2)) => Rtype(opc(0x0E), 0, rd, rs1, rs2, '0000001') 4791 case MulDiv( DIVW(rd, rs1, rs2)) => Rtype(opc(0x0E), 4, rd, rs1, rs2, '0000001') 4792 case MulDiv( DIVUW(rd, rs1, rs2)) => Rtype(opc(0x0E), 5, rd, rs1, rs2, '0000001') 4793 case MulDiv( REMW(rd, rs1, rs2)) => Rtype(opc(0x0E), 6, rd, rs1, rs2, '0000001') 4794 case MulDiv( REMUW(rd, rs1, rs2)) => Rtype(opc(0x0E), 7, rd, rs1, rs2, '0000001') 4795 4796 case Load( LB(rd, rs1, imm)) => Itype(opc(0x00), 0, rd, rs1, imm) 4797 case Load( LH(rd, rs1, imm)) => Itype(opc(0x00), 1, rd, rs1, imm) 4798 case Load( LW(rd, rs1, imm)) => Itype(opc(0x00), 2, rd, rs1, imm) 4799 case Load( LD(rd, rs1, imm)) => Itype(opc(0x00), 3, rd, rs1, imm) 4800 case Load( LBU(rd, rs1, imm)) => Itype(opc(0x00), 4, rd, rs1, imm) 4801 case Load( LHU(rd, rs1, imm)) => Itype(opc(0x00), 5, rd, rs1, imm) 4802 case Load( LWU(rd, rs1, imm)) => Itype(opc(0x00), 6, rd, rs1, imm) 4803 4804 case Store( SB(rs1, rs2, imm)) => Stype(opc(0x08), 0, rs1, rs2, imm) 4805 case Store( SH(rs1, rs2, imm)) => Stype(opc(0x08), 1, rs1, rs2, imm) 4806 case Store( SW(rs1, rs2, imm)) => Stype(opc(0x08), 2, rs1, rs2, imm) 4807 case Store( SD(rs1, rs2, imm)) => Stype(opc(0x08), 3, rs1, rs2, imm) 4808 4809 case FENCE(rd, rs1, pred, succ) => Itype(opc(0x03), 0, rd, rs1, '0000' : pred : succ) 4810 case FENCE_I(rd, rs1, imm) => Itype(opc(0x03), 1, rd, rs1, imm) 4811 4812 case FArith( FADD_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x00) 4813 case FArith( FSUB_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x04) 4814 case FArith( FMUL_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x08) 4815 case FArith( FDIV_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x0c) 4816 case FArith( FSQRT_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x2c) 4817 case FArith( FMIN_S(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x14) 4818 case FArith( FMAX_S(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x14) 4819 case FArith( FEQ_S(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x50) 4820 case FArith( FLT_S(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x50) 4821 case FArith( FLE_S(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x50) 4822 4823 case FArith( FADD_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x01) 4824 case FArith( FSUB_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x05) 4825 case FArith( FMUL_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x09) 4826 case FArith( FDIV_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x0d) 4827 case FArith( FSQRT_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x2d) 4828 case FArith( FMIN_D(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x15) 4829 case FArith( FMAX_D(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x15) 4830 case FArith( FEQ_D(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x51) 4831 case FArith( FLT_D(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x51) 4832 case FArith( FLE_D(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x51) 4833 4834 case FPLoad( FLW(rd, rs1, imm)) => Itype(opc(0x01), 2, rd, rs1, imm) 4835 case FPLoad( FLD(rd, rs1, imm)) => Itype(opc(0x01), 3, rd, rs1, imm) 4836 case FPStore( FSW(rs1, rs2, imm)) => Stype(opc(0x09), 2, rs1, rs2, imm) 4837 case FPStore( FSD(rs1, rs2, imm)) => Stype(opc(0x09), 3, rs1, rs2, imm) 4838 4839 case FArith( FMADD_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x10), frm, rd, rs1, rs2, rs3, 0) 4840 case FArith( FMSUB_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x11), frm, rd, rs1, rs2, rs3, 0) 4841 case FArith(FNMSUB_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x12), frm, rd, rs1, rs2, rs3, 0) 4842 case FArith(FNMADD_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x13), frm, rd, rs1, rs2, rs3, 0) 4843 4844 case FArith( FMADD_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x10), frm, rd, rs1, rs2, rs3, 1) 4845 case FArith( FMSUB_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x11), frm, rd, rs1, rs2, rs3, 1) 4846 case FArith(FNMSUB_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x12), frm, rd, rs1, rs2, rs3, 1) 4847 case FArith(FNMADD_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x13), frm, rd, rs1, rs2, rs3, 1) 4848 4849 case FConv( FSGNJ_S(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x10) 4850 case FConv( FSGNJN_S(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x10) 4851 case FConv( FSGNJX_S(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x10) 4852 4853 case FConv( FCVT_W_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x60) 4854 case FConv(FCVT_WU_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x60) 4855 case FConv( FMV_X_S(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x70) 4856 case FConv( FCLASS_S(rd, rs)) => Rtype(opc(0x14), 1, rd, rs, 0, 0x70) 4857 case FConv( FCVT_S_W(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x68) 4858 case FConv(FCVT_S_WU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x68) 4859 case FConv( FMV_S_X(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x78) 4860 4861 case FConv( FSGNJ_D(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x11) 4862 case FConv( FSGNJN_D(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x11) 4863 case FConv( FSGNJX_D(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x11) 4864 4865 case FConv( FCVT_W_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x61) 4866 case FConv(FCVT_WU_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x61) 4867 case FConv( FCLASS_D(rd, rs)) => Rtype(opc(0x14), 1, rd, rs, 0, 0x71) 4868 case FConv( FCVT_D_W(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x69) 4869 case FConv(FCVT_D_WU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x69) 4870 case FConv( FCVT_S_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x20) 4871 case FConv( FCVT_D_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x21) 4872 4873 case FConv( FCVT_L_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x60) 4874 case FConv(FCVT_LU_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x60) 4875 case FConv( FCVT_S_L(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x68) 4876 case FConv(FCVT_S_LU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x68) 4877 case FConv( FCVT_L_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x61) 4878 case FConv(FCVT_LU_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x61) 4879 case FConv( FMV_X_D(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x71) 4880 case FConv( FCVT_D_L(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x69) 4881 case FConv(FCVT_D_LU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x69) 4882 case FConv( FMV_D_X(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x79) 4883 4884 case AMO( LR_W(aq, rl, rd, rs1)) => Rtype(opc(0x0B), 2, rd, rs1, 0, amofunc('00010', aq, rl)) 4885 case AMO( LR_D(aq, rl, rd, rs1)) => Rtype(opc(0x0B), 3, rd, rs1, 0, amofunc('00010', aq, rl)) 4886 case AMO( SC_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00011', aq, rl)) 4887 case AMO( SC_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00010', aq, rl)) 4888 4889 case AMO(AMOSWAP_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00001', aq, rl)) 4890 case AMO( AMOADD_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00000', aq, rl)) 4891 case AMO( AMOXOR_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00100', aq, rl)) 4892 case AMO( AMOAND_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('01100', aq, rl)) 4893 case AMO( AMOOR_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('01000', aq, rl)) 4894 case AMO( AMOMIN_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('10000', aq, rl)) 4895 case AMO( AMOMAX_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('10100', aq, rl)) 4896 case AMO(AMOMINU_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('11000', aq, rl)) 4897 case AMO(AMOMAXU_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('11100', aq, rl)) 4898 4899 case AMO(AMOSWAP_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00001', aq, rl)) 4900 case AMO( AMOADD_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00000', aq, rl)) 4901 case AMO( AMOXOR_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00100', aq, rl)) 4902 case AMO( AMOAND_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('01100', aq, rl)) 4903 case AMO( AMOOR_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('01000', aq, rl)) 4904 case AMO( AMOMIN_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('10000', aq, rl)) 4905 case AMO( AMOMAX_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('10100', aq, rl)) 4906 case AMO(AMOMINU_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('11000', aq, rl)) 4907 case AMO(AMOMAXU_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('11100', aq, rl)) 4908 4909 case System( ECALL) => Itype(opc(0x1C), 0, 0, 0, 0x000) 4910 case System(EBREAK) => Itype(opc(0x1C), 0, 0, 0, 0x001) 4911 case System( ERET) => Itype(opc(0x1C), 0, 0, 0, 0x100) 4912 case System( MRTS) => Itype(opc(0x1C), 0, 0, 0, 0x305) 4913 case System( WFI) => Itype(opc(0x1C), 0, 0, 0, 0x102) 4914 4915 case System(SFENCE_VM(rs1)) => Itype(opc(0x1C), 0, 0, rs1, 0x101) 4916 4917 case System( CSRRW(rd, rs1, csr)) => Itype(opc(0x1C), 1, rd, rs1, csr) 4918 case System( CSRRS(rd, rs1, csr)) => Itype(opc(0x1C), 2, rd, rs1, csr) 4919 case System( CSRRC(rd, rs1, csr)) => Itype(opc(0x1C), 3, rd, rs1, csr) 4920 case System(CSRRWI(rd, imm, csr)) => Itype(opc(0x1C), 5, rd, imm, csr) 4921 case System(CSRRSI(rd, imm, csr)) => Itype(opc(0x1C), 6, rd, imm, csr) 4922 case System(CSRRCI(rd, imm, csr)) => Itype(opc(0x1C), 7, rd, imm, csr) 4923 4924 case UnknownInstruction => 0 4925 4926 case Internal(FETCH_MISALIGNED(_)) => 0 4927 case Internal(FETCH_FAULT(_)) => 0 4928 } 4929 4930--------------------------------------------------------------------------- 4931-- RVC instruction decoding 4932--------------------------------------------------------------------------- 4933 4934instruction DecodeRVC(h::half) = 4935 match h 4936 { case '000 00000000 rd 00' => UnknownInstruction 4937 case '000 ilo`2 ihi`4 i2`1 i3`1 rd 00' => ArithI(ADDI('01' : rd, 2, '00' : ihi : ilo : i3 : i2 : '00')) 4938 4939 case '001 ilo`3 rs1 ihi`2 rd 00' => FPLoad(FLD('01' : rd, '01' : rs1, '0000' : ihi : ilo : '000' )) 4940 case '010 imi`3 rs1 i2`1 i6`1 rd 00' => Load( LW('01' : rd, '01' : rs1, '00000' : i6 : imi : i2 : '00' )) 4941 case '011 ilo`3 rs1 ihi`2 rd 00' => Load( LD('01' : rd, '01' : rs1, '0000' : ihi : ilo : '000' )) 4942 4943 case '101 ilo`3 rs1 ihi`2 rs2 00' => FPStore(FSD('01' : rs1, '01' : rs2, '0000' : ihi : ilo : '000' )) 4944 case '110 imi`3 rs1 i2`1 i6`1 rs2 00' => Store( SW('01' : rs1, '01' : rs2, '00000' : i6 : imi : i2 : '00' )) 4945 case '111 ilo`3 rs1 ihi`2 rs2 00' => Store( SD('01' : rs1, '01' : rs2, '0000' : ihi : ilo : '000' )) 4946 4947 case '000 0 00000 00000 01' => ArithI(ADDI(0, 0, 0)) 4948 4949 case '000 i5`1 r imi`5 01' => ArithI( ADDI( r, r, i5 ^ 7 : imi)) 4950 case '001 i5`1 r imi`5 01' => ArithI(ADDIW( r, r, i5 ^ 7 : imi)) 4951 case '010 i5`1 rd imi`5 01' => ArithI( ADDI(rd, 0, i5 ^ 7 : imi)) 4952 case '011 0 00010 00000 01' => UnknownInstruction 4953 case '011 i9`1 00010 i4`1 i6`1 imi`2 i5`1 01' => ArithI( ADDI( 2, 2, i9 ^ 3 : imi : i6 : i5 : i4 : '0000')) 4954 4955 case '011 0 rd 00000 01' => UnknownInstruction 4956 case '011 i17`1 rd imi`5 01' => ArithI(LUI(rd, i17 ^ 15 : imi)) 4957 4958 case '100 i5`1 00 r imi`5 01' => Shift(SRLI('01' : r, '01' : r, i5 : imi)) 4959 case '100 i5`1 01 r imi`5 01' => Shift(SRAI('01' : r, '01' : r, i5 : imi)) 4960 4961 case '100 i5`1 10 r imi`5 01' => ArithI(ANDI('01' : r, '01' : r, i5 ^ 7 : imi)) 4962 4963 case '100 0 11 r 00 rs2 01' => ArithR( SUB('01' : r, '01' : r, '01' : rs2)) 4964 case '100 0 11 r 01 rs2 01' => ArithR( XOR('01' : r, '01' : r, '01' : rs2)) 4965 case '100 0 11 r 10 rs2 01' => ArithR( OR('01' : r, '01' : r, '01' : rs2)) 4966 case '100 0 11 r 11 rs2 01' => ArithR( AND('01' : r, '01' : r, '01' : rs2)) 4967 case '100 1 11 r 00 rs2 01' => ArithR(SUBW('01' : r, '01' : r, '01' : rs2)) 4968 case '100 1 11 r 01 rs2 01' => ArithR(ADDW('01' : r, '01' : r, '01' : rs2)) 4969 4970 case '101 i11`1 i4`1 ihi`2 i10`1 i6`1 i7`1 ilo`3 i5`1 01' => Branch(JAL(0, i11 ^ 10 : i10 : ihi : i7 : i6 : i5 : i4 : ilo)) 4971 4972 case '110 i8`1 imi`2 rs1 ihi`2 ilo`2 i5`1 01' => Branch(BEQ('01' : rs1, 0, i8 ^ 5 : ihi : i5 : imi : ilo)) 4973 case '111 i8`1 imi`2 rs1 ihi`2 ilo`2 i5`1 01' => Branch(BNE('01' : rs1, 0, i8 ^ 5 : ihi : i5 : imi : ilo)) 4974 4975 case '000 i5`1 r imi`5 10' => Shift(SLLI(r, r, i5 : imi)) 4976 4977 case '001 i5`1 rd ilo`2 ihi`3 10' => FPLoad(FLD(rd, 2, '000' : ihi : i5 : ilo : '000')) 4978 case '010 i5`1 00000 ilo`3 ihi`2 10' => UnknownInstruction 4979 case '010 i5`1 rd ilo`3 ihi`2 10' => Load( LW(rd, 2, '0000' : ihi : i5 : ilo : '00' )) 4980 case '011 i5`1 00000 ilo`2 ihi`3 10' => UnknownInstruction 4981 case '011 i5`1 rd ilo`2 ihi`3 10' => Load( LD(rd, 2, '000' : ihi : i5 : ilo : '000')) 4982 4983 case '100 0 00000 00000 10' => UnknownInstruction 4984 case '100 0 rs1 00000 10' => Branch(JALR( 0, rs1, 0)) 4985 case '100 0 rd rs2 10' => ArithR( ADD(rd, 0, rs2)) 4986 case '100 1 00000 00000 10' => System(EBREAK) 4987 case '100 1 rs1 00000 10' => Branch(JALR( 1, rs1, 0)) 4988 case '100 1 r rs2 10' => ArithR( ADD( r, r, rs2)) 4989 4990 case '101 ilo`3 ihi`3 rs2 10' => FPStore(FSD(2, rs2, '000' : ihi : ilo : '000')) 4991 case '110 ilo`4 ihi`2 rs2 10' => Store( SW(2, rs2, '0000' : ihi : ilo : '00' )) 4992 case '111 ilo`3 ihi`3 rs2 10' => Store( SD(2, rs2, '000' : ihi : ilo : '000')) 4993 4994 case _ => UnknownInstruction 4995 } 4996 4997type rvcreg = bits(3) 4998 4999half CBtype(o::bits(2), f3::bits(3), rs1::rvcreg, imm::bits(8)) = 5000 f3 : [imm<7>]::bits(1) : imm<3:2> : rs1 : imm<6:5> : imm<1:0> : [imm<5>]::bits(1) : o 5001 5002construct rvc { Comp :: half, Full :: word } 5003 5004rvc EncodeRVC(i::instruction) = 5005 match i 5006 { case Branch( BEQ('01 rs1', '00000', '00000 imm')) => Comp(CBtype(1, 0, rs1, '0' : imm)) 5007 case Branch( BEQ('01 rs1', '00000', '11111 imm')) => Comp(CBtype(1, 0, rs1, '1' : imm)) 5008 -- case Branch( BNE(rs1, rs2, imm)) => SBtype(opc(0x18), 1, rs1, rs2, imm) 5009 -- case Branch( BLT(rs1, rs2, imm)) => SBtype(opc(0x18), 4, rs1, rs2, imm) 5010 -- case Branch( BGE(rs1, rs2, imm)) => SBtype(opc(0x18), 5, rs1, rs2, imm) 5011 -- case Branch( BLTU(rs1, rs2, imm)) => SBtype(opc(0x18), 6, rs1, rs2, imm) 5012 -- case Branch( BGEU(rs1, rs2, imm)) => SBtype(opc(0x18), 7, rs1, rs2, imm) 5013 5014 -- case Branch( JALR(rd, rs1, imm)) => Itype(opc(0x19), 0, rd, rs1, imm) 5015 -- case Branch( JAL(rd, imm)) => UJtype(opc(0x1b), rd, imm) 5016 5017 -- case ArithI( LUI(rd, imm)) => Utype(opc(0x0D), rd, imm) 5018 -- case ArithI(AUIPC(rd, imm)) => Utype(opc(0x05), rd, imm) 5019 5020 -- case ArithI( ADDI(rd, rs1, imm)) => Itype(opc(0x04), 0, rd, rs1, imm) 5021 -- case Shift( SLLI(rd, rs1, imm)) => Itype(opc(0x04), 1, rd, rs1, '000000' : imm) 5022 -- case ArithI( SLTI(rd, rs1, imm)) => Itype(opc(0x04), 2, rd, rs1, imm) 5023 -- case ArithI(SLTIU(rd, rs1, imm)) => Itype(opc(0x04), 3, rd, rs1, imm) 5024 -- case ArithI( XORI(rd, rs1, imm)) => Itype(opc(0x04), 4, rd, rs1, imm) 5025 -- case Shift( SRLI(rd, rs1, imm)) => Itype(opc(0x04), 5, rd, rs1, '000000' : imm) 5026 -- case Shift( SRAI(rd, rs1, imm)) => Itype(opc(0x04), 5, rd, rs1, '010000' : imm) 5027 -- case ArithI( ORI(rd, rs1, imm)) => Itype(opc(0x04), 6, rd, rs1, imm) 5028 -- case ArithI( ANDI(rd, rs1, imm)) => Itype(opc(0x04), 7, rd, rs1, imm) 5029 5030 -- case ArithR( ADD(rd, rs1, rs2)) => Rtype(opc(0x0C), 0, rd, rs1, rs2, 0) 5031 -- case ArithR( SUB(rd, rs1, rs2)) => Rtype(opc(0x0C), 0, rd, rs1, rs2, 0x20) 5032 -- case Shift( SLL(rd, rs1, rs2)) => Rtype(opc(0x0C), 1, rd, rs1, rs2, 0) 5033 -- case ArithR( SLT(rd, rs1, rs2)) => Rtype(opc(0x0C), 2, rd, rs1, rs2, 0) 5034 -- case ArithR( SLTU(rd, rs1, rs2)) => Rtype(opc(0x0C), 3, rd, rs1, rs2, 0) 5035 -- case ArithR( XOR(rd, rs1, rs2)) => Rtype(opc(0x0C), 4, rd, rs1, rs2, 0) 5036 -- case Shift( SRL(rd, rs1, rs2)) => Rtype(opc(0x0C), 5, rd, rs1, rs2, 0) 5037 -- case Shift( SRA(rd, rs1, rs2)) => Rtype(opc(0x0C), 5, rd, rs1, rs2, 0x20) 5038 -- case ArithR( OR(rd, rs1, rs2)) => Rtype(opc(0x0C), 6, rd, rs1, rs2, 0) 5039 -- case ArithR( AND(rd, rs1, rs2)) => Rtype(opc(0x0C), 7, rd, rs1, rs2, 0) 5040 5041 -- case ArithI(ADDIW(rd, rs1, imm)) => Itype(opc(0x06), 0, rd, rs1, imm) 5042 -- case Shift(SLLIW(rd, rs1, imm)) => Itype(opc(0x06), 1, rd, rs1, '0000000' : imm) 5043 -- case Shift(SRLIW(rd, rs1, imm)) => Itype(opc(0x06), 5, rd, rs1, '0000000' : imm) 5044 -- case Shift(SRAIW(rd, rs1, imm)) => Itype(opc(0x06), 5, rd, rs1, '0100000' : imm) 5045 5046 -- case ArithR( ADDW(rd, rs1, rs2)) => Rtype(opc(0x0E), 0, rd, rs1, rs2, '0000000') 5047 -- case ArithR( SUBW(rd, rs1, rs2)) => Rtype(opc(0x0E), 0, rd, rs1, rs2, '0100000') 5048 -- case Shift( SLLW(rd, rs1, rs2)) => Rtype(opc(0x0E), 1, rd, rs1, rs2, '0000000') 5049 -- case Shift( SRLW(rd, rs1, rs2)) => Rtype(opc(0x0E), 5, rd, rs1, rs2, '0000000') 5050 -- case Shift( SRAW(rd, rs1, rs2)) => Rtype(opc(0x0E), 5, rd, rs1, rs2, '0100000') 5051 5052 -- case MulDiv( MUL(rd, rs1, rs2)) => Rtype(opc(0x0C), 0, rd, rs1, rs2, '0000001') 5053 -- case MulDiv( MULH(rd, rs1, rs2)) => Rtype(opc(0x0C), 1, rd, rs1, rs2, '0000001') 5054 -- case MulDiv( MULHSU(rd, rs1, rs2)) => Rtype(opc(0x0C), 2, rd, rs1, rs2, '0000001') 5055 -- case MulDiv( MULHU(rd, rs1, rs2)) => Rtype(opc(0x0C), 3, rd, rs1, rs2, '0000001') 5056 -- case MulDiv( DIV(rd, rs1, rs2)) => Rtype(opc(0x0C), 4, rd, rs1, rs2, '0000001') 5057 -- case MulDiv( DIVU(rd, rs1, rs2)) => Rtype(opc(0x0C), 5, rd, rs1, rs2, '0000001') 5058 -- case MulDiv( REM(rd, rs1, rs2)) => Rtype(opc(0x0C), 6, rd, rs1, rs2, '0000001') 5059 -- case MulDiv( REMU(rd, rs1, rs2)) => Rtype(opc(0x0C), 7, rd, rs1, rs2, '0000001') 5060 5061 -- case MulDiv( MULW(rd, rs1, rs2)) => Rtype(opc(0x0E), 0, rd, rs1, rs2, '0000001') 5062 -- case MulDiv( DIVW(rd, rs1, rs2)) => Rtype(opc(0x0E), 4, rd, rs1, rs2, '0000001') 5063 -- case MulDiv( DIVUW(rd, rs1, rs2)) => Rtype(opc(0x0E), 5, rd, rs1, rs2, '0000001') 5064 -- case MulDiv( REMW(rd, rs1, rs2)) => Rtype(opc(0x0E), 6, rd, rs1, rs2, '0000001') 5065 -- case MulDiv( REMUW(rd, rs1, rs2)) => Rtype(opc(0x0E), 7, rd, rs1, rs2, '0000001') 5066 5067 -- case Load( LB(rd, rs1, imm)) => Itype(opc(0x00), 0, rd, rs1, imm) 5068 -- case Load( LH(rd, rs1, imm)) => Itype(opc(0x00), 1, rd, rs1, imm) 5069 -- case Load( LW(rd, rs1, imm)) => Itype(opc(0x00), 2, rd, rs1, imm) 5070 -- case Load( LD(rd, rs1, imm)) => Itype(opc(0x00), 3, rd, rs1, imm) 5071 -- case Load( LBU(rd, rs1, imm)) => Itype(opc(0x00), 4, rd, rs1, imm) 5072 -- case Load( LHU(rd, rs1, imm)) => Itype(opc(0x00), 5, rd, rs1, imm) 5073 -- case Load( LWU(rd, rs1, imm)) => Itype(opc(0x00), 6, rd, rs1, imm) 5074 5075 -- case Store( SB(rs1, rs2, imm)) => Stype(opc(0x08), 0, rs1, rs2, imm) 5076 -- case Store( SH(rs1, rs2, imm)) => Stype(opc(0x08), 1, rs1, rs2, imm) 5077 -- case Store( SW(rs1, rs2, imm)) => Stype(opc(0x08), 2, rs1, rs2, imm) 5078 -- case Store( SD(rs1, rs2, imm)) => Stype(opc(0x08), 3, rs1, rs2, imm) 5079 5080 -- case FENCE(rd, rs1, pred, succ) => Itype(opc(0x03), 0, rd, rs1, '0000' : pred : succ) 5081 -- case FENCE_I(rd, rs1, imm) => Itype(opc(0x03), 1, rd, rs1, imm) 5082 5083 -- case FArith( FADD_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x00) 5084 -- case FArith( FSUB_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x04) 5085 -- case FArith( FMUL_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x08) 5086 -- case FArith( FDIV_S(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x0c) 5087 -- case FArith( FSQRT_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x2c) 5088 -- case FArith( FMIN_S(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x14) 5089 -- case FArith( FMAX_S(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x14) 5090 -- case FArith( FEQ_S(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x50) 5091 -- case FArith( FLT_S(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x50) 5092 -- case FArith( FLE_S(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x50) 5093 5094 -- case FArith( FADD_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x01) 5095 -- case FArith( FSUB_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x05) 5096 -- case FArith( FMUL_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x09) 5097 -- case FArith( FDIV_D(rd, rs1, rs2, frm)) => Rtype(opc(0x14), frm, rd, rs1, rs2, 0x0d) 5098 -- case FArith( FSQRT_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x2d) 5099 -- case FArith( FMIN_D(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x15) 5100 -- case FArith( FMAX_D(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x15) 5101 -- case FArith( FEQ_D(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x51) 5102 -- case FArith( FLT_D(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x51) 5103 -- case FArith( FLE_D(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x51) 5104 5105 -- case FPLoad( FLW(rd, rs1, imm)) => Itype(opc(0x01), 2, rd, rs1, imm) 5106 -- case FPLoad( FLD(rd, rs1, imm)) => Itype(opc(0x01), 3, rd, rs1, imm) 5107 -- case FPStore( FSW(rs1, rs2, imm)) => Stype(opc(0x09), 2, rs1, rs2, imm) 5108 -- case FPStore( FSD(rs1, rs2, imm)) => Stype(opc(0x09), 3, rs1, rs2, imm) 5109 5110 -- case FArith( FMADD_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x10), frm, rd, rs1, rs2, rs3, 0) 5111 -- case FArith( FMSUB_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x11), frm, rd, rs1, rs2, rs3, 0) 5112 -- case FArith(FNMSUB_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x12), frm, rd, rs1, rs2, rs3, 0) 5113 -- case FArith(FNMADD_S(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x13), frm, rd, rs1, rs2, rs3, 0) 5114 5115 -- case FArith( FMADD_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x10), frm, rd, rs1, rs2, rs3, 1) 5116 -- case FArith( FMSUB_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x11), frm, rd, rs1, rs2, rs3, 1) 5117 -- case FArith(FNMSUB_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x12), frm, rd, rs1, rs2, rs3, 1) 5118 -- case FArith(FNMADD_D(rd, rs1, rs2, rs3, frm)) => R4type(opc(0x13), frm, rd, rs1, rs2, rs3, 1) 5119 5120 -- case FConv( FSGNJ_S(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x10) 5121 -- case FConv( FSGNJN_S(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x10) 5122 -- case FConv( FSGNJX_S(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x10) 5123 5124 -- case FConv( FCVT_W_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x60) 5125 -- case FConv(FCVT_WU_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x60) 5126 -- case FConv( FMV_X_S(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x70) 5127 -- case FConv( FCLASS_S(rd, rs)) => Rtype(opc(0x14), 1, rd, rs, 0, 0x70) 5128 -- case FConv( FCVT_S_W(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x68) 5129 -- case FConv(FCVT_S_WU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x68) 5130 -- case FConv( FMV_S_X(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x78) 5131 5132 -- case FConv( FSGNJ_D(rd, rs1, rs2)) => Rtype(opc(0x14), 0, rd, rs1, rs2, 0x11) 5133 -- case FConv( FSGNJN_D(rd, rs1, rs2)) => Rtype(opc(0x14), 1, rd, rs1, rs2, 0x11) 5134 -- case FConv( FSGNJX_D(rd, rs1, rs2)) => Rtype(opc(0x14), 2, rd, rs1, rs2, 0x11) 5135 5136 -- case FConv( FCVT_W_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x61) 5137 -- case FConv(FCVT_WU_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x61) 5138 -- case FConv( FCLASS_D(rd, rs)) => Rtype(opc(0x14), 1, rd, rs, 0, 0x71) 5139 -- case FConv( FCVT_D_W(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x69) 5140 -- case FConv(FCVT_D_WU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x69) 5141 -- case FConv( FCVT_S_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 1, 0x20) 5142 -- case FConv( FCVT_D_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 0, 0x21) 5143 5144 -- case FConv( FCVT_L_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x60) 5145 -- case FConv(FCVT_LU_S(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x60) 5146 -- case FConv( FCVT_S_L(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x68) 5147 -- case FConv(FCVT_S_LU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x68) 5148 -- case FConv( FCVT_L_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x61) 5149 -- case FConv(FCVT_LU_D(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x61) 5150 -- case FConv( FMV_X_D(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x71) 5151 -- case FConv( FCVT_D_L(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 2, 0x69) 5152 -- case FConv(FCVT_D_LU(rd, rs, frm)) => Rtype(opc(0x14), frm, rd, rs, 3, 0x69) 5153 -- case FConv( FMV_D_X(rd, rs)) => Rtype(opc(0x14), 0, rd, rs, 0, 0x79) 5154 5155 -- case AMO( LR_W(aq, rl, rd, rs1)) => Rtype(opc(0x0B), 2, rd, rs1, 0, amofunc('00010', aq, rl)) 5156 -- case AMO( LR_D(aq, rl, rd, rs1)) => Rtype(opc(0x0B), 3, rd, rs1, 0, amofunc('00010', aq, rl)) 5157 -- case AMO( SC_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00011', aq, rl)) 5158 -- case AMO( SC_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00010', aq, rl)) 5159 5160 -- case AMO(AMOSWAP_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00001', aq, rl)) 5161 -- case AMO( AMOADD_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00000', aq, rl)) 5162 -- case AMO( AMOXOR_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('00100', aq, rl)) 5163 -- case AMO( AMOAND_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('01100', aq, rl)) 5164 -- case AMO( AMOOR_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('01000', aq, rl)) 5165 -- case AMO( AMOMIN_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('10000', aq, rl)) 5166 -- case AMO( AMOMAX_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('10100', aq, rl)) 5167 -- case AMO(AMOMINU_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('11000', aq, rl)) 5168 -- case AMO(AMOMAXU_W(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 2, rd, rs1, rs2, amofunc('11100', aq, rl)) 5169 5170 -- case AMO(AMOSWAP_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00001', aq, rl)) 5171 -- case AMO( AMOADD_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00000', aq, rl)) 5172 -- case AMO( AMOXOR_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('00100', aq, rl)) 5173 -- case AMO( AMOAND_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('01100', aq, rl)) 5174 -- case AMO( AMOOR_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('01000', aq, rl)) 5175 -- case AMO( AMOMIN_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('10000', aq, rl)) 5176 -- case AMO( AMOMAX_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('10100', aq, rl)) 5177 -- case AMO(AMOMINU_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('11000', aq, rl)) 5178 -- case AMO(AMOMAXU_D(aq, rl, rd, rs1, rs2)) => Rtype(opc(0x0B), 3, rd, rs1, rs2, amofunc('11100', aq, rl)) 5179 5180 -- case System( ECALL) => Itype(opc(0x1C), 0, 0, 0, 0x000) 5181 -- case System(EBREAK) => Itype(opc(0x1C), 0, 0, 0, 0x001) 5182 -- case System( ERET) => Itype(opc(0x1C), 0, 0, 0, 0x100) 5183 -- case System( MRTS) => Itype(opc(0x1C), 0, 0, 0, 0x305) 5184 -- case System( WFI) => Itype(opc(0x1C), 0, 0, 0, 0x102) 5185 5186 -- case System(SFENCE_VM(rs1)) => Itype(opc(0x1C), 0, 0, rs1, 0x101) 5187 5188 -- case System( CSRRW(rd, rs1, csr)) => Itype(opc(0x1C), 1, rd, rs1, csr) 5189 -- case System( CSRRS(rd, rs1, csr)) => Itype(opc(0x1C), 2, rd, rs1, csr) 5190 -- case System( CSRRC(rd, rs1, csr)) => Itype(opc(0x1C), 3, rd, rs1, csr) 5191 -- case System(CSRRWI(rd, imm, csr)) => Itype(opc(0x1C), 5, rd, imm, csr) 5192 -- case System(CSRRSI(rd, imm, csr)) => Itype(opc(0x1C), 6, rd, imm, csr) 5193 -- case System(CSRRCI(rd, imm, csr)) => Itype(opc(0x1C), 7, rd, imm, csr) 5194 5195 -- case UnknownInstruction => 0 5196 5197 -- case Internal(FETCH_MISALIGNED(_)) => 0 5198 -- case Internal(FETCH_FAULT(_)) => 0 5199 case _ => Full(Encode(i)) 5200 } 5201 5202--------------------------------------------------------------------------- 5203-- The next state function 5204--------------------------------------------------------------------------- 5205 5206string log_instruction(w::word, inst::instruction) = 5207 "instr " : [procID] : " " : [[c_instret(procID)]::nat] : 5208 " 0x" : hex64(PC) : " : " : hex32(w) : " " : instructionToString(inst) 5209 5210declare done :: bool -- Flag to request termination 5211 5212nat exitCode() = 5213 [ExitCode]::nat 5214 5215-- The clock/timer factor here is arbitrary, except it that if it is 5216-- >= approx 200, some 32-bit -pt- tests unexpectedly pass. 5217 5218nat CYCLES_PER_TIMER_TICK = 200 5219 5220unit tickClock() = 5221{ cycles = c_cycles(procID) + 1 5222; c_cycles(procID) <- cycles 5223; clock <- cycles div [CYCLES_PER_TIMER_TICK] 5224} 5225 5226unit incrInstret() = 5227 c_instret(procID) <- c_instret(procID) + 1 5228 5229unit checkTimers() = 5230{ when (clock >+ MCSR.mtimecmp + MCSR.mtime_delta) 5231 do MCSR.mip.MTIP <- true 5232; when (clock >+ SCSR.stimecmp + SCSR.stime_delta) 5233 do MCSR.mip.STIP <- true 5234} 5235 5236unit Next = 5237{ clear_logs() 5238 5239-- Handle the char i/o section of the Berkeley HTIF protocol 5240-- following cissrStandalone.c. 5241; when MCSR.mtohost <> 0x0 5242 do { mark_log(LOG_IO, log_tohost(MCSR.mtohost)) 5243 -- The HTIF protocol sets bit 0 to indicate exit, with actual 5244 -- exit code left-shifted by 1 bit. 5245 ; if MCSR.mtohost<0> 5246 then { done <- true 5247 ; ExitCode <- MCSR.mtohost >> 1 5248 } 5249 else MCSR.mtohost <- 0x0 -- TODO: rest of relevant HTIF protocol 5250 } 5251 5252; match Fetch() 5253 { case F_Result(Half(h)) => 5254 { inst = DecodeRVC(h) 5255 ; mark_log(LOG_INSN, log_instruction(ZeroExtend(h), inst)) 5256 ; Run(inst) 5257 } 5258 case F_Result(Word(w)) => 5259 { inst = Decode(w) 5260 ; mark_log(LOG_INSN, log_instruction(w, inst)) 5261 ; Run(inst) 5262 } 5263 case F_Error(inst) => 5264 { mark_log(LOG_INSN, log_instruction([0::word], inst)) 5265 ; Run(inst) 5266 } 5267 } 5268 5269; checkTimers() -- this can trigger timer interrupts 5270 5271; match NextFetch, checkInterrupts() 5272 { case None, None => 5273 { incrInstret() 5274 ; PC <- PC + Skip 5275 } 5276 case None, Some(i, p) => 5277 { incrInstret() 5278 ; takeTrap(true, interruptIndex(i), PC + Skip, None, p) 5279 } 5280 case Some(BranchTo(addr)), _ => 5281 { incrInstret() 5282 ; NextFetch <- None 5283 ; PC <- addr 5284 } 5285 case Some(Ereturn), _ => 5286 { incrInstret() 5287 ; NextFetch <- None 5288 ; PC <- curEPC() 5289 5290 ; from = curPrivilege() 5291 ; MCSR.mstatus <- popPrivilegeStack(MCSR.mstatus) 5292 ; to = curPrivilege() 5293 5294 ; mark_log(LOG_INSN, ["exception return from " : privName(from) 5295 : " to " : privName(to)]) 5296 } 5297 case Some(Trap(t)), _ => 5298 { NextFetch <- None 5299 -- We currently don't implement delegation, so always trap to M-mode. 5300 ; takeTrap(false, excCode(t.trap), PC, t.badaddr, Machine) 5301 } 5302 case Some(Mrts), _ => 5303 { incrInstret() 5304 ; NextFetch <- None 5305 ; PC <- SCSR.stvec 5306 } 5307 } 5308 5309; tickClock() 5310} 5311 5312unit initIdent(arch::Architecture) = 5313{ MCSR.mcpuid.ArchBase <- archBase(arch) 5314; MCSR.mcpuid.U <- true 5315; MCSR.mcpuid.S <- true 5316; MCSR.mcpuid.M <- true 5317; MCSR.mcpuid.I <- true 5318 5319; MCSR.mimpid.RVSource <- 0x8000 -- anonymous source 5320; MCSR.mimpid.RVImpl <- 0x0 5321} 5322 5323unit initMachine(hartid::id) = 5324{ -- Startup in Mbare machine mode, with interrupts disabled. 5325 MCSR.mstatus.VM <- vmMode(Mbare) 5326; MCSR.mstatus.MPRV <- privLevel(Machine) 5327; MCSR.mstatus.MIE <- false 5328 -- initialize extension context state 5329; MCSR.mstatus.MFS <- ext_status(Initial) 5330; MCSR.mstatus.MXS <- ext_status(Off) 5331; MCSR.mstatus.MSD <- false 5332 5333 -- MPRV1/MIE1 and MPRV2/MIE2 are unspecified. 5334 5335 -- Setup hartid 5336; MCSR.mhartid <- ZeroExtend(hartid) 5337 -- Initialize mtvec to lower address (other option is 0xF...FFE00) 5338; MCSR.mtvec <- ZeroExtend(0x100`16) 5339} 5340-- This initializes each core (via setting procID appropriately) on 5341-- startup before execution begins. 5342unit initRegs(pc::nat) = 5343{ -- TODO: Check if the specs specify the initial values of the registers 5344 -- on startup. Initializing to an arbitrary value causes issues with 5345 -- the verifier, which assumes 0-valued initialization. 5346 for i in 0 .. 31 do 5347 gpr([i]) <- 0x0 5348; for i in 0 .. 31 do 5349 fpr([i]) <- 0x0 5350 5351; PC <- [pc] 5352; NextFetch <- None 5353; done <- false 5354} 5355