Skip to content

Commit 6e31ff3

Browse files
authored
Merge pull request #254 from magnmaeh/add-flexpret-docs
Add flexpret docs
2 parents ce0f1a8 + 8fe4654 commit 6e31ff3

File tree

1 file changed

+171
-0
lines changed

1 file changed

+171
-0
lines changed

docs/embedded/flexpret.mdx

+171
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
---
2+
title: FlexPRET
3+
description: Developing LF Programs for FlexPRET.
4+
---
5+
# Overview
6+
7+
FlexPRET is a precision-timed (PRET) machine designed for mixed-criticality systems. As of 2024, PRET machines are an open field of research. Refer to its [github page](https://github.com/pretis/flexpret) for more in-depth information. FlexPRET either needs to be emulated or run on a Field-Programmable Gate Array (FPGA). In this guide we will show you how to pair FlexPRET with Lingua Franca, leaving you with precise software execution.
8+
9+
As a developer, you should be aware of a significant difference between FlexPRET's notion of threads versus other platforms. FlexPRET uses fined-grained *hardware* threads, as opposed to the usual (software) threads. This means that if multiple threads are running, they can swap every clock cycle. In addition, hardware threads are designed to be isolated, meaning the execution time of one thread will not affect the execution time of another, as opposed to concurrent software threads. Since the threads are implemented in hardware, FlexPRET can only have a maximum of eight.
10+
11+
# Getting started
12+
13+
## Development environment setup
14+
15+
1. We start out by setting up a development environment. Clone the
16+
`lf-flexpret-template` from Github:
17+
```
18+
git clone --recurse-submodules https://github.com/lf-lang/lf-flexpret-template lf-flexpret-workspace && cd lf-flexpret-workspace
19+
```
20+
2. Source the `env.bash` to set up necessary environment variables. You will need to do this every time, so it could be a good idea to add this to your `~/.bashrc`.
21+
22+
## FlexPRET build
23+
24+
3. Now we will build the FlexPRET emulator. Step into the FlexPRET directory and build the default configuration with `cmake`.
25+
```
26+
cd $FP_PATH
27+
cmake -B build && cd build && make
28+
```
29+
30+
4. You should now install FlexPRET's hardware configuration to the software development kit (SDK). This provides the SDK with necessary information such as the amount of data memory available.
31+
```
32+
make install
33+
```
34+
35+
5. Next, step into the SDK and compile it. This step is strictly speaking not necessary, but it is good to know the system works as expected.
36+
```
37+
cd $FP_SDK_PATH
38+
cmake -B build && cd build && make && ctest
39+
```
40+
41+
## Lingua Franca on FlexPRET
42+
43+
6. Step back to the top-level directory and compile a sample LF application.
44+
```
45+
lfc src/HelloWorld.lf
46+
```
47+
48+
7. Run the compiled program on the FlexPRET emulator.
49+
```
50+
./bin/HelloWorld
51+
```
52+
53+
(This is just a `bash` script that runs the emulator and passes the correct program binary file to it underneath the hood.)
54+
55+
8. Verify that you see the expected output
56+
```
57+
[0]: ---- Start execution ----
58+
[0]: Environment 0: ---- Intializing start tag
59+
[0]: Environment 0: ---- Spawning 1 workers.
60+
[1]: Hello world from FlexPRET
61+
[1]: Goodbye
62+
```
63+
64+
(The `[<n>]` means hardware thread `n` is printing.)
65+
66+
# FlexPRET specific features
67+
68+
Some of FlexPRET's specific features are highlighted in the sample programs. These include `interrupt on expire`, which triggers an interrupt at some scheduled point in time and temporal isolation of hardware threads (i.e., isolated in timing).
69+
70+
## Interrupt on expire
71+
72+
The sample code is available in `src/InterruptExpire.lf`.
73+
74+
Run the application like so:
75+
76+
```
77+
lfc src/InterruptExpire.lf && ./bin/InterruptExpire
78+
```
79+
80+
## Temporal isolation
81+
82+
See `src/multi-threaded/Isolation.lf` for the sample application. The application runs a hardware thread in the background of an LF reactor that triggers every 50 milliseconds. The interrupt handler runs a long `for` loop. On other platforms, the interrupt handler would distrup the timing of the LF reaction. But due to temporal isolation, the LF reaction's timing is unaffected by the interrupts.
83+
84+
Run the application like so:
85+
86+
```
87+
lfc src/multi-threaded/Isolation.lf && ./bin/Isolation
88+
```
89+
90+
## Building FlexPRET with another configuration
91+
92+
Refer to the [FlexPRET docs](https://github.com/pretis/flexpret?tab=readme-ov-file#configuration) for more information on how to run a non-default and custom FlexPRET configuration.
93+
94+
# FlexPRET on FPGA
95+
96+
It is possible to realize FlexPRET on a Field-Programmable Gate Array (FPGA). Refer to [the docs](https://github.com/pretis/flexpret?tab=readme-ov-file#running-on-fpga).
97+
98+
Please note that for FPGA, only hardware thread 0 is connected to a UART peripheral, meaning only hardware thread 0 can print using that.
99+
100+
# Troubleshooting
101+
102+
## Environment not set up
103+
104+
```
105+
lfc: warning: No FP_PATH environment variable found
106+
lfc: warning: No FP_SDK_PATH environment variable found
107+
```
108+
109+
You probably forgot to `source env.bash` or `source env.fish`.
110+
111+
## FlexPRET not installed to SDK
112+
113+
This message means that the SDK did not find a FlexPRET installation.
114+
115+
```
116+
Could not find
117+
<path to workspace>/lf-flexpret-workspace/flexpret/sdk/flexpret/fp-emu.
118+
Please build FlexPRET and install it here with `cmake --install` to
119+
continue.
120+
```
121+
122+
In this case, you need to step into the FlexPRET directory, build FlexPRET (if
123+
not built already) and install it to the SDK.
124+
125+
```
126+
cd $FP_PATH
127+
cmake -B build && cd build && make all install
128+
```
129+
130+
## Instruction memory full
131+
132+
An error that looks like this means your program (i.e., your instructions) are
133+
too large to fit inside the instruction memory.
134+
135+
```
136+
/opt/riscv/lib/gcc/riscv32-unknown-elf/11.1.0/../../../../riscv32-unknown-elf/bin/ld: HelloWorld section `.text' will not fit in region `ROM'
137+
/opt/riscv/lib/gcc/riscv32-unknown-elf/11.1.0/../../../../riscv32-unknown-elf/bin/ld: region `ROM' overflowed by 70664 bytes
138+
```
139+
140+
There are two possible solutions to this issue:
141+
1. Reduce the size of your program. `printf` is notorious for taking up a lot of
142+
space, so consider replacing it with a lower footprint version (or nothing at all). Tip: To inspect
143+
what takes up space in your final executible, use `nm`, like so:
144+
`nm HelloWorld --size-sort`.
145+
1. Increase the size of the instruction memory. This is done in FlexPRET's
146+
configs (see [FlexPRET's README](https://github.com/pretis/flexpret?tab=readme-ov-file#configuration)). This is easily
147+
done when emulating FlexPRET, but might not be so simple when realizing the design on an FPGA.
148+
149+
## Bootloader not found
150+
151+
This error should only occur if you have specified `fpga` in the board target property. It means that you do not have not built the bootloader in the FlexPRET SDK.
152+
```
153+
/opt/riscv/lib/gcc/riscv32-unknown-elf/11.1.0/../../../../riscv32-unknown-elf/bin/ld: cannot open linker script file bootloader.ld: No such file or directory
154+
```
155+
156+
The solution is to build the SDK; it will build the bootloder and generate a `bootloader.ld`.
157+
158+
```
159+
cd $FP_SDK_PATH
160+
cmake -B build && cd build && make
161+
```
162+
163+
## Hardware vs. software configuration mismatch
164+
165+
This error occurs if the configuration used to build FlexPRET does not match the hardware configuration installed to FlexPRET's SDK.
166+
167+
```
168+
Reset_Handler: 165: Abort:[0]: Hardware and software configuration mismatch (0xef49961d vs. 0x79d84635)
169+
```
170+
171+
The solution is to rebuild FlexPRET and install its hardware configuration to the SDK with `make install`.

0 commit comments

Comments
 (0)