From 663e24a3d8f45b4b184b3a4bc3a57bc0f3d6cd78 Mon Sep 17 00:00:00 2001
From: Aditya Naik
Date: Fri, 27 Aug 2021 13:07:37 -0400
Subject: Initial; working SAIL RISC-V regs

The register definition along with read/write functions for registers
are lowered to Coq. The FIRRTL annotation does not work as expected.
---
 riscv_reg_type.sail | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 riscv_reg_type.sail

(limited to 'riscv_reg_type.sail')

diff --git a/riscv_reg_type.sail b/riscv_reg_type.sail
new file mode 100644
index 0000000..99fae3c
--- /dev/null
+++ b/riscv_reg_type.sail
@@ -0,0 +1,60 @@
+/* Content from riscv_xlen64.sail */
+default Order dec
+
+/* $include <smt.sail> */
+$include <option.sail>
+/* $include <arith.sail> */
+$include <string.sail>
+$include <vector_dec.sail>
+/* $include <regfp.sail> */
+
+type xlen       : Int = 64
+type xlen_bytes : Int = 8
+type xlenbits         = bits(xlen)
+
+/* Content from prelude.sail */
+
+val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+
+function EXTS(m, v) = sail_sign_extend(v, m)
+function EXTZ(m, v) = sail_zero_extend(v, m)
+
+val string_length = "string_length" : string -> nat
+val string_startswith = "string_startswith" : (string, string) -> bool
+val string_drop = "string_drop" : (string, nat) -> string
+val string_take = "string_take" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
+/* Content from riscv_reg_type.sail*/
+
+/* default register type */
+type regtype = xlenbits
+
+/* default zero register */
+let zero_reg : regtype = EXTZ(0x0)
+
+/* default register printer */
+/* val RegStr : regtype -> string */
+/* function RegStr(r) = BitStr(r) */
+
+/* conversions */
+
+val regval_from_reg : regtype -> xlenbits
+function regval_from_reg(r) = r
+
+val regval_into_reg : xlenbits -> regtype
+function regval_into_reg(v) = v
+
+/* register file indexing */
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+
+/* val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} */
+/* function regidx_to_regno b = let 'r = unsigned(b) in r */
+
+/* register identifiers */
+
+type regidx  = bits(5)
+type cregidx = bits(3)    /* identifiers in RVC instructions */
+type csreg   = bits(12)   /* CSR addressing */
\ No newline at end of file
-- 
cgit v1.2.3