From e3e79d2b78bff398648d93ce4f211923140e7a66 Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Fri, 29 Nov 2024 03:22:39 -0800 Subject: [PATCH] Remove N extension flag Remove remaining references to the N extension that were leftover from #584. --- handwritten_support/riscv_extras.lem | 4 ---- handwritten_support/riscv_extras.v | 1 - handwritten_support/riscv_extras_sequential.lem | 4 ---- model/riscv_sys_regs.sail | 2 -- 4 files changed, 11 deletions(-) diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 245a7fe80..41d054294 100644 --- 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 index b17f75343..994f3ce5a 100644 --- 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 index 5ffe482cd..c8ee8a20c 100644 --- 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 index eec299b80..dca1c1b41 100644 --- 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