| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
|
|
|
|
The leanprover/lean4:nightly-2025-11-18 toolchain requires the
ConcurrencyInterfaceV1 namespace to use Arch.
|
|
This allows support for the Za64rs and Za128rs profile-defined
extensions.
A trace option to track reservations has been added, to replace the
earlier debug log macro. This trace is outside the callback-driven
tracer for now; this could be fixed later.
The constants for platform configuration have been moved from
`sys/platform` to their own file in `core/platform_config` to enable
access from `core/extensions`.
The `load_reservation` platform handler now receives the requested
reservation width for asserts and logging.
|
|
Since we now use a proper header for the generated model code, we can
#include it in `riscv_softfloat.h` and use the `(fflags, bits(..))`
types to directly return the tuples that the rest of the Sail code wants
instead of using the super hacky method of poking some registers inside
the model.
This is much much cleaner, makes the softfloat functions pure, and
removes their dependency on the model *implementation*. Now it only
depends on the model types (and that is really only because C doesn't
have native tuple types; with fully native C++ codegen we could
theoretically have them return `std::tuple<...>`).
I also switched `riscv_softfloat.c` to C++ which has slightly nicer
syntax for returning values (and is more consistent with everything else
being C++).
|
|
Add following instructions to support bfloat16 conversions:
```
fcvt.bf16.s
fcvt.s.bf16
```
---------
Co-authored-by: Jordan Carlin <jordanmcarlin@gmail.com>
|
|
The `sys_enable_experimental_extensions` function was not added to the
handwritten files for the theorem provers.
This fixes the Lean build failure in #1245.
|
|
1. Add a PC reset address that PC is reset to every time the chip is
reset. Configure this to be the ELF entry point.
2. Switch the ELF entry point and HTIF tohost setting to be setters
rather than callbacks. These are static values and setters are much
easier to deal with.
3. Remove the unused `elf_tohost` and `elf_entry` functions.
|
|
Many of the old handwritten_support function definitions are no longer
used now that the config system is in place.
|
|
Use the new, shorter copyright header introduced for the rest of the
project in #389 for handwritten_support files.
|
|
I've previously used this to inject sprurious Store-Conditional
failures, however it required some tweaking because it's called very
early before various exceptions can happen.
A better solution is to spuriously cancel the reservation directly in
`load_reservation()` or by calling `cancel_reservation()`.
This change doesn't actually do that but I added notes explaining that
you can. In future when we provide a library interface we can do it like
that.
|
|
This adds a new target `generated_lean_rv64d_executable` that does not
use axioms nor any non-computable constructs so that it can be used as a
library for the forthcoming elf binary runner.
|
