Remove N extension flag

Remove remaining references to the N extension that were leftover from riscv#584.
Timmmm · Nov 29, 2024 · e3e79d2 · e3e79d2
1 parent 3911cb7
commit e3e79d2
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 11 deletions.
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
@@ -149,10 +149,6 @@ val sys_enable_rvc : unit -> bool
 let sys_enable_rvc () = true
 declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
 
-val sys_enable_next : unit -> bool
-let sys_enable_next () = true
-declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
-
 val sys_enable_fdext : unit -> bool
 let sys_enable_fdext () = true
 declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`

diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v
@@ -198,7 +198,6 @@ Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
 Axiom sys_enable_writable_misa : unit -> bool.
 Axiom sys_enable_rvc : unit -> bool.
 Axiom sys_enable_fdext : unit -> bool.
-Axiom sys_enable_next : unit -> bool.
 Axiom sys_enable_zfinx : unit -> bool.
 Axiom sys_enable_writable_fiom : unit -> bool.
 

diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
@@ -149,10 +149,6 @@ val sys_enable_zfinx : unit -> bool
 let sys_enable_zfinx () = false
 declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
 
-val sys_enable_next : unit -> bool
-let sys_enable_next () = true
-declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
-
 val sys_enable_writable_fiom : unit -> bool
 let sys_enable_writable_fiom () = true
 declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
@@ -90,8 +90,6 @@ val sys_enable_svinval = pure "sys_enable_svinval" : unit -> bool
 val sys_enable_zcb = pure "sys_enable_zcb" : unit -> bool
 /* whether zfinx was enabled at boot */
 val sys_enable_zfinx = pure "sys_enable_zfinx" : unit -> bool
-/* whether the N extension was enabled at boot */
-val sys_enable_next = pure "sys_enable_next" : unit -> bool
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
    supervisor mode is implemented and non-bare addressing modes are supported. */
 val sys_enable_writable_fiom = pure "sys_enable_writable_fiom" : unit -> bool