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
|
Code Style
==========
This document is an incomplete description of the predominant style used in the
RISC-V Sail model.
Where something is not specified, please look for existing code similar to what
is being added and copy the predominant style.
For C and OCaml, the formatting rules should be followed where applicable.
For other languages, follow the standard style for that language if it exists;
for example, Python should follow the standard PEP-8 style.
Formatting
----------
* Block-level indentation uses two spaces
* Tabs should not be used
* There should be no trailing spaces on any lines
* All files should end with a newline character
* Unix-style line endings should be used
* Files should be free from leading, trailing and double blank lines
* There should be one space either side of operators such as `=` and `+`
* There should be no spaces before and one space after `,`
* There should be one space after control flow keywords such as `if`, `foreach`
and `match`
* There should be no spaces between a function name and its arguments, for both
definitions (valspecs, function definitions and function clauses) and calls,
nor should there be any spaces immediately within the parentheses
* There should be no spaces between a vector and the opening square bracket for
indexing or slicing, nor should there be any spaces immediately within the
square brackets
* For large blocks of code with repetitive structure where it improves
readability, additional whitespace may be inserted to align corresponding
elements horizontally with each other, within reason
* Avoid unnecessary parentheses and curly braces unless doing so seriously
hurts readability
* When modifying existing code that does not conform to this style, prefer
matching the existing style
* Files should have suitable copyright headers.
Implementation
--------------
* Since this is the official model intended to be included as part of the
RISC-V specifications, readability is paramount, including to those not
already familiar with the details of that field of Computer Science (e.g.
floating-point or cryptography)
* All instructions should be built as part of both the RV32 and RV64 models so
as to provide a path to supporting mutable MXL/SXL/UXL; if necessary,
constructs like `assert(sizeof(xlen) == 32)` at the start of the body can be
used to suppress any type errors that arise as a result
* Avoid the use of hard-coded constants like 32 even if the instruction is
RV32-specific, instead favouring `sizeof(xlen)` or a computed constant to
more clearly express the underlying intent
* Local variables should be made immutable whenever possible, but short
imperative loops with a small amount of local mutable state are preferred
over less-readable functional-style recursive equivalents
* Choose carefully between integer and bitvector types, and avoid multiple
round-trips between the two; for example, if counting something, use a `nat`
and convert it to an appropriately-sized bitvector at the point it is stored
in a register, but keep register source values as bitvectors until they are
needed to be interpreted as integers (see the implementation of `MUL` as an
example)
* Prefer `bool` over `bits(1)` when a value logically represents true or false
rather than being a single bit with a numeric meaning, and vice-versa
* Do not use strings for anything that is not text
* No new compile-time warnings from the Sail compiler should be introduced
(this does not include C or OCaml warnings for the code generated by the Sail
compiler)
* Do not use the `ext*` types and hooks for standard extensions unless
providing a stub implementation; these are reserved for use by out-of-tree
extensions that provide their own non-stub implementations
|
