Re: Add Formal Verification chapter v3

2023-03-10 Thread Gedare Bloom
On Fri, Mar 10, 2023 at 8:19 AM andrew.butterfi...@scss.tcd.ie wrote: > > Hi Gedare, > the quick and easy way is to visit > https://github.com/andrewbutterfield/rtems-docs/commit/8165814471402d56c480b1400b121715ad507c58 > Yes, In this case, can you (or I can) create a Pull Request from your new-

[PATCH 4/4] bsps/zynqmp: Add JFFS2 NAND adapter

2023-03-10 Thread Kinsey Moore
This adds the glue code necessary to allow JFFS2 to operate on top of NAND memory hosted by the XNandPsu peripheral/driver. --- .../include/bsp/jffs2_xnandpsu.h | 56 +++ bsps/aarch64/xilinx-zynqmp/jffs2_xnandpsu.c | 326 ++ .../bsps/aarch64/xilinx-zynqmp/grp_zu3eg.

[PATCH 2/4] cpukit/jffs2: Import wbuf.c from upstream

2023-03-10 Thread Kinsey Moore
This pulls in wbuf.c from the upstream Linux repository at the state specified in VERSION. --- cpukit/libfs/src/jffs2/VERSION|1 + cpukit/libfs/src/jffs2/src/wbuf.c | 1350 + 2 files changed, 1351 insertions(+) create mode 100644 cpukit/libfs/src/jffs2/src/wbuf

[PATCH 3/4] cpukit/jffs2: Add support for NAND under JFFS2

2023-03-10 Thread Kinsey Moore
This adds write buffer and bad block support required for JFFS2 operation on NAND devices. This also adds the minor modifications necessary for RTEMS support in the Linux header stubs and in wbuf.c. Memory and NOR backed applications should experience no difference in operation since they do not ex

[PATCH 0/4] JFFS2 NAND Support

2023-03-10 Thread Kinsey Moore
This patch set adds NAND support for flash up to just under 4GB in size by way of write buffer support and an example adapter for ZynqMP systems using the XNandPsu peripheral. ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinf

[PATCH 1/4] cpukit/jffs2: Initialize and lock mutexes

2023-03-10 Thread Kinsey Moore
Mutexes must be locked before they can be unlocked. JFFS2 doesn't currently see this as an issue because all mutex operations are no-ops. --- cpukit/libfs/src/jffs2/src/dir-rtems.c | 2 ++ cpukit/libfs/src/jffs2/src/fs-rtems.c | 2 ++ 2 files changed, 4 insertions(+) diff --git a/cpukit/libfs/sr

[PATCH] bsps/xnandpsu: Allow use of both chip selects

2023-03-10 Thread Kinsey Moore
By default, the Xilinx NAND driver does not probe the second chip select. This alteration allows the second half of chips to be detected when present. --- bsps/include/dev/nand/xnandpsu.h | 4 1 file changed, 4 insertions(+) diff --git a/bsps/include/dev/nand/xnandpsu.h b/bsps/include/dev/na

Re: Add Formal Verification chapter v3

2023-03-10 Thread andrew.butterfi...@scss.tcd.ie
Hi Gedare, the quick and easy way is to visit https://github.com/andrewbutterfield/rtems-docs/commit/8165814471402d56c480b1400b121715ad507c58 That's a fork of RTEMS/rtems-docs on Github - and is the top of my `new-eng-chapter` branch. The commits are those I had developing it and do not match