Ricerc@Sapienza

FPGA-synthesizable soft-processor cores are commonly used in many digital system applications with low medium production volume, to control heterogeneous dedicated computational units and I/O units. In such contexts, the inherently multi-tasking nature of the processor operation demands for a cost-effective and energy-efficient multi-threaded execution, either as multi-core architecture or multi-threaded single-core. This work presents an experimental exploration of microarchitecture design solutions for multi-threaded soft processor core implementations on FPGA.

Model checking has reached a maturity level that allows its techniques to be applied to the verification of industrial systems. Several algorithms and methods have been proposed to increase its effectiveness to tackle models of increasing complexity. In this chapter we present an application of Parallel Satisfiability Solving to the verification of embedded control systems. The adopted toolchain is part of the Formal Specs Verifier framework for the formal verification of Simulink/Stateflow models.