|
| 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 |
| 8 | +systems. As of 2024, PRET machines are an open field of research. Refer to its |
| 9 | +[github page](https://github.com/pretis/flexpret) for more in-depth information. |
| 10 | +FlexPRET either needs to be emulated or run on a Field-Programmable Gate Array |
| 11 | +(FPGA). In this guide we will show you how to pair FlexPRET with Lingua Franca, |
| 12 | +leaving you with precise software execution. |
| 13 | + |
| 14 | +As a developer, you should be aware of a significant difference between FlexPRET's |
| 15 | +notion of threads versus other platforms. FlexPRET uses fined-grained *hardware* |
| 16 | +threads, as opposed to the usual (software) threads. This means that if multiple |
| 17 | +threads are running, they can swap every clock cycle. In addition, hardware |
| 18 | +threads are designed to be isolated, meaning the execution time of one thread |
| 19 | +will not affect the execution time of another, as opposed to concurrent software |
| 20 | +threads. Since the threads are implemented in hardware, FlexPRET can only have |
| 21 | +a maximum of eight. |
| 22 | + |
| 23 | +# Prerequisites |
| 24 | + |
| 25 | +- cmake |
| 26 | +- sbt to build FlexPRET |
| 27 | + |
| 28 | +# Getting started |
| 29 | + |
| 30 | +## Development environment setup |
| 31 | + |
| 32 | +1. We start out by setting up a development environment. Clone the |
| 33 | +`lf-flexpret-template` from Github: |
| 34 | +``` |
| 35 | +TODO: Github link with --recurse-submodules |
| 36 | +``` |
| 37 | +2. Source the `env.bash` or `env.fish` 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`. |
| 38 | +``` |
| 39 | +source env.bash |
| 40 | +``` |
| 41 | +``` |
| 42 | +source env.fish |
| 43 | +``` |
| 44 | + |
| 45 | +## FlexPRET build |
| 46 | + |
| 47 | +3. Now we will build the FlexPRET emulator. Step into the FlexPRET directory and build the default configuration with `cmake`. |
| 48 | +``` |
| 49 | +cd flexpret |
| 50 | +cmake -B build && cd build && make |
| 51 | +``` |
| 52 | + |
| 53 | +4. You should now install the FlexPRET build to the FlexPRET software development kit (SDK). This provides the SDK with the necessary knowledge of FlexPRET's hardware configuration, such as the amount of data memory available. |
| 54 | +``` |
| 55 | +make install |
| 56 | +``` |
| 57 | + |
| 58 | +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. |
| 59 | +``` |
| 60 | +cd ../sdk |
| 61 | +cmake -B build && cd build && make && ctest |
| 62 | +``` |
| 63 | + |
| 64 | +## Lingua Franca on FlexPRET |
| 65 | + |
| 66 | +6. Step back to the top-level directory and compile a sample LF application. |
| 67 | +``` |
| 68 | +lfc src/Test.lf |
| 69 | +``` |
| 70 | + |
| 71 | +7. Run the compiled program on the FlexPRET emulator. |
| 72 | +``` |
| 73 | +fp-emu +ispm=src-gen/Test/build/Test.mem |
| 74 | +``` |
| 75 | + |
| 76 | +8. Verify that you see the expected output |
| 77 | +``` |
| 78 | +TODO: Add expected output |
| 79 | +``` |
| 80 | + |
| 81 | +## Building FlexPRET with another configuration |
| 82 | + |
| 83 | +TODO: URL |
| 84 | +Refer to the [FlexPRET docs](./flexpret/README.md#Configuration) for more information on how to run a non-default and custom FlexPRET configuration. |
| 85 | + |
| 86 | +# FlexPRET on FPGA |
| 87 | + |
| 88 | +TODO: Write |
| 89 | + |
| 90 | +# FlexPRET specific features |
| 91 | + |
| 92 | + |
| 93 | +TODO: Describe and create example program |
| 94 | +1. fp_int_on_expire() |
| 95 | +2. interrupt temporal isolation |
| 96 | + |
| 97 | + |
0 commit comments