| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
|
|
Very minor. Uses an existing type alias.
|
|
|
|
Implicit `var` declarations will eventually be an error. This makes some implicit `var` declarations explicit.
|
|
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.
|
|
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.
|
|
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
|
|
These guards were missing from one side of each clause.
|
|
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>
|
|
|
|
|
|
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.
|
|
|
|
|
|
These two instructions are RV64-only, as noted in the comment, but were missing the check. There are other instructions in this file that did have the check so it was just an ommission.
|
|
CSR MCONFIGPTR is defined in RISCV priv spec 1.12 but is missing from the
RISC-V SAIL model. This commit adds the read-only CSR MCONFIGPTR.
Co-authored-by: Dan Smathers <dan.smathers@seagate.com>
|
|
Signed-off-by: Xinlai Wan <xinlai.w@rioslab.org>
|
|
This adds an implementation of the Zcb code size extension.
Co-authored-by: Martin Berger <martinberger@users.noreply.github.com>
|
|
|
|
* Remove the duplicate mapping functions.
* Rename to `size_bytes` for consistency with the other two functions.
* Rename `size_bits` to `size_enc`, otherwise it's quite confusing that `size_bits` is not just `8 * size_bytes`.
Fixes #423
|
|
* Move `write_knd_of_flags` into its own function.
* Wrap really long lines
* Move PMP check into `phys_access_check` function. This is needed for two reasons:
- The CBO extension needs to do explicit access checks.
- In future it will also check PMAs so the name needs changing.
|
|
This has been broken for at least 2 years. This fixes the compilation.
Fixes #351
|
|
Old vmem code had much 'cut-and-paste' replication for RV32 (Sv32) and (#408)
RV64 (Sv39, Sv48), and was scattered over several files.
New code unifies them into single set of parameterized functions
that works for RV32/RV64 and Sv32/Sv39/Sv48 (and is ready for Sv57).
Deleted old files:
riscv_vmem_rv32.sail riscv_vmem_rv64.sail
riscv_vmem_sv32.sail riscv_vmem_sv39.sail riscv_vmem_sv48.sail
riscv_pte.sail
riscv_ptw.sail
Current files: all named riscv_vmem_*
riscv_vmem.sail (root file for vmem)
riscv_vmem_common.sail
riscv_vmem_pte.sail
riscv_vmem_ptw.sail
riscv_vmem_tlb.sail
riscv_vmem_types.sail
Modified top-level Makefile accordingly.
Added documentation on new vmem code: doc/notes_Virtual_Memory.adoc
|
|
Fixes #294
|
|
|
|
|
|
This is the newer, less confusing (and documented!) syntax. Fixes #425.
|
|
The restriction was present for `C.SLLI` but was missing for `C.SRLI` and `C.SRAI`.
The format is copied from `C.SLLI`.
Fixes #356
|
|
Some less-than/greater-than operators were missing. This adds the full set.
|
|
These were missed when those CSRs were implemented.
|
|
This script was used to do the modification:
```
from pathlib import Path
import re
RE_LINE = r"/\*={50,150}\*/\n"
RE_MIDDLE = r"/\*.*\*/\n"
NEW_TEXT = """/*=======================================================================================*/
/* 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 */
/*=======================================================================================*/
"""
REPLACEMENT = re.compile(rf"^{RE_LINE}(?:{RE_MIDDLE}){{10,100}}{RE_LINE}")
def main():
for file in Path("model").glob("**/*.sail"):
text = file.read_text(encoding="utf-8")
text = REPLACEMENT.sub(NEW_TEXT, text, 1)
file.write_text(text, encoding="utf-8")
if __name__ == "__main__":
main()
```
|
|
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.
|
|
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!
|
|
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
|
|
|
|
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>
|
|
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.
|
|
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.
|
