ISIS - Efficient Verification of SystemC TLM Designs

ISIS: Assertion-Based Verification of SoC's described in SystemC TLM

ISIS is devoted to the runtime Assertion-Based Verification of SystemC TLM platforms (untimed or timed, clocked or unclocked), for verifying transaction-oriented properties formalized in PSL (IEEE standard 1850). It automatically instruments the SoC description with assertion checkers associated with system-level requirements, such that the satisfaction of those requirements is checked during simulation.
For example, it can help answer questions like:

Is a communication channel reliable?
Does my DMA protocol satisfy its specification?
Are data accessed as expected in a memory?
Does my software conform to given hardware-related constraints?
Does my trusted platform actually prevent access to sensitive data?

Methodology

Our methodology (IEEE TC paper, [PF08]) enables the automatic verification of temporal properties during simulation, for SystemC TLM LT or AT (or even CABA) descriptions. We can check the validity of PSL assertions that express properties regarding transactional operations i.e., requirements associated with the behaviour of some components of the SoC (DMA, interrupt controller,...) or with the interactions between hardware/software components.

In order to automatically produce SystemC monitors from PSL properties, we use a method inspired by the HORUS compositional technique. In this technology, the composite monitors are built as the interconnection of primitive components associated with the primitive operators of PSL.

For monitoring SystemC transactional descriptions, we adopt the following principle: the FL (Foundation Language) semantics of PSL is defined with regard to execution traces. At the synchronous RT level, the observations that constitute these traces are made on the clock edges. Transposing the interpretation at the TLM level, with the same PSL semantics, simply requires to identify the observation points at this level. We consider that observation points are when the assertion needs to be re-evaluated i.e., each time a variable of the assertion has possibly been modified (an appropriate event occurs in the corresponding channel). Hence, our traces are made of all the events that may enable the observation of updated values for the variables involved in the assertion. Technically, we use a model that allows to observe these transactional events in the system and to trigger the monitors when needed. This model is inspired by the well-known observer pattern.

The main advantages of this methodology are:

it supports the IEEE standard specification language PSL
it is fully automatic, and it uses very efficient and formally proven checkers
it supports TLM timed or untimed descriptions
it enables the verification of properties on hardware/software interactions
the observation mechanism does not rely on SystemC events
the assertions can involve as many channels as necessary, of any type (TLM channels or SystemC signals), and the values of the communication parameters can be taken into account in the assertions

- Recent improvements and achievements

Definition of an operational semantics of PSL endowed with the Modeling layer and implementation in ISIS (DATE'2010 paper, [FP10]).
Thanks to the PSL Modeling layer, auxiliary variables can be used in assertions. This feature is useful for instance to check the reliability of a communication channel: in the example below (Motion-JPEG decoding platform), an auxiliary variable enables the comparison of the transmitted and received data.

New features have been introduced to support properties about channels in which several communications overlap (e.g., pipelined behavior).
ISIS now supports reentrant assertions through the use of multiple checker instances. For example, this allows checking the correct delivery of every packet, for the 4x4 multicast helix packet switch given with the SystemC distribution (MEMOCODE'2010 paper, [PF10]). By the way, we found a small bug in this design (depending on their destination, some packets are not correctly delivered).

Application of the ISIS technology to a SoC Platform developed by Astrium: PSL formalization of requirements expressed by Astrium, automatic construction of the associated checkers and instrumentation of the platform, runtime verification (FMICS'2011 paper, [FP11]).

Presentation of experiments with ISIS on platforms of critical embedded systems developed by Airbus (avionics flight control remote module) and by Astrium (space high resolution image processing) at the workshop of the SoCKET project (November 2011).

Application of the ISIS technology to a modem SoC (for digital radio reception, supporting the DAB and DRM standards) developed by Thales Communications and Security (SIES'2012 paper, [PF12]): presentation at the SIES conference (June 2012).

Implementation

ISIS inputs PSL assertions and performs the automatic construction of TLM-oriented SystemC monitors, built compositionally from primitive components. The monitors are automatically linked to the design, this instrumented design is compiled using the SystemC library of primitive monitors, and the SystemC simulator can be run on this combination of modules. The monitors inform about the satisfaction of the properties during simulation.

Example

Let us consider the example of a Motion-JPEG decoding platform described at the Transaction Accurate level (from P.Gerin, X.Guérin, and F.Pétrot, "Efficient implementation of native software simulation for MPSoC", Proc. DATE'2008). It embeds a configurable number of processors (here we use one processor), a global memory, a hardware semaphore RAM, and hardware terminals (TTY). The traffic generator takes its data from a MJPEG file, and RAMDAC is the viewer.

One of the properties that can be checked to verify the reliability of the communication channel is:
the data that are written on the RAMDAC are exactly the ones that have been transmitted by the EU.
The figure below gives a screenshot of a simulation instrumented with the corresponding ISIS monitor. For this simulation, design errors have purposedly been introduced in the communication channel: while the image on the RAMDAC is not as expected, our monitor reports errors when detected (on the left).

Some experimental results

In the table below, CPU times are taken on an Intel Core2 Duo (3 GHz) under Debian Linux. The first column gives SystemC simulation times without any monitoring. The second column gives CPU times for simulation instrumented with our checkers. The number of times the checker functions have been evaluated is reported in the third column. Checkers construction times are negligible.

Four examples are reported here (see details in [FP09], [PF10] and [FP11]). The verification of a modem SoC developed by Thales Communications and Security is also reported in [PF12].

DMA system.
This case study (delivered with the first draft TLM 2.0 library) gives the implementation of a simple DMA system. A master programs the DMA through a router in order to perform transfers between two memories:
- it writes into DMA registers the source address, the destination address, and the length of the transfered data,
- then it requests for the transfer by writing into the DMA control register,
- afterwards, it waits for the dma irq signal from the DMA that indicates the completion of the transfer, and clears the DMA interrupt by resetting the control register. Once the DMA has received all the needed data, it performs the transfer between the two memories by alternating read and write operations.
We consider three properties:
- any time the control register is programmed, an end-of-transfer notification occurs before the next writing into the control register (P1),
- read and write operations in the memories alternate (P2),
- any time a source address is transfered, a read access in the first memory eventually occurs and the right address is used (P3).
For this example, 200000 memory transfers are performed, data of length 64 bytes are transfered (each atomic transfer carries 4 bytes i.e., 16 transfers are needed). For instance, the monitor for P3 is evaluated 4.2 million times (21 times for each transfer: 5 writings to the DMA + 16 read operations).

Motion-JPEG platform.
This is the Motion-JPEG decoding platform described above. The property is the data that are written on the RAMDAC are exactly the ones that have been transmitted by the EU (P4). A simulation that corresponds to 10 seconds of video decoding is reported.

Packet switch.
This is the 4x4 multicast helix packet switch given with the SystemC distribution. This switch uses a self routing ring of shift registers to transfer packets from one port to another in a pipelined fashion. Input and output ports have FIFO buffers of depth four each. Three properties are reported:
- each time a packet is received by a node, it was actually addressed to that node (P5),
- every packet sent by a sender X to a receiver Y will eventually be delivered (P6),
- two packets sent sequentially on the same input to the same destination will be received in the same order (P7).
The number of iterations is set to 5 millions. In each iteration, one packet per input and output is processed.

SoC for space telemetry (Astrium).
Among others, this platform includes a Leon processor and a convolution coprocessor. Three properties are reported:
- the Leon processor does not start a new convolution processing before the end of the previous one (P8),
- both the destination and source addresses are sent to the convolution unit before it starts a convolution processing (P9),
- the memory cannot emit two successive splits for the same master (P10).
For properties P8 and P9, the testbench is configured to process 100000 images (untimed simulation). For property P10, the testbench is configured to process 30000 images (timed simulation).

Properties	Simu. without monitoring	Simu. + ISIS checkers	# property evaluations
DMA, P1	4.97 s	5.18 s	1.4 millions
DMA, P2	4.97 s	6.21 s	6.4 millions
DMA, P3	4.97 s	5.54 s	4.2 millions
MJPEG platform, P4	18.67 s	21.64 s	13.7 millions (av.)
Packet switch, P5	8.94 s	9.56 s	4 millions (av.)
Packet switch, P6	8.94 s	15.81 s	1.6 millions (av.) + 60 millions (av.) of "eventually" sub-monitor
Packet switch, P7	8.94 s	10.03 s	1.8 millions (av.) + 2 millions (av.) for sub-monitors
SoC for space telemetry, P8	9.38 s	9.81 s	500000
SoC for space telemetry, P9	9.38 s	10.02 s	500000
SoC for space telemetry, P10	7.68 s	7.83 s	360000

References

[PF12] L.Pierre, L.Ferro, Z.Bel Hadj Amor, P.Bourgon, J.Quévremont : "Integrating PSL Properties into SystemC Transactional Modeling - Application to the Verification of a Modem SoC". Proc. IEEE International Symposium on Industrial Embedded Systems (SIES'2012), Karlsruhe (Germany), June 2012.

[PF11] L.Pierre, L.Ferro : "Dynamic Verification of SystemC Transactional Models". Chapter 22 of "Model-Based Testing for Embedded Systems" (Series "Computational Analysis, Synthesis, and Design of Dynamic Systems"), CRC Press, September 2011.

[FP11] L.Ferro, L.Pierre, Z.Bel Hadj Amor, J.Lachaize, V.Lefftz : "Runtime Verification of Typical Requirements for a Space Critical SoC Platform". Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'2011), Trento, August 2011 (Springer LNCS 6959).

[PF10] L.Pierre, L.Ferro: "Enhancing the Assertion-Based Verification of TLM Designs with Reentrancy". Proc. ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2010), Grenoble, July 2010.

[FP10] L.Ferro, L.Pierre: "Formal Semantics for PSL Modeling Layer and Application to the Verification of Transactional Models". Proc. DATE'2010, Dresden, March 2010.

[FP09] L.Ferro, L.Pierre: "ISIS: Runtime Verification of TLM Platforms". Proc. Forum on specification & Design Languages (FDL'09), Sophia-Antipolis (France), September 2009.
(Best Paper Award)
Also in "Advances in Design Methods from Modeling Languages for Embedded Systems and SoC's": Springer page

[FPL08] L.Ferro, L.Pierre, Y.Ledru, L.Du Bousquet: "Generation of Test Programs for the Assertion-Based Verification of TLM Models". Proc. IEEE International Design and Test Workshop (IDT'08), December 2008.

[PF08] L.Pierre, L.Ferro: "A Tractable and Fast Method for Monitoring SystemC TLM Specifications". IEEE Transactions on Computers, Vol. 57(10), October 2008 (Special Section on Programming Models and Architectures for Embedded Systems).

[Pi07] L.Pierre: "A Model for Assertion-Based Verification of TLM Designs". Report TIMA-RR--07/09-01--FR, TIMA Lab., 2007.

Contact:
Prof. Laurence PIERRE
TIMA Laboratory
Laurence.Pierre@imag.fr
Tel. +33 (0)4 76 57 49 92