Verifying RISC-V Platforms for Space

Space applications are booming, prompted by rapidly declining launch costs now attainable through commercial competition. Thanks to ventures like SpaceX, the cost to put a satellite into low earth orbit (LEO) has dropped from $20k/kg to $2k/kg today and is expected to drop further to $200/kg or lower. Plummeting costs drive new opportunities including widely accessible SATCOM (satellite communication), offering phone and broadband support through large constellations of satellites from Starlink and Amazon Leo (previously Amazon Kuiper). China is also on this bandwagon, building multiple constellations of their own. Standardization through the 3GPP (cellular) consortium is accelerating and will enable competitive interoperability, already partially supported in 5G-Advanced and expected to be fully supported in 6G. This isn’t just for emergency calls but also for regular calls direct to your smartphone. Standards-based phone communication, broadband and IoT support, across 85%+ of the earth’s surface where there are no terrestrial base stations? This is an exciting time for space-ready systems.

Equally space-based services will continue to grow in importance for defense, weather and climate monitoring, disaster support, and many other applications. Across all these deployments, expect to see growth in similar directions to those we see in terrestrial applications: AI, high performance servers, security, and much more. A new space-based economy is blossoming and will demand electronics able to function reliably for many years in this harsh environment.

Space-ready is not just about rad-hard

Radiation, solar and deep space, makes space a particularly hostile environment for electronics. Protection against electron cascades triggered by high energy cosmic rays demands special radiation hardened (rad-hard) processes, logic redundancy, ECC, all the tricks we now see for high-safety automotive systems but in space much more demanding, lacking the shielding our atmosphere provides.

Rad-hard is important but alone it is not enough. Beyond remotely triggered options, electronics in space can’t be serviced cost-effectively. If something stops working and a reset or reboot won’t fix the problem, the satellite is dead. This puts much higher emphasis on bullet-proof verification while the system is still in design. Good enough for a phone, even for a car, isn’t good enough for a satellite.

Comprehensive verification against a spec

Complex specifications present some unique challenges in this respect. According to Dave Kelf (CEO, Breker) the RISC-V International ISA spec runs to around 1400 pages, all carefully considered and agreed. Now you must verify behavior not just for what you added to the ISA but also across interactions with other features, driven by as many positive and corner case use-cases as you can construct.

It is not difficult to generate comprehensive unit test cases for rad-hardening features such as ECC or redundancy. Testing individually against other spec features, one at a time, say cache coherence management, may not be too bad but difficult to test comprehensively. But where testing becomes hard is in cross verifying all relevant use cases against each other. Real systems run many objectives simultaneously, stalling as needed to deal with traffic contention in bus fabrics. Stalls, latency and congestion are where difficult bugs lurk, satellite-dooming bugs. Getting to high confidence here requires system-level test definition, with the ability to run multiple use-cases simultaneously.

Breker’s approach to testing starts with system-level test models abstracted from implementation details, allowing you to easily combine VIPs defined at the same level. Breker themselves offer several VIPs, including RISC-V-related tests, together with tests checking coherency compliance, security and other areas. You can easily add your own models following the PSS standard or using standard C++, allowing for randomization especially around test models for your ISA extensions. Running these models together, generating interwoven and high demand traffic loads, will probe every dark corner of your system behavior.

What if you missed spec corners when building your test models?

The purpose of verification is to test compliance of your implementation with the spec. As a description of what compliance should mean, the RISC-V spec may be one of the more debated and refined specifications in our industry. But there is still a fallible, human step in mapping that document to a complete implementation of intent as represented in a test specification.

As linear documents, even the best and most reviewed of specs are an awkward way to capture a web of interconnected feature dependencies. This is not an academic concern. Dave shared a real challenge in interpreting RISC-V requirements around fence instructions. Quick reminder, these are instructions inserted in assembly code to control accesses to shared memory between multiple cores, which must be correctly ordered to avoid races. Standard coherence protocols can handle many but not all such cases. Special cases are typically application specific, such as a shared memory location used as a semaphore. Core A updates the semaphore indicating it is safe for core B to perform some other action. If core B reads the semaphore before Core A has updated, it may incorrectly assume it is OK to proceed. Adding fence instructions forces sufficient delay to avoid races between read and write.

Coherency bugs can be very challenging to catch, sometimes only appearing after billions of cycles in production. Not the kind of problem you want to see in a deployed satellite. The Breker guys spotted a RISC-V spec challenge that could lead to such a bug (leading one now loyal Breker customer to a redesign). The spec is completely accurate, detailing fence behaviors early in the document. But in a later unrelated part of the document, there is a mention of a fence behavior which is also important to understand, yet is easy to miss if your reading is limited to the earlier section.

Specs are living documents and it is probably unrealistic to expect this kind of problem cannot appear again. A safer approach would be to use AI to tease out such traps and more generally the web of relationships through a spec. I have talked earlier about Breker’s approach to AI, based on NLP rather than LLM. Dave tells me this is still in development, but they have already applied it to detect these distributed fence references in the spec, which it has done very successfully. To me this looks like an essential second step to closing the understanding loop in specs. First make sure the spec is oracle-worthy (not a problem for RISC-V), second make sure that you understand all relationship webs throughout the spec when translating into test models.

Very interesting. You can learn more in this press release on the Breker and FrontGrade Gaisler collaboration

Also Read:

A Principled AI Path to Spec-Driven Verification

RISC-V Virtualization and the Complexity of MMUs

How Breker is Helping to Solve the RISC-V Certification Problem