At the end of the physical address range, the last address isn't turned
into an UT object. The scripts generating the memory regions
unnecessarily round down to a small page size when they could instead
round down to the smallest UT size and this memory could be used for
smaller kernel objects.
Signed-off-by: Kent McLeod <kent@kry10.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>
- Provide a nicer string for debugging purposes.
- improve comments about the purpose of __repr__() and __str__()
Signed-off-by: Axel Heider <axelheider@gmx.de>
- A region can't be created from an invalid range
- A region might be too small to support the change. There is no trivial
way to fix this.
Signed-off-by: Axel Heider <axelheider@gmx.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>
TQ Group produces a system-on-module family called TQMa8Xx.
The user manual for this SoM is available here:
https://www.tq-group.com/filedownloads/files/products/embedded/manuals/arm/embedded-modul/TQ-Socket/TQMa8Xx/TQMa8Xx.UM.0104.pdf
This SoM comes in a number of different configurations.
The specific NXP SoC used, and the amount of memory are both
configurable.
The TQMa8XQP is the part number for the TQMa8Xx family configured with
the i.MX 8QuadXPlus SoC.
The datasheet for the SoC is available here:
https://www.nxp.com/docs/en/data-sheet/IMX8QXPAEC.pdf
In addition to the SoC being configurable the amount of SDRAM
on the SoM is also configurable.
The support provided in this PR is specifically for the TQMa8XQP
configured for 1GiB of memory. Note: Actual usable memory available
to the ARM application processor is 1022MiB.
System-on-modules rely on an appropriate carrier board.
Testing of this PR has been done on the MBa8Xx carrier board
that is available from TQ Group as part of their starter kit.
To the best of my knowledge there is nothing in this PR
that depends on the carrier board itself; all code is SoM
specific and should support any carrier board.
Note: This support is very specifically for the TQMa8XQP configured
with 1GiB of memory.
This may be a starting point for supporting other boards that
also have the NXP i.MX 8QuadXPlus SoC (as well as the i.MX 8DXP
and possibly other SoC in the i.MX 8 family).
Support is limited to the specific SoM due to the way in which
platform support currently works for seL4. Building a kernel
currently relies on the information from the DTS file (which is
SoM + RAM configuration specific). It would be preferable to
allow more generic support but SoC families but that is beyond
the scope of this PR.
Signed-off-by: Ben Leslie <benno@brkawy.com>
The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Using explicit field name in the assignment states more clearly what the
generated code does. It is also more robust and allows the compiler to
catch potential inconsistencies in case the structure details change.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This implements GitHub PR #115 on the current repo state. /usr/bin/env
is already used for other (cmake/python/etc) invocations, and this PR
brings bash/sh into line with that for slightly improved portability.
Co-authored-by: Douglas Wilson <douglas.wilson@gmail.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Memoization is not worth it here, the runtime of the entire program
is tiny. Removing the comment to curb temptations in the future.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Avoid the warning 'WARNING:root:Not sure how to parse interrupts for
"/cpus/cpu@0/interrupt-controller"' when building for platform hifive.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
CMake treats any text output that is generated by tools during the
configuration phase as important if it isn't part of a message(STATUS)
command. Output generated by hardware_gen.py often shows up as warnings
about device tree properties that are usually uninformative. Resolving
some of the warning conditions removes these messages for most
platforms.
- Setting kernel_size in hardware.yml to 0x1000 to handle cases where
the kernel only needs the first page of a device that has a
device-tree definition larger than that.
- Remove status print about each Interrupt processed as it's usually not
useful information.
- Only process IRQs for a selected kernel device if the rule for that
device has any interrupt queries. This prevents warnings for IRQ
controllers that the script doesn't know how to process when it
doesn't need to.
Signed-off-by: Kent McLeod <kent@kry10.com>
This adds support for the ODroidC4. The ODroidC4 is just a beefier
ODroidC2 with some bits moved around. The devices we care about here are
all essentially the same except the cores are A55s instead of A53s.
Signed-off-by: Curtis Millar <curtis@curtism.me>
Add support the i.MX low-power UART. This is available on
chipsets such as i.MX8QXP.
Note: This is a preliminary patch in advance of providing
full support for the i.MX8QXP platform.
Note: getchar is not implemented (current) for this platform.
Signed-off-by: Ben Leslie <benno@brkawy.com>
The max IRQ and devicetree definitions are slightly outdated. This
commit updates these definitions.
Signed-off-by: Damon Lee <Damon.Lee@data61.csiro.au>
Isabelle2021 sometimes gets further with mask_simps, so this commit
makes them optional. Also removes a duplicate simp-rule warning.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
There are duplicate interrupts in some of the devices in the devicetree.
This commit removes these duplicate interrupt entries to avoid errors
with some of our tools (CAmkES, etc).
Signed-off-by: Damon Lee <Damon.Lee@data61.csiro.au>
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>
Fix tk1 smmu cmake config variables.
Fix platforn_gen for tk1.
Add separate hardware.yml for tk1.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
"const TYPE *ptr" creates a non-const pointer to const data; for the
pointer itself to be rodata requires "TYPE *const ptr".
Taking the size of the pointer is caught by -Werror by default; suppress
that.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
Changes the 'size suffix map' to be useful in more places. In general,
when we use the 'short name' of a variable in these generated proofs, we
run the risk of a change in variable declaration order breaking the
resulting proofs (since declaration order is how the C parser chooses
which variables get the short name). Best practice is to use the long
names whenever possible.
Uses the suffix map for some generated proofs.
Removes an unnecessary simp step.
Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
On e.g. FreeBSD, Bash lives at /usr/local/bin/bash. This change
makes the script find Bash wherever it may be hiding.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
These files are derived from the output of the device tree compiler in
the Linux kernel. The licenses of the input files do all have to be
compatible with at least GPL-2.0-only to be part of Linux.
