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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148

// =======================================================================================
// This Sail RISC-V architecture model, comprising all files and
// directories except where otherwise noted is subject the BSD
// two-clause license in the LICENSE file.
//
// SPDX-License-Identifier: BSD-2-Clause
// =======================================================================================

// These functions define the primitives for physical memory access.
// They depend on the XLEN of the architecture.
//
// They also depend on the type of metadata that is read and written
// to physical memory.  For models that do not require this metadata,
// a unit type can be used.

$include <concurrency_interface.sail>

enum write_kind = {
  Write_plain,
  Write_RISCV_release,
  Write_RISCV_strong_release,
  Write_RISCV_conditional,
  Write_RISCV_conditional_release,
  Write_RISCV_conditional_strong_release,
}

enum read_kind = {
  Read_plain,
  Read_ifetch,
  Read_RISCV_acquire,
  Read_RISCV_strong_acquire,
  Read_RISCV_reserved,
  Read_RISCV_reserved_acquire,
  Read_RISCV_reserved_strong_acquire,
}

enum barrier_kind = {
  Barrier_RISCV_rw_rw,
  Barrier_RISCV_r_rw,
  Barrier_RISCV_r_r,
  Barrier_RISCV_rw_w,
  Barrier_RISCV_w_w,
  Barrier_RISCV_w_rw,
  Barrier_RISCV_rw_r,
  Barrier_RISCV_r_w,
  Barrier_RISCV_w_r,
  Barrier_RISCV_tso,
  Barrier_RISCV_i,
}

// Most of the above read/write_kinds are understood natively by the
// Sail concurrency interface, except for the strong acquire release
// variants which require an architecture specific access kind.
struct RISCV_strong_access = {
  variety : Access_variety,
}

// The Sail concurrency interface lets us have a physical address type
// with additional information, provided we can supply a function that
// converts it into a bitvector. When in RV32 mode, physaddrbits is
// bits(34), which needs to be zero-extended to bits(64) for
// sail_mem_write/read interface. This conversion is necessary because
// the memory interface only supports 32-bit or 64-bit physical
// addresses regardless of the actual physical address width.
val physaddrbits_zero_extend : physaddrbits -> bits(64)

function physaddrbits_zero_extend xs = zero_extend(xs)

instantiation sail_mem_write with
  'pa = physaddrbits,
  pa_bits = physaddrbits_zero_extend,
  // We don't have a relaxed-memory translation model for RISC-V, so
  // we just use unit as a dummy type.
  'translation_summary = unit,
  'arch_ak = RISCV_strong_access,
  // Similarly to translation_summary, we don't have a defined type for external
  // aborts, so just use unit here too
  'abort = unit

val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> bool

function write_ram(wk, Physaddr(addr), width, data, meta) = {
  let request : Mem_write_request('n, 64, physaddrbits, unit, RISCV_strong_access) = struct {
    access_kind = match wk {
      Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }),
      Write_RISCV_release => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }),
      Write_RISCV_strong_release => AK_arch(struct { variety = AV_plain }),
      Write_RISCV_conditional => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }),
      Write_RISCV_conditional_release => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }),
      Write_RISCV_conditional_strong_release => AK_arch(struct { variety = AV_exclusive }),
    },
    va = None(),
    pa = addr,
    translation = (),
    size = width,
    value = Some(data),
    tag = None(),
  };
  // Write out metadata only if the value write succeeds.
  // It is assumed for now that this write always succeeds;
  // there is currently no return value.
  // FIXME: We should convert the external API for all backends
  // (not just for Lem) to consume the value along with the
  // metadata to ensure atomicity.
  match sail_mem_write(request) {
    Ok(_) => {
      __WriteRAM_Meta(addr, width, meta);
      true
    },
    Err() => false,
  }
}

val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n)) -> unit
function write_ram_ea(wk, Physaddr(addr), width) = ()

instantiation sail_mem_read with
  pa_bits = physaddrbits_zero_extend

val read_ram : forall 'n, 0 < 'n <= max_mem_access.  (read_kind, physaddr, int('n), bool) -> (bits(8 * 'n), mem_meta)
function read_ram(rk, Physaddr(addr), width, read_meta) = {
  let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta;
  let request : Mem_read_request('n, 64, physaddrbits, unit, RISCV_strong_access) = struct {
    access_kind = match rk {
      Read_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }),
      Read_ifetch => AK_ifetch(),
      Read_RISCV_acquire => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }),
      Read_RISCV_strong_acquire => AK_arch(struct { variety = AV_plain }),
      Read_RISCV_reserved => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }),
      Read_RISCV_reserved_acquire => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }),
      Read_RISCV_reserved_strong_acquire => AK_arch(struct { variety = AV_exclusive }),
    },
    va = None(),
    pa = addr,
    translation = (),
    size = width,
    tag = false,
  };
  match sail_mem_read(request) {
    Ok((value, _)) => (value, meta),
    Err() => exit(),
  }
}

instantiation sail_barrier with 'barrier = barrier_kind

val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
val __TraceMemoryRead  : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit