Changed CSR addresses and names in the RISC-V L3 model to agree with …

…the latest version of the ISA manual
kth-step · Dec 5, 2024 · 9cc7ffb · 9cc7ffb
1 parent caf07c3
commit 9cc7ffb
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 23 deletions.
diff --git a/src/shared/l3-machine-code/riscv/model/riscvLib.sig b/src/shared/l3-machine-code/riscv/model/riscvLib.sig
@@ -1,4 +1,4 @@
-(* riscvLib - generated by L3 - Mon Jun 01 11:52:39 2020 *)
+(* riscvLib - generated by L3 - Thu Dec 05 14:01:53 2024 *)
 signature riscvLib =
 sig
    val riscv_compset: Thm.thm list -> computeLib.compset

diff --git a/src/shared/l3-machine-code/riscv/model/riscvLib.sml b/src/shared/l3-machine-code/riscv/model/riscvLib.sml
@@ -1,4 +1,4 @@
-(* riscvLib - generated by L3 - Mon Jun 01 11:52:39 2020 *)
+(* riscvLib - generated by L3 - Thu Dec 05 14:01:53 2024 *)
 structure riscvLib :> riscvLib =
 struct
 open HolKernel boolLib bossLib

diff --git a/src/shared/l3-machine-code/riscv/model/riscvScript.sml b/src/shared/l3-machine-code/riscv/model/riscvScript.sml
@@ -1,4 +1,4 @@
-(* riscvScript.sml - generated by L3 - Mon Jun 01 11:52:39 2020 *)
+(* riscvScript.sml - generated by L3 - Thu Dec 05 14:01:53 2024 *)
 open HolKernel boolLib bossLib Import
 
 val () = Import.start "riscv"
@@ -63,18 +63,19 @@ val _ = Record ("mcause",[("EC",F4),("Int",bTy),("mcause'rst",FTy 59)])
 ;
 val _ = Record
   ("MachineCSR",
-   [("mbadaddr",F64),("mbase",F64),("mbound",F64),("mcause",CTy"mcause"),
+   [("mbase",F64),("mbound",F64),("mcause",CTy"mcause"),
     ("mcpuid",CTy"mcpuid"),("mdbase",F64),("mdbound",F64),("mepc",F64),
     ("mfromhost",F64),("mhartid",F64),("mibase",F64),("mibound",F64),
     ("mie",CTy"mie"),("mimpid",CTy"mimpid"),("mip",CTy"mip"),
     ("mscratch",F64),("mstatus",CTy"mstatus"),("mtdeleg",CTy"mtdeleg"),
-    ("mtime_delta",F64),("mtimecmp",F64),("mtohost",F64),("mtvec",F64)])
+    ("mtime_delta",F64),("mtimecmp",F64),("mtohost",F64),("mtval",F64),
+    ("mtvec",F64)])
 ;
 val _ = Record
   ("HypervisorCSR",
-   [("hbadaddr",F64),("hcause",CTy"mcause"),("hepc",F64),("hscratch",F64),
+   [("hcause",CTy"mcause"),("hepc",F64),("hscratch",F64),
     ("hstatus",CTy"mstatus"),("htdeleg",CTy"mtdeleg"),("htime_delta",F64),
-    ("htimecmp",F64),("htvec",F64)])
+    ("htimecmp",F64),("htval",F64),("htvec",F64)])
 ;
 val _ = Record
   ("sstatus",
@@ -87,8 +88,8 @@ val _ = Record ("sie",[("SSIE",bTy),("STIE",bTy),("sie'rst",FTy 62)])
 ;
 val _ = Record
   ("SupervisorCSR",
-   [("sasid",F64),("sbadaddr",F64),("scause",CTy"mcause"),("sepc",F64),
-    ("sptbr",F64),("sscratch",F64),("stime_delta",F64),("stimecmp",F64),
+   [("sasid",F64),("scause",CTy"mcause"),("sepc",F64),("sptbr",F64),
+    ("sscratch",F64),("stime_delta",F64),("stimecmp",F64),("stval",F64),
     ("stvec",F64)])
 ;
 val _ = Record
@@ -1717,7 +1718,7 @@ val is_CSR_defined_def = Def
                                             LW(3840,12)),
                                         Bop(Le,Var("csr",FTy 12),
                                             LW(3841,12))),TP[LT,qVar"s"]),
-                                   (EQ(Var("csr",FTy 12),LW(3856,12)),
+                                   (EQ(Var("csr",FTy 12),LW(3860,12)),
                                     TP[LT,qVar"s"]),
                                    (Bop(And,
                                         Bop(Ge,Var("csr",FTy 12),
@@ -1960,7 +1961,7 @@ val CSRMap_def = Def
                        Dest("procID",F8,qVar"state")))),qVar"state"]),
           (LW(3395,12),
            TP[Dest
-                ("sbadaddr",F64,
+                ("stval",F64,
                  Apply
                    (Dest("c_SCSR",ATy(F8,CTy"SupervisorCSR"),qVar"state"),
                     Dest("procID",F8,qVar"state"))),qVar"state"]),
@@ -2125,7 +2126,7 @@ val CSRMap_def = Def
                        Dest("procID",F8,qVar"state")))),qVar"state"]),
           (LW(579,12),
            TP[Dest
-                ("hbadaddr",F64,
+                ("htval",F64,
                  Apply
                    (Dest("c_HCSR",ATy(F8,CTy"HypervisorCSR"),qVar"state"),
                     Dest("procID",F8,qVar"state"))),qVar"state"]),
@@ -2164,7 +2165,7 @@ val CSRMap_def = Def
                     Apply
                       (Dest("c_MCSR",ATy(F8,CTy"MachineCSR"),qVar"state"),
                        Dest("procID",F8,qVar"state")))),qVar"state"]),
-          (LW(3856,12),
+          (LW(3860,12),
            TP[Dest
                 ("mhartid",F64,
                  Apply
@@ -2246,7 +2247,7 @@ val CSRMap_def = Def
                        Dest("procID",F8,qVar"state")))),qVar"state"]),
           (LW(835,12),
            TP[Dest
-                ("mbadaddr",F64,
+                ("mtval",F64,
                  Apply
                    (Dest("c_MCSR",ATy(F8,CTy"MachineCSR"),qVar"state"),
                     Dest("procID",F8,qVar"state"))),qVar"state"]),
@@ -3040,7 +3041,7 @@ val write'CSRMap_def = Def
                    (Dest("c_MCSR",ATy(F8,CTy"MachineCSR"),qVar"state"),
                     Dest("procID",F8,qVar"state"),
                     Rupd
-                      ("mbadaddr",
+                      ("mtval",
                        TP[Apply
                             (Dest
                                ("c_MCSR",ATy(F8,CTy"MachineCSR"),
@@ -3236,7 +3237,7 @@ val csrName_def = Def
        (LW(260,12),LS"sie"),(LW(289,12),LS"stimecmp"),
        (LW(3329,12),LS"stime"),(LW(3457,12),LS"stimeh"),
        (LW(320,12),LS"sscratch"),(LW(321,12),LS"sepc"),
-       (LW(3394,12),LS"scause"),(LW(3395,12),LS"sbadaddr"),
+       (LW(3394,12),LS"scause"),(LW(3395,12),LS"stval"),
        (LW(324,12),LS"mip"),(LW(384,12),LS"sptbr"),(LW(385,12),LS"sasid"),
        (LW(2304,12),LS"cycle"),(LW(2305,12),LS"time"),
        (LW(2306,12),LS"instret"),(LW(2432,12),LS"cycleh"),
@@ -3245,15 +3246,15 @@ val csrName_def = Def
        (LW(514,12),LS"htdeleg"),(LW(545,12),LS"htimecmp"),
        (LW(3585,12),LS"htime"),(LW(3713,12),LS"htimeh"),
        (LW(576,12),LS"hscratch"),(LW(577,12),LS"hepc"),
-       (LW(578,12),LS"hcause"),(LW(579,12),LS"hbadaddr"),
+       (LW(578,12),LS"hcause"),(LW(579,12),LS"htval"),
        (LW(2561,12),LS"stime"),(LW(2689,12),LS"stimeh"),
        (LW(3840,12),LS"mcpuid"),(LW(3841,12),LS"mimpid"),
-       (LW(3856,12),LS"mhartid"),(LW(768,12),LS"mstatus"),
+       (LW(3860,12),LS"mhartid"),(LW(768,12),LS"mstatus"),
        (LW(769,12),LS"mtvec"),(LW(770,12),LS"mtdeleg"),
        (LW(772,12),LS"mie"),(LW(801,12),LS"mtimecmp"),
        (LW(1793,12),LS"mtime"),(LW(1857,12),LS"mtimeh"),
        (LW(832,12),LS"mscratch"),(LW(833,12),LS"mepc"),
-       (LW(834,12),LS"mcause"),(LW(835,12),LS"mbadaddr"),
+       (LW(834,12),LS"mcause"),(LW(835,12),LS"mtval"),
        (LW(836,12),LS"mip"),(LW(896,12),LS"mbase"),
        (LW(897,12),LS"mbound"),(LW(898,12),LS"mibase"),
        (LW(899,12),LS"mibound"),(LW(900,12),LS"mdbase"),
@@ -3932,7 +3933,7 @@ val takeTrap_def = Def
                                                         ("write'SCSR",
                                                          ATy(qTy,qTy),
                                                          Rupd
-                                                           ("sbadaddr",
+                                                           ("stval",
                                                             TP[Apply
                                                                  (Const
                                                                     ("SCSR",
@@ -4037,7 +4038,7 @@ val takeTrap_def = Def
                                                         ("write'MCSR",
                                                          ATy(qTy,qTy),
                                                          Rupd
-                                                           ("mbadaddr",
+                                                           ("mtval",
                                                             TP[Apply
                                                                  (Const
                                                                     ("MCSR",
@@ -10430,10 +10431,10 @@ val dfn'MRTS_def = Def
                  (Call
                     ("write'SCSR",ATy(qTy,qTy),
                      Rupd
-                       ("sbadaddr",
+                       ("stval",
                         TP[Var("v",CTy"SupervisorCSR"),
                            Dest
-                             ("mbadaddr",F64,
+                             ("mtval",F64,
                               Apply
                                 (Const("MCSR",ATy(qTy,CTy"MachineCSR")),
                                  qVar"s"))])),qVar"s"),