| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
With the move to Sail 0.18 this is no longer needed.
|
|
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
|
|
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()
```
|
|
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.
|
|
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
|
|
|
|
|
|
|
|
|
|
spec. This is not possible for RV32, so pass zeros there.
|
|
definitions.
|
|
Can have unintended consequences, due to how overloading interacts
with casts. For example, x : X == y : X can be interpreted as
eq_string(cast(x), cast(y)) if x and y are both castable to string,
even when there is an equality function (X, X) -> bool. Sail->SMT
can't handle strings very well so it's best to just ensure that this
can never occur.
Rather than implicitly casting in logging statements like:
print("xyz" ^ x ^ " foo " ^ y)
it's now
print("xyz" ^ to_str(x) ^ " foo " ^ to_str(y))
which ensures that the conversion to strings only happens where
intended. I also added a warning to Sail itself to try to catch these
cases in future.
|
|
This showed up in RV32, but not in RV64, presumably because the highest address bits are not typically exercised typical physical memory maps.
|
|
|
|
|
|
simplicity. This might need revisiting for Sv59 and Sv64.
|
|
definitions for Sv32 and Sv48.
|
