Scale4Edge
Static hardware/software analyses in the context of scalable edge computing platforms
Start: 05/2020
End: 12/2025
Scale4Edge reduces the currently extensive development times and high development costs for application-specific edge components. The approach is based on providing an ecosystem for a scalable and flexibly expandable edge computing platform based on the free RISC-V instruction set architecture.
Verification of the entire hardware/software system is significant for application-specific, flexible edge computing platforms. Software development, for example, often falls back on assumptions about the hardware that are difficult to verify, as the hardware is only available as a closed system (black box). Nevertheless, statements about the hardware behavior must be considered during software verification. Scale4Edge investigates an approach considering the mutual interaction in HW/SW co-verification.
The approach’s core is the behavioral description, a description format that formally specifies assumptions about the hardware/software interaction. With the ‘verify-down’ tool, these assumptions can be automatically included in both the static software analysis and the formal hardware verification using Bounded Model Checking.
Via the domain-specific language CHIPS, the generator-based design process of RISC-V platforms is enhanced by a lightweight option for specifying hardware properties in a hardware generator. Utilizing the provided transformations, CHIPS properties can be automatically transferred to, e.g., SystemVerilog assertions.
Combining these approaches allows for comprehensive verification of the hardware/software system
