- Jun 03, 2024
-
-
Tim Hutt authored
Instead of `word_width` which can only be up to 8 bytes, just use bytes. This allows larger accesses (the limit is increased to 4096), e.g. for `cbo.zero`.
-
Mudassir Ali authored
This uses the Make job server so that multiple threads can be used for LTO, which speeds up the build.
-
- May 23, 2024
-
-
Bill McSpadden authored
fix disassembly problems
-
Bill McSpadden authored
Remove duplicate type declarations for mem_read
-
Bill McSpadden authored
Minor style fixes
-
Bill McSpadden authored
csim: Fix C23 compatability warning
-
- May 22, 2024
-
-
Jordan Carlin authored
-
- May 21, 2024
-
-
Bill McSpadden authored
Remove unused (f)reg_name_abi functions
-
Alasdair authored
The plat_get_16_random_bits was missing its unit argument, which produces the following warning: ``` generated_definitions/c/riscv_model_RV64.c:28041:34: warning: passing arguments to 'plat_get_16_random_bits' without a prototype is deprecated in all versions of C and is not supported in C2x [-Wdeprecated-non-prototype] zseed = plat_get_16_random_bits(UNIT); ``` This commit adds the appropriate argument to the function in the C simulator
-
Jordan Carlin authored
-
- May 20, 2024
-
-
Bill McSpadden authored
RVWMO support via Sail concurrency interface
-
Bill McSpadden authored
Don't read or write 8 bytes for 4-byte PTEs
-
Bill McSpadden authored
Move haveAtomics() guard for atomic instructions to guard clauses
-
Bill McSpadden authored
Move haveMulDiv() guard to encdec for M extension
-
- May 19, 2024
-
-
Jordan Carlin authored
-
Jordan Carlin authored
-
- May 18, 2024
-
-
Jordan Carlin authored
-
Tim Hutt authored
Very minor. Uses an existing type alias.
-
- May 16, 2024
-
-
Bill McSpadden authored
Fix the encoding and assembly of `vsetvl` instruction
-
Bill McSpadden authored
-
Tim Hutt authored
Implicit `var` declarations will eventually be an error. This makes some implicit `var` declarations explicit.
-
Tim Hutt authored
These used to be different because they had different effects annotations, but those have since been removed and now they are the same.
-
Tim Hutt authored
The existing PMP code could not handle physical addresses above 32 bits on RV32, which are possible since Sv32 has 34-bit physical addresses, and the PMP registers are in units of 4 bytes, so they can encode 34-bit addresses. This fixes that by delaying the *4 until the comparison where it can be done using `nat` instead of `xlenbits` which it would overflow.
-
- May 15, 2024
- May 14, 2024
-
-
Tim Hutt authored
This matches the style of all the other instructions, which use the decoder mapping for this purpose.
-
KotorinMinami authored
-
- May 13, 2024
-
-
Alasdair authored
This instruction had a bit of a case of 'boolean blindness' code smell, where the mul operation was represented as a triple of booleans. This commit refactors the implemention to use a struct with named fields for high, signed_rs1, and signed_rs2. The C_MUL instruction in Zcb also needs to be changed appropriately The mul_op struct was added in riscv_types While there do some housekeeping w.r.t the comment about a workaround for Sail < 0.15.1, as this is no longer needed.
-
- May 11, 2024
-
-
Alasdair authored
These stub functions are required for building the Riscv.thy file from the generated lem file.
-
Alasdair authored
Furthermore, make sure variables defined by calling opam are created using :=, so opam is not called each time they are expanded
-
KotorinMinami authored
These immediates are sign extended and usually interpreted as signed, so it's less confusing to use signed numbers. This also matches SPIKE's disassembly.
-
- May 10, 2024
-
-
Alasdair Armstrong authored
In general we aren't requiring contributors to implement the correct Lem/Isabelle/HOL4/Coq stubs for new extensions (this would almost certainly be way too high a bar) so having these in the default set of build targets just means that typing 'make' is broken until those of us who are invested in maintaining those targets can add updates for those stubs.
-
Shivang Mishra authored
Updates the instruction mnemonics for vmandn and vmorn * replace mnemonics "vmandnot" and "vmornot" with "vmandn" and "vmorn" respectively * renamed MM_VMORNOT and MM_VMANDNOT to match mnemonics
-
- May 08, 2024
-
-
Tim Hutt authored
These guards were missing from one side of each clause.
-
Martin Berger authored
These changes add the "Svinval" Standard Extension for Fine-Grained Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model. This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL, SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA. HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the Hypervisor Extension which is yet to be included in the model. SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration of the coherency model (rmem) with sail. The specification says that SINVAL.VMA behaves just as SFENCE.VMA, except there are additional ordering constraints with respect to the new SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we can treat SINVAL.VMA as if it were SFENCE.VMA. Co-authored-by:Kristin Barber <kristinbarber@google.com>
-
Martin Berger authored
-
Martin Berger authored
-
Martin Berger authored
-
Martin Berger authored
These changes add the "Svinval" Standard Extension for Fine-Grained Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model. This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL, SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA. HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the Hypervisor Extension which is yet to be included in the model. SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration of the coherency model (rmem) with sail. The specification says that SINVAL.VMA behaves just as SFENCE.VMA, except there are additional ordering constraints with respect to the new SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we can treat SINVAL.VMA as if it were SFENCE.VMA.
-
- May 01, 2024
-
-
Alasdair authored
Sail has for a while now had a flexible way of passing additional information to either operational or axiomatic concurrency models by instantiating outcomes (effects) with model-specific types. The set of possible outcomes is defined in the Sail library, and a subset of these can be instantiated by any model. As part of adapting the model to this newer concurrency interface, the riscv_analysis file is no-longer needed, so it has been removed.
-