Lines Matching defs:x0
1492 val MEM8 = ref (Map.mkMap(SOME 18446744073709551616,BitsN.B(0x0,8)))
1495 val c_ExitCode = ref (Map.mkMap(SOME 256,BitsN.B(0x0,64)))
1501 {hbadaddr = BitsN.B(0x0,64),
1503 {EC = BitsN.B(0x0,4), Int = false, mcause'rst = BitsN.B(0x0,59)},
1504 hepc = BitsN.B(0x0,64), hscratch = BitsN.B(0x0,64),
1506 {MFS = BitsN.B(0x0,2), MIE = false, MIE1 = false, MIE2 = false,
1507 MIE3 = false, MMPRV = false, MPRV = BitsN.B(0x0,2),
1508 MPRV1 = BitsN.B(0x0,2), MPRV2 = BitsN.B(0x0,2),
1509 MPRV3 = BitsN.B(0x0,2), MSD = false, MXS = BitsN.B(0x0,2),
1510 VM = BitsN.B(0x0,5), mstatus'rst = BitsN.B(0x0,41)},
1512 {Exc_deleg = BitsN.B(0x0,16), Intr_deleg = BitsN.B(0x0,48)},
1513 htime_delta = BitsN.B(0x0,64), htimecmp = BitsN.B(0x0,64),
1514 htvec = BitsN.B(0x0,64)})): (HypervisorCSR Map.map) ref
1519 {mbadaddr = BitsN.B(0x0,64), mbase = BitsN.B(0x0,64),
1520 mbound = BitsN.B(0x0,64),
1522 {EC = BitsN.B(0x0,4), Int = false, mcause'rst = BitsN.B(0x0,59)},
1524 {ArchBase = BitsN.B(0x0,2), I = false, M = false, S = false,
1525 U = false, mcpuid'rst = BitsN.B(0x0,58)},
1526 mdbase = BitsN.B(0x0,64), mdbound = BitsN.B(0x0,64),
1527 mepc = BitsN.B(0x0,64), mfromhost = BitsN.B(0x0,64),
1528 mhartid = BitsN.B(0x0,64), mibase = BitsN.B(0x0,64),
1529 mibound = BitsN.B(0x0,64),
1532 SSIE = false, STIE = false, mie'rst = BitsN.B(0x0,58)},
1533 mimpid = {RVImpl = BitsN.B(0x0,48), RVSource = BitsN.B(0x0,16)},
1536 SSIP = false, STIP = false, mip'rst = BitsN.B(0x0,58)},
1537 mscratch = BitsN.B(0x0,64),
1539 {MFS = BitsN.B(0x0,2), MIE = false, MIE1 = false, MIE2 = false,
1540 MIE3 = false, MMPRV = false, MPRV = BitsN.B(0x0,2),
1541 MPRV1 = BitsN.B(0x0,2), MPRV2 = BitsN.B(0x0,2),
1542 MPRV3 = BitsN.B(0x0,2), MSD = false, MXS = BitsN.B(0x0,2),
1543 VM = BitsN.B(0x0,5), mstatus'rst = BitsN.B(0x0,41)},
1545 {Exc_deleg = BitsN.B(0x0,16), Intr_deleg = BitsN.B(0x0,48)},
1546 mtime_delta = BitsN.B(0x0,64), mtimecmp = BitsN.B(0x0,64),
1547 mtohost = BitsN.B(0x0,64), mtvec = BitsN.B(0x0,64)}))
1553 val c_PC = ref (Map.mkMap(SOME 256,BitsN.B(0x0,64)))
1562 {sasid = BitsN.B(0x0,64), sbadaddr = BitsN.B(0x0,64),
1564 {EC = BitsN.B(0x0,4), Int = false, mcause'rst = BitsN.B(0x0,59)},
1565 sepc = BitsN.B(0x0,64), sptbr = BitsN.B(0x0,64),
1566 sscratch = BitsN.B(0x0,64), stime_delta = BitsN.B(0x0,64),
1567 stimecmp = BitsN.B(0x0,64), stvec = BitsN.B(0x0,64)}))
1573 {cycle_delta = BitsN.B(0x0,64),
1575 {DZ = false, FRM = BitsN.B(0x0,3), NV = false, NX = false,
1576 OF = false, UF = false, fpcsr'rst = BitsN.B(0x0,24)},
1577 instret_delta = BitsN.B(0x0,64), time_delta = BitsN.B(0x0,64)}))
1580 val c_cycles = ref (Map.mkMap(SOME 256,BitsN.B(0x0,64)))
1583 val c_fpr = ref (Map.mkMap(SOME 256,Map.mkMap(SOME 32,BitsN.B(0x0,64))))
1586 val c_gpr = ref (Map.mkMap(SOME 256,Map.mkMap(SOME 32,BitsN.B(0x0,64))))
1589 val c_instret = ref (Map.mkMap(SOME 256,BitsN.B(0x0,64)))
1599 fetch_exc = false, fp_data = NONE, pc = BitsN.B(0x0,64),
1600 rinstr = BitsN.B(0x0,32), st_width = NONE}))
1603 val clock = ref (BitsN.B(0x0,64)): BitsN.nbit ref
1609 val procID = ref (BitsN.B(0x0,8)): BitsN.nbit ref
1657 val BYTE = BitsN.B(0x0,3)
1667 RV32I => BitsN.B(0x0,2)
1673 BitsN.B(0x0,_) => RV32I
1685 User => BitsN.B(0x0,2)
1692 BitsN.B(0x0,_) => User
1707 BitsN.B(0x0,_) => Mbare
1723 BitsN.B(0x0,_) => true
1735 Mbare => BitsN.B(0x0,5)
1757 Off => BitsN.B(0x0,2)
1764 BitsN.B(0x0,_) => Off
1778 case i of Software => BitsN.B(0x0,4) | Timer => BitsN.B(0x1,4);
1782 Fetch_Misaligned => BitsN.B(0x0,4)
1796 BitsN.B(0x0,_) => Fetch_Misaligned
2020 val sip = ref (rec'sip(BitsN.B(0x0,64)))
2030 val sie = ref (rec'sie(BitsN.B(0x0,64)))
2087 val st = ref (rec'sstatus(BitsN.B(0x0,64)))
2175 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2179 ((!c_UCSR),BitsN.toNat (!procID),UserCSR_fpcsr_rupd(x0,value)))
2182 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2183 val x1 = #mstatus(x0 : MachineCSR)
2189 (x0,mstatus_MFS_rupd(x1,ext_status Dirty))))
2192 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2193 val x1 = #mstatus(x0 : MachineCSR)
2198 MachineCSR_mstatus_rupd(x0,mstatus_MSD_rupd(x1,true))))
2280 val x0 = Map.lookup((!c_MCSR),BitsN.toNat id)
2281 val x1 = #mip(x0 : MachineCSR)
2286 MachineCSR_mip_rupd(x0,mip_MSIP_rupd(x1,true))))
2293 BitsN.B(0x0,_) => Option.SOME RNE
2303 BitsN.B(0x0,_) => Option.SOME RNE
2335 (not((BitsN.bits(21,0) x) = (BitsN.B(0x0,22)))));
2340 (not((BitsN.bits(50,0) x) = (BitsN.B(0x0,51)))));
2687 | BitsN.B(0x783,_) => BitsN.B(0x0,64)
2695 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2696 val x1 = #fpcsr(x0 : UserCSR)
2703 (x0,
2709 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2710 val x1 = #mstatus(x0 : MachineCSR)
2716 (x0,mstatus_MFS_rupd(x1,ext_status Dirty))))
2719 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2720 val x1 = #mstatus(x0 : MachineCSR)
2725 MachineCSR_mstatus_rupd(x0,mstatus_MSD_rupd(x1,true))))
2730 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2731 val x1 = #fpcsr(x0 : UserCSR)
2737 (x0,FPCSR_FRM_rupd(x1,BitsN.bits(2,0) value))))
2740 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2741 val x1 = #mstatus(x0 : MachineCSR)
2747 (x0,mstatus_MFS_rupd(x1,ext_status Dirty))))
2750 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2751 val x1 = #mstatus(x0 : MachineCSR)
2756 MachineCSR_mstatus_rupd(x0,mstatus_MSD_rupd(x1,true))))
2761 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2762 val x1 = #fpcsr(x0 : UserCSR)
2768 (x0,write'reg'FPCSR(x1,BitsN.bits(31,0) value))))
2771 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2772 val x1 = #mstatus(x0 : MachineCSR)
2778 (x0,mstatus_MFS_rupd(x1,ext_status Dirty))))
2781 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2782 val x1 = #mstatus(x0 : MachineCSR)
2787 MachineCSR_mstatus_rupd(x0,mstatus_MSD_rupd(x1,true))))
2792 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2798 (x0,
2807 val x0 = Map.lookup((!c_SCSR),BitsN.toNat (!procID))
2812 SupervisorCSR_stvec_rupd(x0,value)))
2816 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2822 (x0,
2831 val x0 = Map.lookup((!c_SCSR),BitsN.toNat (!procID))
2836 SupervisorCSR_stimecmp_rupd(x0,value)))
2839 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2840 val x1 = #mip(x0 : MachineCSR)
2845 MachineCSR_mip_rupd(x0,mip_STIP_rupd(x1,false))))
2850 val x0 = Map.lookup((!c_SCSR),BitsN.toNat (!procID))
2855 SupervisorCSR_sscratch_rupd(x0,value)))
2859 val x0 = Map.lookup((!c_SCSR),BitsN.toNat (!procID))
2865 (x0,BitsN.&&(value,BitsN.signExtend 64 (BitsN.B(0x4,3))))))
2869 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2875 (x0,
2884 val x0 = Map.lookup((!c_SCSR),BitsN.toNat (!procID))
2889 SupervisorCSR_sptbr_rupd(x0,value)))
2893 val x0 = Map.lookup((!c_SCSR),BitsN.toNat (!procID))
2898 SupervisorCSR_sasid_rupd(x0,value)))
2902 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2908 (x0,
2913 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2918 UserCSR_time_delta_rupd(x0,BitsN.-(value,(!clock)))))
2922 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2928 (x0,
2934 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2935 val w = #cycle_delta(x0 : UserCSR)
2941 (x0,
2953 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2954 val w = #time_delta(x0 : UserCSR)
2960 (x0,
2970 val x0 = Map.lookup((!c_UCSR),BitsN.toNat (!procID))
2971 val w = #instret_delta(x0 : UserCSR)
2977 (x0,
2989 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
2995 (x0,
3003 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3007 ((!c_MCSR),BitsN.toNat (!procID),MachineCSR_mtvec_rupd(x0,value)))
3011 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3016 MachineCSR_mtdeleg_rupd(x0,rec'mtdeleg value)))
3020 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3025 MachineCSR_mie_rupd(x0,rec'mie value)))
3029 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3034 MachineCSR_mtimecmp_rupd(x0,value)))
3037 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3038 val x1 = #mip(x0 : MachineCSR)
3043 MachineCSR_mip_rupd(x0,mip_MTIP_rupd(x1,false))))
3048 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3053 MachineCSR_mtime_delta_rupd(x0,BitsN.-(value,(!clock)))))
3057 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3058 val w = #mtime_delta(x0 : MachineCSR)
3064 (x0,
3074 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3079 MachineCSR_mscratch_rupd(x0,value)))
3083 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3089 (x0,BitsN.&&(value,BitsN.signExtend 64 (BitsN.B(0x4,3))))))
3093 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3098 MachineCSR_mcause_rupd(x0,rec'mcause value)))
3102 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3107 MachineCSR_mbadaddr_rupd(x0,value)))
3111 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3116 MachineCSR_mip_rupd(x0,rec'mip value)))
3120 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3124 ((!c_MCSR),BitsN.toNat (!procID),MachineCSR_mbase_rupd(x0,value)))
3128 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3133 MachineCSR_mbound_rupd(x0,value)))
3137 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3142 MachineCSR_mibase_rupd(x0,value)))
3146 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3151 MachineCSR_mibound_rupd(x0,value)))
3155 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3160 MachineCSR_mdbase_rupd(x0,value)))
3164 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3169 MachineCSR_mdbound_rupd(x0,value)))
3173 val x0 = Map.lookup((!c_HCSR),BitsN.toNat (!procID))
3178 HypervisorCSR_htime_delta_rupd(x0,BitsN.-(value,(!clock)))))
3182 val x0 = Map.lookup((!c_HCSR),BitsN.toNat (!procID))
3183 val w = #htime_delta(x0 : HypervisorCSR)
3189 (x0,
3199 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3204 MachineCSR_mtohost_rupd(x0,value)))
3208 val x0 = Map.lookup((!c_MCSR),BitsN.toNat (!procID))
3213 MachineCSR_mfromhost_rupd(x0,value)))
3303 if r = (BitsN.B(0x0,5))
3366 if r = (BitsN.B(0x0,5))
3628 val x0 = #mstatus(x : MachineCSR)
3631 (MachineCSR_mstatus_rupd(x,mstatus_MMPRV_rupd(x0,false)))
3646 val x0 = #scause(x : SupervisorCSR)
3649 (SupervisorCSR_scause_rupd(x,mcause_Int_rupd(x0,intr)))
3653 val x0 = #scause(x : SupervisorCSR)
3656 (SupervisorCSR_scause_rupd(x,mcause_EC_rupd(x0,ec)))
3677 val x0 = #mcause(x : MachineCSR)
3680 (MachineCSR_mcause_rupd(x,mcause_Int_rupd(x0,intr)))
3684 val x0 = #mcause(x : MachineCSR)
3686 write'MCSR(MachineCSR_mcause_rupd(x,mcause_EC_rupd(x0,ec)))
3731 fun GPR n = if n = (BitsN.B(0x0,5)) then BitsN.B(0x0,64) else gpr n;
3734 if not(n = (BitsN.B(0x0,5)))
3758 val x0 = #mstatus(x : MachineCSR)
3761 (MachineCSR_mstatus_rupd(x,mstatus_MFS_rupd(x0,ext_status Dirty)))
3765 val x0 = #mstatus(x : MachineCSR)
3767 write'MCSR(MachineCSR_mstatus_rupd(x,mstatus_MSD_rupd(x0,true)))
3781 val x0 = #mstatus(x : MachineCSR)
3784 (MachineCSR_mstatus_rupd(x,mstatus_MFS_rupd(x0,ext_status Dirty)))
3788 val x0 = #mstatus(x : MachineCSR)
3790 write'MCSR(MachineCSR_mstatus_rupd(x,mstatus_MSD_rupd(x0,true)))
3982 BitsN.B(0x0,_) =>
4069 else if ((#PTE_T(pte : SV_PTE)) = (BitsN.B(0x0,4))) orelse
4143 val ent = ref {age = BitsN.B(0x0,64), asid = BitsN.B(0x0,6),
4144 global = false, pAddr = BitsN.B(0x0,64),
4146 {PTE_D = false, PTE_PPNi = BitsN.B(0x0,38), PTE_R = false,
4147 PTE_SW = BitsN.B(0x0,3), PTE_T = BitsN.B(0x0,4), PTE_V = false,
4148 sv_pte'rst = BitsN.B(0x0,16)}, pteAddr = BitsN.B(0x0,64),
4149 vAddr = BitsN.B(0x0,64), vAddrMask = BitsN.B(0x0,64),
4150 vMatchMask = BitsN.B(0x0,64)}
4274 (if ((asid = (BitsN.B(0x0,6))) orelse
4286 (if (asid = (BitsN.B(0x0,6))) orelse
4320 val x0 = #pte((!ent) : TLBEntry)
4324 ((!ent),SV_PTE_PTE_D_rupd(x0,true)))
4616 ( write'GPR(BitsN.signExtend 64 (BitsN.@@(imm,BitsN.B(0x0,12))),rd)
4624 (BitsN.signExtend 64 (BitsN.@@(imm,BitsN.B(0x0,12))))))
4630 (BitsN.+(PC (),BitsN.signExtend 64 (BitsN.@@(imm,BitsN.B(0x0,12)))),
4641 BitsN.signExtend 64 (BitsN.@@(imm,BitsN.B(0x0,12)))))))
5065 if (GPR rs2) = (BitsN.B(0x0,64))
5086 if (GPR rs2) = (BitsN.B(0x0,64))
5115 if v2 = (BitsN.B(0x0,64))
5136 if (GPR rs2) = (BitsN.B(0x0,64))
5161 if s2 = (BitsN.B(0x0,32))
5193 if s2 = (BitsN.B(0x0,32))
5223 if s2 = (BitsN.B(0x0,32))
5255 if s2 = (BitsN.B(0x0,32))
5282 if not((BitsN.bits(1,0) addr) = (BitsN.B(0x0,2)))
5304 if not((BitsN.bits(1,0) addr) = (BitsN.B(0x0,2)))
5772 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
5801 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
5823 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
5860 ; ( write'GPR(BitsN.B(0x0,64),rd)
5866 (x,Option.SOME(BitsN.B(0x0,64))))
5881 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
5919 ; ( write'GPR(BitsN.B(0x0,64),rd)
5925 (x,Option.SOME(BitsN.B(0x0,64))))
5938 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
5989 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6038 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6096 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6152 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6210 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6266 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6324 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6380 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6438 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6494 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6552 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6608 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6666 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6722 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6780 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
6836 if not((BitsN.bits(1,0) vAddr) = (BitsN.B(0x0,2)))
6894 if not((BitsN.bits(2,0) vAddr) = (BitsN.B(0x0,3)))
7124 (BitsN.@@(BitsN.B(0x0,1),BitsN.bits(31,0) (GPR rs)))))
7164 then BitsN.B(0x0,64)
7168 then BitsN.B(0x0,64)
7190 (rd,FP32.fromInt(r,BitsN.toInt(BitsN.@@(BitsN.B(0x0,1),GPR rs))))
7230 then BitsN.B(0x0,64)
7234 then BitsN.B(0x0,64)
7288 then ( ( write'GPR(BitsN.B(0x0,64),rd)
7293 (StateDelta_data1_rupd(x,Option.SOME(BitsN.B(0x0,64))))
7301 IEEEReal.LESS => BitsN.B(0x0,64)
7303 | IEEEReal.GREATER => BitsN.B(0x0,64)
7304 | IEEEReal.UNORDERED => BitsN.B(0x0,64)
7322 then ( ( write'GPR(BitsN.B(0x0,64),rd)
7327 (StateDelta_data1_rupd(x,Option.SOME(BitsN.B(0x0,64))))
7336 | IEEEReal.EQUAL => BitsN.B(0x0,64)
7337 | IEEEReal.GREATER => BitsN.B(0x0,64)
7338 | IEEEReal.UNORDERED => BitsN.B(0x0,64)
7356 then ( ( write'GPR(BitsN.B(0x0,64),rd)
7361 (StateDelta_data1_rupd(x,Option.SOME(BitsN.B(0x0,64))))
7371 | IEEEReal.GREATER => BitsN.B(0x0,64)
7372 | IEEEReal.UNORDERED => BitsN.B(0x0,64)
7386 val ret = ref (BitsN.B(0x0,10))
7614 (BitsN.@@(BitsN.B(0x0,1),BitsN.bits(31,0) (GPR rs)))))
7654 then BitsN.B(0x0,64)
7658 then BitsN.B(0x0,64)
7680 (rd,FP64.fromInt(r,BitsN.toInt(BitsN.@@(BitsN.B(0x0,1),GPR rs))))
7720 then BitsN.B(0x0,64)
7724 then BitsN.B(0x0,64)
7788 then ( ( write'GPR(BitsN.B(0x0,64),rd)
7793 (StateDelta_data1_rupd(x,Option.SOME(BitsN.B(0x0,64))))
7801 IEEEReal.LESS => BitsN.B(0x0,64)
7803 | IEEEReal.GREATER => BitsN.B(0x0,64)
7804 | IEEEReal.UNORDERED => BitsN.B(0x0,64)
7822 then ( ( write'GPR(BitsN.B(0x0,64),rd)
7827 (StateDelta_data1_rupd(x,Option.SOME(BitsN.B(0x0,64))))
7836 | IEEEReal.EQUAL => BitsN.B(0x0,64)
7837 | IEEEReal.GREATER => BitsN.B(0x0,64)
7838 | IEEEReal.UNORDERED => BitsN.B(0x0,64)
7856 then ( ( write'GPR(BitsN.B(0x0,64),rd)
7861 (StateDelta_data1_rupd(x,Option.SOME(BitsN.B(0x0,64))))
7871 | IEEEReal.GREATER => BitsN.B(0x0,64)
7872 | IEEEReal.UNORDERED => BitsN.B(0x0,64)
7886 val ret = ref (BitsN.B(0x0,10))
7966 val x0 = #mstatus(x : MachineCSR)
7970 (x,mstatus_MPRV_rupd(x0,privLevel Supervisor)))
7998 if checkCSROp(csr,(rs1,if rs1 = (BitsN.B(0x0,5)) then Read else Write))
8002 ( if not(rs1 = (BitsN.B(0x0,5)))
8016 if checkCSROp(csr,(rs1,if rs1 = (BitsN.B(0x0,5)) then Read else Write))
8020 ( if not(rs1 = (BitsN.B(0x0,5)))
8035 (csr,(zimm,if zimm = (BitsN.B(0x0,5)) then Read else Write))
8039 ( if not(zimm = (BitsN.B(0x0,5)))
8054 (csr,(zimm,if zimm = (BitsN.B(0x0,5)) then Read else Write))
8058 ( if not(zimm = (BitsN.B(0x0,5)))
8073 (csr,(zimm,if zimm = (BitsN.B(0x0,5)) then Read else Write))
8077 ( if not(zimm = (BitsN.B(0x0,5)))
8095 if rs1 = (BitsN.B(0x0,5)) then NONE else Option.SOME(GPR rs1)
8316 if not((BitsN.bits(1,0) vPC) = (BitsN.B(0x0,2)))
13604 (BitsN.B(0x0,_),BitsN.B(0x0,_)) => ""
13605 | (BitsN.B(0x1,_),BitsN.B(0x0,_)) => ".aq"
13606 | (BitsN.B(0x0,_),BitsN.B(0x1,_)) => ".rl"
13898 SBtype(opc(BitsN.B(0x18,8)),(BitsN.B(0x0,3),(rs1,(rs2,imm))))
13910 Itype(opc(BitsN.B(0x19,8)),(BitsN.B(0x0,3),(rd,(rs1,imm))))
13915 Itype(opc(BitsN.B(0x4,8)),(BitsN.B(0x0,3),(rd,(rs1,imm))))
13919 (BitsN.B(0x1,3),(rd,(rs1,BitsN.@@(BitsN.B(0x0,6),imm)))))
13929 (BitsN.B(0x5,3),(rd,(rs1,BitsN.@@(BitsN.B(0x0,6),imm)))))
13941 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13945 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x20,7))))))
13949 (BitsN.B(0x1,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13953 (BitsN.B(0x2,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13957 (BitsN.B(0x3,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13961 (BitsN.B(0x4,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13965 (BitsN.B(0x5,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13973 (BitsN.B(0x6,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13977 (BitsN.B(0x7,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13979 Itype(opc(BitsN.B(0x6,8)),(BitsN.B(0x0,3),(rd,(rs1,imm))))
13983 (BitsN.B(0x1,3),(rd,(rs1,BitsN.@@(BitsN.B(0x0,7),imm)))))
13987 (BitsN.B(0x5,3),(rd,(rs1,BitsN.@@(BitsN.B(0x0,7),imm)))))
13995 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
13999 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x20,7))))))
14003 (BitsN.B(0x1,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
14007 (BitsN.B(0x5,3),(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
14015 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x1,7))))))
14047 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x1,7))))))
14065 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x0,3),(rd,(rs1,imm))))
14067 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x1,3),(rd,(rs1,imm))))
14069 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x2,3),(rd,(rs1,imm))))
14071 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x3,3),(rd,(rs1,imm))))
14073 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x4,3),(rd,(rs1,imm))))
14075 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x5,3),(rd,(rs1,imm))))
14077 Itype(opc(BitsN.B(0x0,8)),(BitsN.B(0x6,3),(rd,(rs1,imm))))
14079 Stype(opc(BitsN.B(0x8,8)),(BitsN.B(0x0,3),(rs1,(rs2,imm))))
14089 (BitsN.B(0x0,3),(rd,(rs1,BitsN.concat[BitsN.B(0x0,4),pred,succ]))))
14093 Rtype(opc(BitsN.B(0x14,8)),(frm,(rd,(rs1,(rs2,BitsN.B(0x0,7))))))
14103 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x2C,7))))))
14107 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x14,7))))))
14123 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x50,7))))))
14135 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x2D,7))))))
14139 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x15,7))))))
14155 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x51,7))))))
14166 (opc(BitsN.B(0x10,8)),(frm,(rd,(rs1,(rs2,(rs3,BitsN.B(0x0,2)))))))
14169 (opc(BitsN.B(0x11,8)),(frm,(rd,(rs1,(rs2,(rs3,BitsN.B(0x0,2)))))))
14172 (opc(BitsN.B(0x12,8)),(frm,(rd,(rs1,(rs2,(rs3,BitsN.B(0x0,2)))))))
14175 (opc(BitsN.B(0x13,8)),(frm,(rd,(rs1,(rs2,(rs3,BitsN.B(0x0,2)))))))
14191 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x10,7))))))
14203 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x60,7))))))
14211 (BitsN.B(0x0,3),(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x70,7))))))
14215 (BitsN.B(0x1,3),(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x70,7))))))
14219 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x68,7))))))
14227 (BitsN.B(0x0,3),(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x78,7))))))
14231 (BitsN.B(0x0,3),(rd,(rs1,(rs2,BitsN.B(0x11,7))))))
14243 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x61,7))))))
14251 (BitsN.B(0x1,3),(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x71,7))))))
14255 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x69,7))))))
14267 (frm,(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x21,7))))))
14295 (BitsN.B(0x0,3),(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x71,7))))))
14307 (BitsN.B(0x0,3),(rd,(rs,(BitsN.B(0x0,5),BitsN.B(0x79,7))))))
14312 (rd,(rs1,(BitsN.B(0x0,5),amofunc(BitsN.B(0x2,5),(aq,rl)))))))
14317 (rd,(rs1,(BitsN.B(0x0,5),amofunc(BitsN.B(0x2,5),(aq,rl)))))))
14333 (BitsN.B(0x2,3),(rd,(rs1,(rs2,amofunc(BitsN.B(0x0,5),(aq,rl)))))))
14369 (BitsN.B(0x3,3),(rd,(rs1,(rs2,amofunc(BitsN.B(0x0,5),(aq,rl)))))))
14401 (BitsN.B(0x0,3),(BitsN.B(0x0,5),(BitsN.B(0x0,5),BitsN.B(0x0,12)))))
14405 (BitsN.B(0x0,3),(BitsN.B(0x0,5),(BitsN.B(0x0,5),BitsN.B(0x1,12)))))
14409 (BitsN.B(0x0,3),
14410 (BitsN.B(0x0,5),(BitsN.B(0x0,5),BitsN.B(0x100,12)))))
14414 (BitsN.B(0x0,3),
14415 (BitsN.B(0x0,5),(BitsN.B(0x0,5),BitsN.B(0x305,12)))))
14419 (BitsN.B(0x0,3),
14420 (BitsN.B(0x0,5),(BitsN.B(0x0,5),BitsN.B(0x102,12)))))
14424 (BitsN.B(0x0,3),(BitsN.B(0x0,5),(rs1,BitsN.B(0x101,12)))))
14437 | UnknownInstruction => BitsN.B(0x0,32)
14438 | Internal(FETCH_MISALIGNED _) => BitsN.B(0x0,32)
14439 | Internal(FETCH_FAULT _) => BitsN.B(0x0,32);
14478 val x0 = #mip(x : MachineCSR)
14480 write'MCSR(MachineCSR_mip_rupd(x,mip_MTIP_rupd(x0,true)))
14490 val x0 = #mip(x : MachineCSR)
14492 write'MCSR(MachineCSR_mip_rupd(x,mip_STIP_rupd(x0,true)))
14499 ; if not((#mtohost((MCSR ()) : MachineCSR)) = (BitsN.B(0x0,64)))
14510 write'MCSR(MachineCSR_mtohost_rupd(x,BitsN.B(0x0,64)))
14522 ( log := ((1,log_instruction(BitsN.B(0x0,32),inst)) :: (!log))
14583 val x0 = #mcpuid(x : MachineCSR)
14586 (MachineCSR_mcpuid_rupd(x,mcpuid_ArchBase_rupd(x0,archBase arch)))
14590 val x0 = #mcpuid(x : MachineCSR)
14592 write'MCSR(MachineCSR_mcpuid_rupd(x,mcpuid_U_rupd(x0,true)))
14596 val x0 = #mcpuid(x : MachineCSR)
14598 write'MCSR(MachineCSR_mcpuid_rupd(x,mcpuid_S_rupd(x0,true)))
14602 val x0 = #mcpuid(x : MachineCSR)
14604 write'MCSR(MachineCSR_mcpuid_rupd(x,mcpuid_M_rupd(x0,true)))
14608 val x0 = #mcpuid(x : MachineCSR)
14610 write'MCSR(MachineCSR_mcpuid_rupd(x,mcpuid_I_rupd(x0,true)))
14614 val x0 = #mimpid(x : MachineCSR)
14618 (x,mimpid_RVSource_rupd(x0,BitsN.B(0x8000,16))))
14622 val x0 = #mimpid(x : MachineCSR)
14625 (MachineCSR_mimpid_rupd(x,mimpid_RVImpl_rupd(x0,BitsN.B(0x0,48))))
14632 val x0 = #mstatus(x : MachineCSR)
14635 (MachineCSR_mstatus_rupd(x,mstatus_VM_rupd(x0,vmMode Mbare)))
14639 val x0 = #mstatus(x : MachineCSR)
14643 (x,mstatus_MPRV_rupd(x0,privLevel Machine)))
14647 val x0 = #mstatus(x : MachineCSR)
14649 write'MCSR(MachineCSR_mstatus_rupd(x,mstatus_MIE_rupd(x0,false)))
14653 val x0 = #mstatus(x : MachineCSR)
14657 (x,mstatus_MFS_rupd(x0,ext_status Initial)))
14661 val x0 = #mstatus(x : MachineCSR)
14664 (MachineCSR_mstatus_rupd(x,mstatus_MXS_rupd(x0,ext_status Off)))
14668 val x0 = #mstatus(x : MachineCSR)
14670 write'MCSR(MachineCSR_mstatus_rupd(x,mstatus_MSD_rupd(x0,false)))
14692 write'gpr(BitsN.B(0x0,64),x)
14700 write'fpr(BitsN.B(0x0,64),x)