Next Craig Interpolant Prover (NCIP)
NCIP is a Bounded Model Checker (BMC) for solving formal problems in various input formats (AIGER / CNF). Using Craig interpolants it is able to prove unreachability for some formal problems that can be validated via generated unreachability certificates.
Longnail High-Level Hardware Synthesis of Custom RISC-V Instructions
The Longnail High-Level Synthesis system translates abstract descriptions of the semantics of custom instructions formulated in CoreDSL 2.0 into actual hardware-blocks in RTL.
proprietary
UPEC: Formal Security Verification
Figure: Speculative program execution can enable side channel
Formale Security Analyse (UPEC)
Abbildung: Spekulative Programmausführung kann Seitenkanal ermöglichen
On Chip Debug Solution
Lauterbach implements debugging and trace support in alignment with Partner Infineon specific Hardware Solution.
The Solution will be part of Lauterbach's commercial RISC-V Debug Tools
On Chip Debug Hardware
Infineon implements for its evaluation platform in alignment with Partner Lauterbach specific Hardware Components for On-Chip-Debug. The Hardware acts as Evaluation Vehicle for the Lauterbach On Chip Debug solution.
The Infineon Solution will be productized with its chips. It is therefore no tool or IP but part of semiconductor products.
PikeOS Operating System and Hypervisor
PikeOS and PikeOS for MPU are each a real-time operating system and hypervisor for embedded systems. It provides partitioning to separate different applications or guest operating systems from each other. PikeOS is often combined with ELinOS, SYSGO's embedded Linux, which is then run in a partition under the PikeOS hypervisor.
SYSGO issues evaluation licenses in the scope of the Scale4Edge project to interested project partners.