Correct-by-design hardware: FPGAs for satellite communication

Once launched, a satellite runs on the power its panels produce, cannot be repaired, and is too far away to debug. Whatever is on board, including any FPGAs, has to ‘just work’ and continue to work for many years, under extreme conditions. This is why our ‘correct by design’ approach of FPGA engineering is such a good fit with satellite communication technology.

Correct by design means that the specification is the part you spend most effort on, and the implementation follows from that specification almost automatically. At QBayLogic, we write specifications as an executable Haskell model, test that model before any hardware exists, and then refine that same model into a design. For a system you cannot reach after deployment, this is the order that produces the most reliable results.

Why satellite communication hardware is different

As of now, there are no QBayLogic-designed chips on satellites.

It has, however, been a subject of much discussion and thinking in our team, since the constraints of such an application seem to fit our engineering process perfectly. Satellites are extremely complex pieces of technology, consisting of many subsystems. Part of the reason these devices take so long to develop and build, is that testing such systems is very time-consuming. It’s almost impossible to put hardware this complex through a realistic test suite with every iteration, with proper test coverage, within budget and planning.

Our FPGA design process eases that load by providing hardware that guarantees to conform to the specification, before it’s even built.

A satellite cannot be repaired once it is launched, so most of the effort goes into the specification, before any hardware exists.

Correct by design: this is how we do it in practice

When we are asked to design an FPGA, we first take the specification and turn it into a model. The model is ordinary Haskell: a standalone program that can be compiled and run. Then we test it. Then we refine that model, in the same language, into a design that meets the performance targets, testing against the original specification after every step. The design never leaves the codebase the specification lives in.

This ensures that the design – first in software, then in hardware – does exactly what the specification says. For a space application, that is where you want the effort. On earth, late changes or bug discoveries are expensive. In space, they are impossible.

The limit here, of course, is that the specification can still be wrong. If a failure mode was missed, we have built a correct implementation of an incomplete specification. Correct by design does not remove that risk. It does move the whole effort to the point where the risk is cheapest to catch: before implementation, safely on the ground.

Why an executable specification finds more errors faster

In a traditional design process, the specification is prose and is checked by a person, in their head. A specification in code is checked by a compiler, mechanically, every time it runs. This way, the spec is checked more rigorously and a lot more often.

Another, ever more significant effect is what happens while you write the specification. Turning client input into code forces every vague statement into a decision. What exactly happens when the signal drops below this level? How much noise is acceptable before we stop trusting a symbol? Each decision shows up as a line to be written, and each line has consequences for how well the system, for example, copes with interference and, of course, for what it will cost to produce and operate. In prose, those questions can stay open until the very end, in code they cannot. The model implements the specification, but writing the model is also how the specification gets perfected.

With the model in hand you can start adding the environment: different kinds of noise, occlusion, multipath, directed interference. These are now tests on a software program, not on hardware, so they are cheap and fast to run and easy to extend when new test cases come up.

What the customer does with the model

In the TOmCAT project, which involved laser communication between satellites and ground stations, our responsibility was the turbulence correction chip, which was in the ground station. Atmospheric turbulence changes quickly, so the correction also had to be fast, making it a good fit for an FPGA.

Early in the project we sent the customer the Haskell model as a standalone executable with the agreed data interface. They ran it on their own data, on their own machines, without needing to install our design tools. Our development team, in turn, did not need access to their data. The client team iterated on their own, without us in the loop, and came back with what they found. Every failure that surfaced in their tests was fixed in the model in just a few hours, before detailed implementation started, where fixes are much more expensive.

When a specification does change late, the same structure helps. We change the model, then re-apply the refinement steps that led to the design. Every intermediate stage is still there to test against, because it is a permanent part of the code base.

The power of property-based testing

How you test matters as much as when you test. We tend to use property-based testing. You state a property the system must satisfy at a high level, for instance: every packet that enters an Ethernet switch must also leave it (no dropped packets). Then you generate pseudo-random inputs in large numbers and check the property against all of them.

Unit tests with hand-picked inputs tend to miss the edges. They also invite a specific failure that has become common: an implementation, written by a person or an AI, that fits the test cases and nothing else. A property cannot be fitted that way. Either it holds across all the generated inputs or it does not.

Where AI fits in

AI can now write a large part of an implementation for a satellite communication FPGA from a good specification. We see this in our own work: when the model and its constraints are set down in enough detail, a language model has very little room for errors or hallucinations. The constraints are key, because a language model will usually ‘take the easy route’ if these are absent, resulting in trivial tests and proofs.

Since our design methodology is engineered to eliminate error early in the process, we are usually in a position to define test criteria that cannot be ‘gamed’ by a language model. This makes AI increasingly valuable in at least parts of our work. Not to save time, but to increase the amount of (test) work we can do.

For a satellite, time saving is not the point. These types of projects have very long engineering processes, so saving a couple of days on FPGA testing would not matter. What the speed does buy us is coverage: more scenarios, more failure modes, more iterations on the model before the design is frozen. So when we use AI, we use it to increase quality by increasing test coverage.

Why all this matters: a look into the future

So, why do we spend so much time thinking about space technology? First, of course, because developing things for space is a technological challenge. And we like those. Also, we feel that QBayLogic has unique value to offer in this market. The standards for space technology, set in the ESA standards framework ECSS, are very strict and this will not change. What is changing, is the pressure to get from a specification to a working implementation faster.

The geopolitical circumstances have companies of all sizes and governments around the globe scrambling to get ahead in the race for digital dominance and space is very much a part of this competition. A method like ours, which puts the effort into an executable specification and generates the implementation from it, is built for exactly that: getting projects from idea to being guaranteed to work reliably within increasingly strict time constraints.

For us, the next step will probably be to implement formal verification and provable security into this process, which may eliminate a large part of the testing phase to speed up development even more while providing tighter guarantees on the security front. We’re already involved in research related to this, funded by the German government.

Why FPGAs on satellites must be correct by design: the specification is written as an executable Haskell model and tested before any hardware exists.