Speaker
Description
With the ever-increasing complexity of digital designs targeting both ASIC and FPGA technologies, the verification gap is not-so-slowly reaching the space sector. Although the space sector has been traditionally driven by rad-hard designs and devices that traded design capabilities and performance for radiation tolerance, recent advances in both microelectronics technology and usage of commercial off-the-shelf (COTS) components in the space sector have greatly increased the average complexity of digital designs in space applications.
In this age of even-more-complex digital designs, Formal Verification poses itself as a promising complement to simulation-based verification, with the potential to both uncover hard-to-find bugs, by performing exhaustive breadth-first searches, and to greatly increase the confidence in designs, by mathematically proving they work as expected.
The semiconductor sector is not blind to these facts: industry trends show an increase in the use of formal methods in general throughout the microelectronics industry… but not as much on ‘VHDL-centric teams’, because the majority of formal verification is typically done using SystemVerilog Assertions (SVA).
Therefore, the European space sector -which predominantly and traditionally has relied on VHDL- is at risk of getting left behind. If nothing is done, it will be a late adopter of formal verification techniques, resulting in high entry barriers, low efficiency, and a lot of redundant duplication of efforts, as teams struggle to implement these methods.
But simply recommending the usage of formal methods is not enough. Formal verification is difficult, both in conceptual difficulty and tool usage. Thus, there is a need to lower the adoption barriers for VHDL-centric teams within the European space sector.
With that objective in mind, the presentation will explain the advances on:
1. The definition of a Formal Verification Methodology for submodules and IP cores for the European space sector,
2. The development of a software framework that acts as an easy-to-use abstraction layer to interact with the formal tools,
3. A repository of examples, in increasing order of complexity, selected so the different concepts in the methodology can be learned incrementally, in a structured way.
This work is funded by the European Space Agency, through the activity "Lowering the adoption barriers for Formal Verification of ASIC and FPGA designs in the Space sector", ESA Contract No. 4000144681/24/NL/GLC/ov. The methodology, framework, and repository of examples will be published under a free and/or open-source (FOSS) license.
Affiliation of author(s)
Department of Electronic Engineering, Universidad de Sevilla //
Microelectronics Section, European Space Agency
| Track | Design Flow |
|---|
