| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
This implements a lot of missing functionality for PMPs.
* Support 64 PMPs as well as 0 and 16.
* Support setting PMP grain
* Return correct address bits on read (some read as 0 or 1 depending on the grain and match type)
* Unlock PMPs on reset
* Implement pmpcfg WARL legalisation
Co-authored-by: Ben Fletcher <benjamin.fletcher@codasip.com>
|
|
And string_of_bits to bits_str. These are the names that Sail uses so it makes sense to use them.
|
|
This change includes `generic_equality.sail` and `mapping.sail` from the Sail standard library which defines a lot of things that were defined in `prelude.sail`.
I also removed `reg_deref` which is no longer required.
The `mapping.sail` and `hex_bits.sail` files are in Sail 0.18 which is not yet released, so they have been temporarily copied here.
|
|
Bitfields allow [<bitfield> with field = value], like bitvectors,
so use that instead of the old-style `update_field` overloads.
|
|
Use newer bitfield syntax, which has been part of Sail for
a while now. Should in theory be more efficient as it removes
a level of indirection for bitfield accesses.
It's also much more friendly to `sail -fmt`, which has no idea
how to handle the old bitfield syntax.
|
|
Switch to bitlist representation because the machine words
can't handle the vector code currently
Remove RMEM target from default set of targets in Makefile.
This is only interesting for RMEM maintainers. There's no reason for it
to be generated by default, and it's also broken.
While we are hacking on these files purge the duplicate versions for Sail 0.11+
|
|
class is a reserved keyword in lem, so the use of class as a variable
name was causing issues. While ultimately this should be fixed in Sail
this can easily be worked around here.
Fortunately the code in questions was ultimately using a pattern like
let class = f(x);
let y = match class {
...
};
y
which can be simplified to
match f(x) {
...
}
removing the variable entirely, and making the code simpler so a
win-win overall!
|
|
Add a line to CODE_STYLE.md saying that tabs should not be used
Signed-off-by: Alasdair Armstrong <alasdair.armstrong@cl.cam.ac.uk>
|
|
Use fixed-length vectors for AES tables
Note that because we have `default Order dec`, Sail vectors
are indexed the same as bitvectors, in decreasing order, hence why
the indexing in sbox_lookup becomes
```
table[255 - unsigned(x)]
```
rather than
```
table[unsigned(x)]
```
The alternative would be to flip all the literals
|
|
This removes the warning about `opam config var`. Setting OPAMCLI in
this way is the correct thing to do if we want to continue supporting
opam 2.0.
If we decide to require opam 2.1+ then all `opam var` invocations should
become `opam --cli=2.1 var`, as per the opam CLI versioning spec:
https://github.com/ocaml/opam/wiki/Spec-for-opam-CLI-versioning
|
|
|
|
There are a few places where operand/field names are not consistent
across scattered definitions for an instruction.
Here, parameter `rs2` is used for encode/decode and execute, but
`rd` is used for the same purpose in the assembly clause:
```
mapping clause encdec_compressed = C_SWSP(ui76 @ ui52, rs2)
<-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
function clause execute (C_SWSP(uimm, rs2)) = {
let imm : bits(12) = zero_extend(uimm @ 0b00);
execute(STORE(imm, rs2, sp, WORD, false, false))
}
mapping clause assembly = C_SWSP(uimm, rd)
<-> "c.swsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm)
```
Fix these by using the operand names found in
"The RISC-V Instruction Set Manual, Volume I: Unprivileged ISA",
document version 20191213, and "RISC-V Cryptography Extensions
Volumn I: Scalar & Entropy Source Instructions", version v1.0.1.
|
|
The operand order for Store-Conditional assembly has the second
and third operands reversed.
The RISC-V Instruction Set Manual states:
> ```
> SC.W conditionally writes a word in rs2 to the address in rs1 [...]
> If the SC.W succeeds, the instruction writes the word in rs2 to memory,
> and it writes zero to rd. If the SC.W fails, the instruction does not
> write to memory, and it writes a nonzero value to rd.
> ```
`rd` is for the return code, `rs2` is the value, and `rs1` is the memory
address.
For the syntax `sc.w A,B,(C)`:
- `A` is where the result is stored, per convention. So, this is `rd`.
- `B` is the value to be stored. So, this is `rs2`.
- `C` is the address at which to store the value. So, this is `rs1`.
The resulting syntax would be `stc.w rd,rs2,(rs1)`.
The current assembly representation is:
```
"sc." ^ size_mnemonic(size) [...] reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
```
Note that the order is wrong. In addition, parentheses are missing around `rs2`.
Fix this instance, as well as two other instances where parentheses are missing.
Fixes #338.
Fixes #344.
Suggested-by: Tim Hutt <timothy.hutt@codasip.com>
|
|
Update the versions of some of the Github actions, as some of the older
action versions used parts of the github API that are deprecated and
due to be removed.
|
|
The issue shows that the encoding and assembly definitions of vsetvl and vsetvli are incorrectly mixed together,
but they actually differ a lot and therefore cannot have a unified definition as the old implementation did,
so this section has been rewritten to split their definitions and executions.
And because these instructions have similar functional behavior after the decoding stage,
some common code is further extracted to be helper functions in this commit.
|
|
Fixes a warning introduced by commit 5725f3f
|
|
In `model/riscv_insts_zfa.sail`, there are quite a few cases where
spaces (`spc()`) are utilized instead of separators (`sep()`) between operands:
```
mapping clause assembly = RISCV_FMAXM_D(rs2, rs1, rd)
<-> "fmaxm.d" ^ spc() ^ freg_name(rd)
^ spc() ^ freg_name(rs1)
^ spc() ^ freg_name(rs2)
```
In the assembly representation, spaces are between the mnemonic and
its operands, and separators are between operands.
Fix the errant cases.
Signed-off-by: Paul A. Clarke <pclarke@ventanamicro.com>
|
|
SHIFTW and SHIFTIWOP were duplicated. This did not cause any harm except that the disassembly for the SHIFTW version was incorrect. Therefore I removed that version.
The `execute()` functions were identical but the SHIFTW version is slightly neater (only one `[31..0]`) so I applied that to the SHIFTIWOP version.
This should cause no functional changes to the model except that the disassembly will have the extra `w` which is correct.
|
|
Instead of keeping a mirror register in sync with fflags, just return the new flags.
|
|
This PR adds the following:
General Framework and Configurations:
* Introduced the V extension's general framework and configuration setting instructions.
* Updated model/riscv_insts_vext_vset.sail and effect matching functions in riscv_vlen.sail.
* Addressed code formatting issues and made revisions post the Nov 22 meeting.
* Co-authored by Nicolas Brunie and Jessica Clarke.
Vector Load/Store Instructions:
* Integrated vector load and store instructions.
* Enhanced the implementation of SEW, LMUL, VLEN and removed real numbers from the code.
* Updated vstart settings and removed unnecessary assert statements.
* Rectified bugs in vleff instructions and overhauled coding styles.
* Incorporated guards for vector encdec clauses and optimized memory access post vector load/store failures.
Vector Integer/Fixed-Point Instructions:
* Added vector integer/fixed-point arithmetic and mask instructions.
* Improved vector EEW and EMUL checking functions and introduced illegal instruction check functions.
* Fine-tuned code formatting for vector instruction checks.
Vector Floating-Point Instructions:
* Rolled out vector floating-point instructions and updated their conversion counterparts.
* Refreshed copyright headers specific to the vector extension code.
Vector Reduction and Mask Instructions:
* Integrated vector mask and reduction instructions.
* Addressed register overlap checks for vector mask instructions.
Miscellaneous Enhancements and Fixes:
* Updated vector CSR vtype.vill settings and judgements.
* Systematized patterns for vector illegal instruction checks.
* Rectified issues in vector load/store and reduction operations.
* Purged redundant elements from the V extension code and vector floating-point functions.
* Cleaned up softfloat makefiles and renamed EXTZ and EXTS within the V extension code.
* Addressed a clang-format check issue and NaN boxing anomalies. Provided annotations for pending RVV configurations.
* Initialized default VLEN value and set vlenb CSR.
* Set constraints for vector variable initialization and added mstatus.VS settings specific to the vector extension.
|
|
This is a much clearer name because the option allows code to enable FIOM, it doesn't enable FIOM itself.
|
|
This implements the m/senvcfg(h) CSRs. This CSR is used to enable/disable extensions and behaviours for lower privilege modes. Currently the only implemented bit is FIOM which affects how fences work.
It also affects how atomic memory accesses work in non-cacheable regions, but the model does not currently support PMAs so that can't easily be implemented.
|
|
The speculate_conditional should be marked monadic. It would seem like
the various _reservation functions should be also, but it seems like
perhaps they are not implemented in lem right now.
|
|
Likely a cut-and-paste error, the definition for fmaxm.d uses the fmaxm.s
mnemonic, which is already used earlier in the same file.
|
|
both should be disabled if F=0
|
|
This makes it easier to use a separate M-mode bootloader and kernel
payload (e.g. OpenSBI fw_jump). It also makes it easier to test booting
systems such as FreeBSD without bundling the kernel with the bootloader.
|
|
This makes it possible for a follow-up commit to add logic that allows
loading more than one ELF file (e.g. M-mode firmware and S-mode kernel).
|
|
In some cases we were reporting the translated value instead, but the
privileged spec text requires the virtual address:
```
If mtval is written with a nonzero value when a breakpoint,
address-misaligned, access-fault, or page-fault exception occurs on an
instruction fetch, load, or store, then mtval will contain the faulting
virtual address.
```
|
|
Since Sail 0.15 (released Nov 2022), effects have had no effect. They now generate a deprecation warning. This commit removes all the effect annotations from the model, thus fixing the compiler warnings.
|
|
|
|
These are given on the previous line already. Sail does not let you change the type of a variable like Rust does. The `var` ensures this definitely refers to a local rather than global variable.
|
|
|
|
This file seems to be created on every build.
|
|
|
|
This is already provided by Sail.
|
|
|
|
These empty lines don't add to the readability of the trace and in fact
when trace redirection is enabled they result in lots of empty lines being
printed to stderr which makes it impossible to read the OS boot messages.
|
|
Previously --help printed the following:
```
-V --no-trace
-� --trace-output
-l --inst-limit
```
With the new change it is:
```
-V --no-trace
--trace-output
-l --inst-limit
```
|
|
This is useful when booting an operating system with tracing enabled
as it allows showing the printed messages on the terminal and storing
the trace log to a separate file. All categorized trace messages are
now redirected to the --trace-output file when passed. If this option is
not gived, the current behaviour of using stdout is retained.
Example usage:
`./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb --trace-output /dev/stderr os-boot/linux-rv64-64mb.bbl --trace-output /tmp/linux.log`
|
|
Rename EXTZ to zero_extend and EXTS to sign_extend. Two main reasons
for doing this - it means that the source more closely follows the
descriptions in the documentation with more readable names, and EXTS
and EXTZ are visually very close to each other with just the S and Z.
They are also following an odd convention where they are ALLCAPS rather
than snake_case like other functions in the spec.
I think this convention comes from early Power specs in Sail, which
influenced Sail MIPS and CHERI-MIPS, but I don't think it's a very
good convention we should be keeping in sail-riscv
|
|
Allows for (e.g.) BSD sed, which uses -i differently.
|
|
|
|
This formats the code with clang-format 15 since the pre-commit hook for
clang-format 16 would require a newer version of pre-commit.
|
|
The template that I used when adding it uses hooks from 2020. Update this
to the latest version and add a minimum pre-commit version check to ensure
we get sensible error messages rather than obscure failures.
The minimum chosen here is 2.10 as that is the version shipping with
Debian 11 and most other distributions have newer versions. If needed
a newer version can always be installed using pip.
|
|
Do this before installing sail or building the model to avoid wasting CI
time if these basic checks are failing.
|
|
This strips trailing whitespace and fixes line endings. I had to add the
*.dump files to the exclude list to avoid excessive changes, but
ideally these would not be part of the repository since they can just be
generated by running objdump manually.
|
|
Recommend installation of this basic pre-commit hook that ensures that
all files are free of trailing whitespace and have a final newline.
It also checks that no large files are added and that YAML files are valid.
|
|
* Add a clang-format configuration and reformat C code
From my testing it turns out the built-in WebKit style is the closest to
the current style. I added a few config options to further reduce the
diff and I think the current output looks reasonable.
In the future it would be good to add a CI and pre-commit check to enforce
that all C code is consistently formatted to reduce the need for reviewers
to look for formatting issues.
* Fix formatting of commented-out reservation debug code
Use an empty-by-default macro instead of commented-out fprintf calls.
This way clang-format can format the calls sensibly and it's easier
to enable the debug prints.
* Improve formatting of fprintf call in set_config_print()
Clang-format does not like long string literals, so split this manually
to format the call sensibly.
* Fix formatting of function pointer typedef
Clang-format gets this wrong `*` is part of the typedef.
* Improve formatting of getopt_long call
* Fix odd fprintf continuation by splitting long string literal
|
|
Apparently this needs stating and isn't obvious.
Signed-off-by: Jessica Clarke <jrtc27@jrtc27.com>
|
|
|
