Semi Formal Instrumentation for Circuits and Systems – SFINCS

The SFINCS project (Semi-Formal INstrumentation for Circuits and Systems) investigates and develops new technologies for SoC validation. SFINCS addresses Assertion-Based Verification (ABV). During the design process, assertions (written for instance in PSL or in SVA) help describe:
? the results expected from the device (assert). These assert statements can be checked through the design flow using observation monitors.
? the constraints on the inputs (assume). Input sequences satisfying these assume statements can be produced by test sequence generators.

The aim of this project (see Figure 1) is to develop and integrate methodologies to apply ABV to a variety of hardware systems, using a uniform approach founded on a technology conceived in the TIMA Laboratory. We target the following designs:
? synchronous IPs described at the RT level
? pseudo-synchronous, mixed functions and GALS systems (Globally Asynchronous Locally Synchronous)
? HW/SW system aspects described at the SystemC TLM (transactional) level
? application to complex, mixed SoC and to safety critical systems.

In the HORUS prototype tool developed by the TIMA laboratory, synthesizable designs are automatically produced in Verilog or in VHDL for:
? synchronous or asynchronous observation monitors
? test sequence generators
? interfaces and history tracing mechanisms.
The approach is based on a library (VHDL or Verilog) of primitive components, one for each PSL or SVA primitive operator, and an interconnection scheme, both of them formally proven correct. It leads to optimised and synthesizable VHDL or Verilog descriptions.
Through the cooperation between the TIMA Laboratory and the Dolphin and Thales Communications companies, we will mainly carry out the following tasks:
? implementation by Dolphin of the HORUS technology for building synchronous monitors and test generators in the mixed signal simulation environment. Its incorporated tool for power consumption estimation will be useful for evaluating the consumption induced by the assertion logic. The HORUS method will be advantageous from early simulation to FPGA prototyping.
? the complete development of the emerging technique for building asynchronous monitors, and its implementation in the environment of Dolphin. This approach covers a wide range of applications domains (GALS, mixed functions, critical systems,...). Testbenches will be provided by Thales Communications. In particular, the technology will be experimented on safety critical components for avionics or security.
? the extension to descriptions of complex SoCs written in SystemC at the TLM (transactional level modelling) level. TIMA is currently defining an object-oriented model for adapting the monitoring approach of HORUS to this level. The technique will be fully specified, and implemented as a prototype tool. Its applicability to realistic designs will be demonstrated by experiments on SoC testbenches selected by Thales Communications.