The SiFive Premier P550 [1] is a new development board from SiFive
that is based on the ESWIN EIC7700X SoC.
The platform is interesting to the seL4 community as it implements
the RISC-V hypervisor extension meaning we now have real hardware to
evaluate RISC-V hypervisor changes to seL4. It also implements the
Sscofpmf extension and so we'll be able to get more experiment with
proper profiling on RISC-V.
Unfortunately, it seems we still do not have proper ASID suppor
according to [2].
The board comes in two configurations, 16GB and 32GB of memory.
This adds support for the 16GB model.
The DTS comes from SiFive's fork of Linux [3].
No modifications were made, any extra things are in the overlay.
[1]: https://www.sifive.com/boards/hifive-premier-p550
[2]: https://forums.sifive.com/t/asid-vmid-support-in-p550-eic7700x/6887
[3]: https://github.com/sifive/riscv-linux/tree/dev/kernel/hifive-premier-p550
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
The comment that PRECISION is too low when the assert fails was wrong.
PRECISION should have no influence on it.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Move the ksCurTime assertions out of setDeadline, because they are not
necessarily true there. Assert ksCurTime in setNextInterrupt instead.
We only know that the deadline being set is at least ksCurTime -
getTimerPrecision(), which can be slightly in the past (ksCurTime is
already slightly in the past, at kernel entry).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Enable the timer only at initialization and since it is always
enabled. It is not needed to be re-enabled.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
Generic Timer IRQs are level-sensitive, when the CNT_TVAL
is updated the trigger condition is de-asserted and the
change is propagated to the GIC in a finite time to clear
the pending state.
However, we have to make sure the timer deasserts before
EOIR/DIR, otherwise the interrupt happens again. Therefore,
we need an isb() to cause the timer to de-assert before EOIR/DIR.
There is also a chance of spurious IRQ. A spurious IRQ can be
generated, in the case we have a level-sensitive IRQ, and its
pending state is cleared at device-level but not yet propagated
to the GIC. In between the IRQ deactivation and IRQ ack of the
new interrupt if the requested change from the timer gets propagated
then it causes a spurious IRQ.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
On the ZCU102 Rocketchip instantiation, the PLIC is available required
to use hardware peripherals like a UART
Signed-off-by: Chris Guikema <chris.guikema@dornerworks.com>
The memory mapping for the timer only uses 1K on AllwinnerA20, but
the minimum device mapping is 4K in seL4. Other devices within this
4K page (CCU and PIO) cannot be accessed in the userland.
Replace the kernel timer with the ARM generic timer on AllwinnerA20,
and remove the implementation for AllwinnerA20 specific timer in the
kernel. So we should have user access to those devices now.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
The platform was the original verification target of seL4 over 10 years
ago and by now there doesn't appear to be any ways to obtain new
hardware.
Currently, the KZM platform is the only ARMv6 platform and supporting it
requires a few work-arounds for emulating mechanisms that newer hardware
supports. Removing this platform also implies removing armv6 support
soon.
Signed-off-by: Kent McLeod <kent@kry10.com>
- Use SMP_TERNARY() macro.
- Rename get_hart_id() to plic_get_current_hart_id(), as this is just a
helper function for the other PLIC code in this file.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
RISC-V defines the concept of a PLIC, but leaves the details open. The
driver is for the PLIC of the SiFive U54/U74 SOC, which is used on
the HiFive Unleashed/Unmatched and Polarfire board.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- describe PLIC behavior and corner cases.
- provide a common header file for the API.
- add a dummy PLIC driver for spike.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Move CSR SIE access wrappers to generic code.
- Move CSR SIE/SIP bit constants to header file.
- Rename CSR SIE/SIP bit constants to use the names from the RISC-V
specification.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
Remove the UART handling details from the top level I/O handling that
implements printf(). The architecture's I/O handling must define how
the debug channel is implemented and what special handling is
required. This allows separating UART and SBI debug output handling.
Signed-off-by: Axel Heider <axelheider@gmx.de>
For 64-bit, this adds a 2nd-level page table for mapping devices using
2MiB frames instead of 1GiB frames.
The boot mapping and hardware header generator have also been fixed to
correctly report the number of large frames needed for devices rather
than only reporting the first. The frame size is also specified
correctly (rather than assuming mapping with 4KiB frames).
This likely fixes an issue whereby only the first 4KiB frame of a device
was reserved but the remaining region of that kernel device could be
mapped at user level.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
merge the PLIC drivers for ariane and hifive
Signed-off-by: Nils Wistoff <nwistoff@iis.ee.ethz.ch>
Reviewed-by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
The kernel connects ASID used in MMU and context banks used in
SMMU, and conducts TLB invalidation on context banks if a page
entry is invalidated from MMU is also used in SMMU.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls on stream ID caps that unbinds its
context banks. Any future transaction using this stream ID
will result on faluts.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing a system call that removes an assigned vspace root from its
context bank. This operation causes the context bank being disabled
as it does not have a valid vspace root after the unassignment.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls for conducting TLB invalidation operations
on all TLB entries or entries in a context bank.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls that binds context banks to stream IDs.
Once the stream ID is bound, the transaction using that SID is
enabled.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Supporting user-level applications to assign vsapce root to context
banks through system calls. This commit also configures the context
bank according to stage 1 or stage 2 requirement.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
This renames the RISCV PLIC driver file hifive.h to riscv_plic0.h to
better reflect the fact that the driver could be used for a number of
platforms that use the PLIC used by SiFive and SiFive derived platforms.
Signed-off-by: Jesse Millwood <jesse.millwood@dornerworks.com>
This method is a no-op for the hifive platform as all of its interrupts
are positive-level triggered. But we expose the API so that the verified
configuration can include this API method to make it easier to support
different RISC-V platforms under verified configurations in the future.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
Added support for reading and writing additional virtual timer
registers for vcpu hw read and write accesses. These include the
compare value register (CNTV_CVAL) and offset register (CNTV_OFF),
each represented as two 32 bit (high and low) registers on aarch32 and
as single 64 bit registers on aarch64.
Added support for explicitly saving and restoring the virtual
timer registers when the vcpu is enabled and disabled. This
ensures when the vcpu is switched in and out, the virtual timer
registers are restored to a state that is consistent to when
it was last run.
By default the CNTVOFF register will be updated by the kernel to
accumulate the time the VCPU is not running. From the guest this will
result in the VCNT register not increasing when the VCPU is suspended.
This behavior can be turned off by disabling the
KernelArmVtimerUpdateVOffset config option.
Every platform has to implement a standard set of interrupt interfaces
that the kernel uses to interract with a machine's interrupt controller.
Providing a single header file for each of these functions provides a
single location to document their behavior.
On exynos5 platforms the Arm Generic timer is available and is used for
MCS, but the mct.h is still used as the mct device needs to be
configured to implement the Arm Generic timer. mct.h is a common header
for register definitions while exynos4412-mct.h is used for implementing
timer functions on the exynos4 where the mct doesn't support being the
Arm generic timer.
Also remove misplaced initGenericTimer() declaration.
- use gpt, so we can have overflow and compare interrupts at the same
time (epit only allows compare)
- set the gpt to use the ipg_highfreq timer, as the standard ipg is too
low and breaks the timer calculations
