1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
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 */
|
