aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support
AgeCommit message (Collapse)AuthorFilesLines
2024-05-10lem: Add PMP related stubs for Isabelle buildAlasdair1-0/+8
These stub functions are required for building the Riscv.thy file from the generated lem file.
2024-02-05Improve PMP supportTim Hutt2-8/+0
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>
2023-12-19lem: Fix issues created by vector extensionAlasdair7-688/+146
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+
2023-10-17RISC-V Vector Extension SupportXinlai Wan1-0/+9
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.
2023-10-11Rename enable-fiom to enable-writable-fiomTim Hutt3-7/+7
This is a much clearer name because the option allows code to enable FIOM, it doesn't enable FIOM itself.
2023-10-11Implement menvcfgTim Hutt3-0/+9
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.
2023-06-15Run the pre-commit hook on all filesAlex Richardson7-72/+72
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.
2023-05-31Fix build for Coq 8.17Michael Sammler1-1/+1
2023-05-31Coq updates for Sail 0.15Brian Campbell2-15/+1
2023-05-29apply_headers: regenerate copyright headersupdate-copyright-headersPhilipp Tomsich6-6/+18
2023-05-29Add Zfa extension support (excl. quad-precision)Philipp Tomsich1-0/+27
This commit adds the following: - infrastructure for Zfa (e.g., existence macro) - support for the following instructions: + FLI.[HSD] + FMINM.[HSD] and FMAXM.[HSD] + FROUND.[HSD] and FROUNDNX.[HSD] + FMVH.X.D and FMVP.D.X + FLEQ.[HSD] and FLTQ.[HSD] + FCVTMOD.W.D Note the following implementation details: FMINM and FMAXM provide similar functionality to FMIN and FMAX, differing only in their NaN-handling: * FMIN/FMAX return a canonical NaN only if both operands are a NaN * FMINM/FMAXM return a canonical Nan if any operand is a NaN Consequently, the implementation is identical to FMIN/FMAX with only the NaN-related tests changed. FROUND instruction rounds a floating-point number in floating-point register rs1 and writes that integer, represented as a floating-point number to floating-point register rd while: * Zero and infinite inputs are copied to rd unmodified. * NaN inputs cause the invalid operation exception flag to be set. FROUNDNX instruction is defined similarly, but also sets the inexact exception flag if the input differs from the rounded result and is not NaN. FMVH.X.D instruction is available for RV32 only and moves bits 63:32 of floating-point register rs1 into integer register rd. FMVP.D.X instruction is available for RV32 only and moves a double-precision number from a pair of integer registers into a floating-point register. Integer registers rs1 and rs2 supply bits 31:0 and 63:32, respectively. FLEQ and FLTQ instructions are defined like the FLE and FLT instructions, except that quiet NaN inputs do not cause the invalid operation exception flag to be set. The FCVTMOD.W.D instruction is defined similarly to the FCVT.W.D instruction, with the following differences: * FCVTMOD.W.D always rounds towards zero. * Bits 31:0 are taken from the rounded, unbounded two's complement result, then sign-extended to XLEN bits and written to integer register rd. * Positive infinity, negative infinity and NaN are converted to zero. Signed-off-by: Charalampos Mitrodimas <charalampos.mitrodimas@vrull.eu> Signed-off-by: Philipp Tomsich <philipp.tomsich@vrull.eu>
2023-02-23Remove duopodBrian Campbell1-5/+0
This can now be found in the Sail repository. Includes an update to sail-riscv.install
2022-08-09Minimal updates for Coq proof assistant outputBrian Campbell1-2/+4
2022-01-19Add support for Zfh extension (#129)Bilal Sakhawat2-0/+128
2021-11-22Implement support for Zfinx (#130)Jessica Clarke4-0/+16
NB: Smstateen support is missing in the model so enabling the Zfinx extension provides an architectural covert channel via FCSR if privileged software is not aware of Zfinx's existence. Co-authored-by: Jessica Clarke <jrtc27@jrtc27.com> Co-authored-by: Ibrahim Abu Kharmeh <abukharmeh@gmail.com>
2021-11-17Revert "Initial introduction of zfinx (#75)"Jessica Clarke4-16/+0
This reverts commit c5e62ea4b3d481fcd491b22b317cc319b089f05d.
2021-11-17Initial introduction of zfinx (#75)Ibrahim Abu Kharmeh4-0/+16
* Adds Zfinx enable flag * Hardwire misa.{f,d} and mstats.FS to 0 * Moving nan boxing functions to fdext_reg * Swaps register names for floating point instructions Adds new mapping to swap register names, and use it in all assembly clauses * Disable Floating point loads, stores and moves * Add X_or_F_s and X_or_F_d functions, and use them to access all registers for floating points Changes register accessed for floating point instructions and modify nan boxing functions for zfinx * Formatting Remove couple of misplaced whitespace, unnecessary parens * Fix inconsistent indentation in insts_dext file * Fix spacing in fdext_regs * Remove redundant comparasion with true/ false * Constistant tuples spacing and removes couple of unnecessary parens. * Consistent functions declaration & calls spacing and removes couple of unnecessary parens. * Consistent spacing and removes couple of unnecessary comparasion with true/false * Make spacing consistent * Remove checks from execution stage * Add checks to encdec stage
2021-10-18scalar-crypto: Initial commit of 1.0.0-rc2 spec work. (#99)Ben Marshall2-0/+8
Merged scalar-crypto pull request #99 of 1.0.0-rc2 spec work from Ben Marshall. See https://github.com/riscv/sail-riscv/pull/99.
2021-07-29Use headache to apply copyright header at request of Peter Sewell.Robert Norton6-0/+408
2021-02-11Make N extension configurable.Prashanth Mundkur5-0/+17
2020-06-15Remove obsolete Coq axiomBrian Campbell1-2/+0
2020-06-15Update handwritten Coq support files to match current Sail.Brian Campbell2-10/+4
2020-04-07Switch floating-point comparisons to using softfloat to avoid missed ↵Prashanth Mundkur2-0/+32
corner-cases in hand-rolled helpers.
2020-01-23Add lem stubs for softfloat externs.rsnikhilPrashanth Mundkur2-0/+218
2020-01-22Some fixes for lem build.Prashanth Mundkur2-0/+8
2020-01-22Fix coq build.Prashanth Mundkur1-0/+1
2020-01-17Update handwritten Coq to use boolean predicatesBrian Campbell2-11/+13
Matches recent changes to Sail
2019-11-26Fix RV32 Coq buildThomas Bauereiss1-4/+4
2019-11-25Fix RV32 Lem buildThomas Bauereiss2-4/+4
2019-10-09Add {read,write}_ram for CoqThomas Bauereiss1-0/+11
2019-10-09Read/write memory values and metadata together atomicallyThomas Bauereiss2-0/+32
For Lem, bypass the Sail implementation of {read,write}_ram and map to atomic primitives directly. We might want to make these functions primitive for other backends as well.
2019-08-13Update barriers in Coq.Brian Campbell1-11/+11
2019-07-18Make sure everything builds correctlyAlasdair Armstrong2-45/+79
Move updated 0.11 lem files from Shaked's commit into their own directory Remove the 0.7.1 lem directory that performed a similar purpose during the prompt monad changes Re-add model changes from Shaked's commit with a feature flag
2019-07-18Revert "Support DMB/DSB domains"Alasdair Armstrong2-22/+22
Move this commit to new_barriers branch until we can update C/SMT/etc and make a new release of Sail for backwards compatability with the opam package This reverts commit 273ec8b0715b39844101c8081114f2697f291312.
2019-07-18Support DMB/DSB domainsShaked Flur2-22/+22
2019-06-24Add PMP checks to physical memory accesses.Prashanth Mundkur2-0/+8
- unify AccessType and ReadType since they were essentially redundant, making it easier to implement PMP checks for ReadWrite/atomic accesses. - add command line options to enable PMP in the platform - also fix the matching for the case when all entries are off
2019-04-25Fix coq build.Prashanth Mundkur1-19/+19
2019-04-25riscv_extras.lem: update read/write_mem calls with (dummy) addrsize argumentJon French1-18/+18
2019-04-10Update Coq memory interfacesBrian Campbell1-20/+27
(requires recent changes to the Coq library)
2019-04-04Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras fileBrian Campbell1-0/+3
2019-04-03Tweak print_* bindings for LemThomas Bauereiss2-0/+6
Map to a function that does not actuaylly output anything, in order to not confuse rmem.
2019-04-01Add missed lem definitions for sys misa/rvcflags.Prashanth Mundkur2-0/+16
2019-02-26Restore riscv_extras damaged by merge.Prashanth Mundkur1-9/+13
2019-02-13Make repository have shape RMEM expectsAlasdair Armstrong4-3/+140
2019-02-13Switch version of riscv_extras.lem depending on Sail versionAlasdair Armstrong1-0/+137
Works around change to write_mem function signature in monad embedding
2019-01-22Add build Makefile targets for prover backendsThomas Bauereiss1-4/+6
2019-01-21Output auxiliary Isabelle theories into generated_definitions/isabelleThomas Bauereiss1-2/+2
Also copy ROOT file into the same directory
2019-01-19Moved gen/ to handwritten_support/hgenShaked Flur19-0/+1367
2019-01-16More reorg.Prashanth Mundkur5-0/+439
. move prover files into a single support directory . generated_models -> generated_definitions . reset vector -> c_emulator
generated by cgit v1.1 at 2024-08-27 13:55:31 +0000