riscv/model/riscvScript.sml

583 val rec'mcpuid_def = Def
584   ("rec'mcpuid",Var("x",F64),
612 val write'rec'mcpuid_def = Def
613   ("write'rec'mcpuid",TP[AVar F64,Var("x",CTy"mcpuid")],
618    Call("rec'mcpuid",CTy"mcpuid",Var("x",F64)))
620 val rec'mimpid_def = Def
621   ("rec'mimpid",Var("x",F64),
632 val write'rec'mimpid_def = Def
633   ("write'rec'mimpid",TP[AVar F64,Var("x",CTy"mimpid")],
638    Call("rec'mimpid",CTy"mimpid",Var("x",F64)))
640 val rec'mstatus_def = Def
641   ("rec'mstatus",Var("x",F64),
668 val write'rec'mstatus_def = Def
669   ("write'rec'mstatus",TP[AVar F64,Var("x",CTy"mstatus")],
674    Call("rec'mstatus",CTy"mstatus",Var("x",F64)))
676 val rec'mtdeleg_def = Def
677   ("rec'mtdeleg",Var("x",F64),
688 val write'rec'mtdeleg_def = Def
689   ("write'rec'mtdeleg",TP[AVar F64,Var("x",CTy"mtdeleg")],
694    Call("rec'mtdeleg",CTy"mtdeleg",Var("x",F64)))
696 val rec'mip_def = Def
697   ("rec'mip",Var("x",F64),
719 val write'rec'mip_def = Def
720   ("write'rec'mip",TP[AVar F64,Var("x",CTy"mip")],
725    Call("rec'mip",CTy"mip",Var("x",F64)))
727 val rec'mie_def = Def
728   ("rec'mie",Var("x",F64),
750 val write'rec'mie_def = Def
751   ("write'rec'mie",TP[AVar F64,Var("x",CTy"mie")],
756    Call("rec'mie",CTy"mie",Var("x",F64)))
758 val rec'mcause_def = Def
759   ("rec'mcause",Var("x",F64),
770 val write'rec'mcause_def = Def
771   ("write'rec'mcause",TP[AVar F64,Var("x",CTy"mcause")],
776    Call("rec'mcause",CTy"mcause",Var("x",F64)))
778 val rec'sstatus_def = Def
779   ("rec'sstatus",Var("x",F64),
803 val write'rec'sstatus_def = Def
804   ("write'rec'sstatus",TP[AVar F64,Var("x",CTy"sstatus")],
809    Call("rec'sstatus",CTy"sstatus",Var("x",F64)))
811 val rec'sip_def = Def
812   ("rec'sip",Var("x",F64),
828 val write'rec'sip_def = Def
829   ("write'rec'sip",TP[AVar F64,Var("x",CTy"sip")],
834    Call("rec'sip",CTy"sip",Var("x",F64)))
836 val rec'sie_def = Def
837   ("rec'sie",Var("x",F64),
853 val write'rec'sie_def = Def
854   ("write'rec'sie",TP[AVar F64,Var("x",CTy"sie")],
859    Call("rec'sie",CTy"sie",Var("x",F64)))
861 val rec'FPCSR_def = Def
862   ("rec'FPCSR",Var("x",F32),
879 val write'rec'FPCSR_def = Def
880   ("write'rec'FPCSR",TP[AVar F32,Var("x",CTy"FPCSR")],
885    Call("rec'FPCSR",CTy"FPCSR",Var("x",F32)))
893             TP[Call("rec'sip",CTy"sip",LW(0,64)),
903             TP[Call("rec'sie",CTy"sie",LW(0,64)),
1012                                                ("rec'sstatus",
1061                                                ("rec'mstatus",
2539                                   ("rec'sstatus",CTy"sstatus",
2577                              TP[Call("rec'sie",CTy"sie",Var("value",F64)),
2663                              TP[Call("rec'sip",CTy"sip",Var("value",F64)),
2853                                   ("rec'mstatus",CTy"mstatus",
2883                             ("rec'mtdeleg",CTy"mtdeleg",Var("value",F64))]))])),
2897                           Call("rec'mie",CTy"mie",Var("value",F64))]))])),
3012                           Call("rec'mcause",CTy"mcause",Var("value",F64))]))])),
3040                           Call("rec'mip",CTy"mip",Var("value",F64))]))])),
4631 val rec'SV_PTE_def = Def
4632   ("rec'SV_PTE",Var("x",F64),
4651 val write'rec'SV_PTE_def = Def
4652   ("write'rec'SV_PTE",TP[AVar F64,Var("x",CTy"SV_PTE")],
4657    Call("rec'SV_PTE",CTy"SV_PTE",Var("x",F64)))
4659 val rec'SV_Vaddr_def = Def
4660   ("rec'SV_Vaddr",Var("x",F64),
4675 val write'rec'SV_Vaddr_def = Def
4676   ("write'rec'SV_Vaddr",TP[AVar F64,Var("x",CTy"SV_Vaddr")],
4681    Call("rec'SV_Vaddr",CTy"SV_Vaddr",Var("x",F64)))
4690           Call("rec'SV_Vaddr",CTy"SV_Vaddr",Var("vAddr",F64)),
4705                     ("rec'SV_PTE",CTy"SV_PTE",