B - Bit Manipulation

Verification IP

Component is required for safety critical systems
Nein
Target TRL at the end of phase 1
TRL3: Nachweis der Funktionsfähigkeit --> Plattform ohne Parametrisierbarkeit
Target TRL at the end of phase 2
TRL4: Versuchsaufbau im Labor --> Plattform mit Parametrisierung

An RTL processor implementation can be verified using our co-simulation approaches, which compares the implementation with a functional reference model. As a functional reference model, an instruction set simulator (ISS) that is part of the open-source RISC-V VP can be used. Our cross-level processor verification approach generates endless instruction streams and tightly integrates the ISS with the RTL core with the aid of in-memory communication. The setup allows restriction-free instruction generation, enabling a comprehensive testing approach.

Status
Visibility
Internal for Scale4Edge partners only!

Fault Effect Simulation and Analysis for RISC-V (FEAR-V)

Image
FEAR-V Tool Flow
Component is required for safety critical systems
Ja
Target TRL at the end of phase 1
TRL6: Prototyp in vereinfachter/simulierter Einsatzumgebung --> Anwendungsfälle
Target TRL at the end of phase 2
TRL6: Prototyp in vereinfachter/simulierter Einsatzumgebung --> Anwendungsfälle

FEAR-V is a fast scalable simulation and analysis framework for RISC-V architectures based on QEMU. The generation, simulation, and analysis can be scaled by ISA configuration as well as n-bit permanent and transient faults. The fault injection covers GPR, CSR, instruction, and memory analysis.

Status
License

The source code of FEAR-V is freely available with all its components and has been published under https://github.com/hni-sct/fear-v.

Visibility
Publicly available!

FreiTest

Image
FreiTest Logo
Component is required for safety critical systems
Ja
Target TRL at the end of phase 1
TRL4: Versuchsaufbau im Labor --> Plattform mit Parametrisierung
Target TRL at the end of phase 2
TRL6: Prototyp in vereinfachter/simulierter Einsatzumgebung --> Anwendungsfälle

FreiTest (developed from PHAETON) is an ATPG (Automatic Test Pattern Generation) Framework based on SAT-Solving (Boolean Satisfiability Problem) and BMC (Bounded Model Checking). It generates Test Patterns and Software-Based Self-Tests (SBSTs) for synthesized circuits and is under active development. First results on achieved Fault Coverages have been published on the IEEE ETS2023 conference in Venice under the title "Constraint-Based Automatic SBST Generation for RISC-V Processor Families".

Status
Visibility
Publicly available!

Extensible Compiler (X-LLVM, Seal5)

Image
Extensible Compiler
Component is required for safety critical systems
Nein
Target TRL at the end of phase 1
TRL4: Versuchsaufbau im Labor --> Plattform mit Parametrisierung
Target TRL at the end of phase 2
TRL6: Prototyp in vereinfachter/simulierter Einsatzumgebung --> Anwendungsfälle

The Extensible Compiler provides an LLVM-based toolchain to develop C/C++/Assembly programs for RISC-V. It is designed to easily accommodate custom extensions to the RISC-V ISA by supporting the Scale4Edge developed CoreDSL for describing ISA extensions.

Status
License

Apache License 2.0

A permissive license whose main conditions require preservation of copyright and license notices. Contributors provide an express grant of patent rights. Licensed works, modifications, and larger works may be distributed under different terms and without source code.

Visibility
Publicly available!

CompCert - Formally verified C compiler

Image
Compilation steps performed by CompCert
Component is required for safety critical systems
Nein
Target TRL at the end of phase 1
TRL4: Versuchsaufbau im Labor --> Plattform mit Parametrisierung
Target TRL at the end of phase 2
TRL6: Prototyp in vereinfachter/simulierter Einsatzumgebung --> Anwendungsfälle

CompCert is a formally verified optimizing C compiler. It accepts most of the ISO-C 99 language, with some minor exceptions and a few useful extensions. Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance.

License

This distribution of CompCert can be used for evaluation and research, but not for commercial purposes (see also the license information in the installation packages). Commercial licenses can be obtained from AbsInt.

 

Visibility
Publicly available!