Exception - 1 Level (Machine Level only) - for Compiler: Assembler only

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.

SymEx-VP focuses explicitly on testing software for constrained embedded devices (e.g. as used in the Internet of Things). This software often interacts very closely with low-level hardware peripherals and in order to support these interactions, during simulation-based software testing, SymEx-VP supports SystemC peripheral models. SystemC is a C++ class library for modeling hardware peripherals.

aiT automatically computes safe bounds for the worst-case execu­tion time of tasks in bina­ry execut­ables, taking into account the cache and pipe­line behavior of the processor in question.

StackAnalyzer automatically determines the worst-case stack usage of the tasks in embed­ded applications. It directly ana­lyzes binary execut­ables and considers all possible execution scenarios.

Based on years of experience developing and integrating SystemC based virtual platforms in the industry, MINRES has created DBT-RISE (Dynamic Binary Translation Re-targetable Instruction Set Simulator), a versatile environment to rapidly implement ISS of any architecture. DBT-RISE serves as basis for the implementation of the TGC (The Good Core) ISS (TGC-VP).

TGC-VP provides the following features:

The Good Folk Series is a highly flexible, scalable and configurable RISC-V based core family developed by MINRES. The standard cores can easily be tailored to specific application requirements using CoreDSL.

It is technology independent, ensures integrity and targets low power edge computing applications. The comprehensive SDK and concise documentation makes it accessible to small and medium companies.

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.