ISIS: Assertion-Based Verification of system-level requirements for SoC's

ISIS enables the runtime Assertion-Based Verification of SystemC TLM virtual platforms (untimed or timed), for verifying behavioural and transactional requirements. For example, it can help answer questions like:

• Are data correctly transferred by the communication channel?
• Does the software application properly interact with the DMA or coprocessor(s)?
• Are data accessed as expected in a memory?
• Does the software application conform to given hardware-related constraints?
• Is there a possible loss of data?
• ...and what are the frequencies/latencies that enable the respect of these properties?

Such transaction-oriented properties are formalized in PSL (IEEE standard 1850). The SoC description is automatically instrumented with assertion checkers associated with these system-level requirements, such that their satisfaction can be checked during simulation (independently of the chosen simulator).

Methodology

Our methodology [PF08] enables the automatic runtime verification of temporal properties, for SystemC TLM LT or AT (or even CABA) descriptions. It 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.
The main advantages of this methodology are:

• it enables verification at the System Level, and it supports TLM timed or untimed descriptions
• it supports the IEEE standard specification language PSL
• it is fully automatic, and it uses very efficient and formally proven checkers
• 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

For monitoring SystemC descriptions, 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 action occurs in the corresponding channel).
Hence, execution traces are made of all the actions 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.

Additional features:
•  Semantical and practical support for PSL assertions with auxiliary variables (PSL Modeling layer and global variables, multiple instances of PSL assertions with local variables). It enables to consider: properties that involve components which make concurrent data transfers possible (switches, pipelined busses), properties that are related to data processing throughout a platform or within memory, properties that consider possibly overlapping events (like interrupt processings), [Pi16], [PF10], [FP10].
•  The tool is equipped with a monitoring manager that gives the user the possibility to customize and to optimize the verification process (configuration of the monitors without recompilation, automatic monitors enabling/disabling according to conceptual correlation relations between properties), [CP14], [PC14].
The identification of verification key events in the assertion evaluations also alleviates debugging, [PC17].
•  Results about the refinement of system-level assertions, for reuse at the RT level - for dynamic or formal verification - once actual models of communication channels are introduced (protocol and timing), [Pi21],[PB13],[BP14].

Industrial case studies

• Application of the ISIS technology to a SoC platform for space telemetry 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) developed by Thales Communications and Security (SIES'2012 paper, [PF12]).

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. The SystemC simulator can then be run on this combination of modules; the monitors inform about the satisfaction of the properties during simulation.
ISIS can be installed on Linux or MacOS platforms.

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.
Five examples are reported here (see details in [FP09], [PF10], [FP11] and [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 an 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, a global memory, a hardware semaphore RAM, hardware terminals (TTY), and a viewer RAMDAC.
  The property under consideration 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).
• Modem SoC (Thales Communications and Security).
  This SoC contains an ARM processor and its data and instruction memories, an AHB-bridge-APB structure, an interrupt controller, a Viterbi decoder, and a DMA managing data transfers for a DDC (digital down converter). Four properties are reported:
  • a reading of the interrupt controller register IVR clears the interrupt request sent to the processor (P11),
  • the DMA generates an interrupt between two transfer requests (P12),
  • if the DDC has data to transfer, the DMA must initiate a transfer which is a read operation of the data in the DDC followed by a write operation in the memory (P13),
  • no loss of data for the SW application: there cannot be two consecutive DMA transfers at the same address in memory before a processor read at this address (P14).
  A simulation that corresponds to running the SoC platform for 55 ms (with a provided toy SW application, and a file with a limited amount of data) is reported.

 

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
Modem SoC, P11+P12+P13	47 s	48 s	406000
Modem SoC, P14	47 s	115 s	270000 + multiple sub-monitors devoted to the variety of memory addresses

 

References

• [Pi21] L.Pierre : "Refinement Rules for the Automatic TLM-to-RTL Conversion of Temporal Assertions". Integration, the VLSI Journal (Elsevier), vol.76, January 2021. See here.
• [PC17] L.Pierre, M.Chabot : "Assertion-Based Verification for SoC Models and Identification of Key Events". Proc. Euromicro Conference on Digital System Design (DSD'2017), Vienna (Austria), August 2017.
• [Pi16] L.Pierre : "Auxiliary Variables in Temporal Specifications: Semantic and Practical Analysis for System-Level Requirements". ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 21 (Issue 2), January 2016. See here.
• [BP14] Z.Bel Hadj Amor, L.Pierre, D.Borrione : "A Tool for the Automatic TLM-to-RTL Conversion of Embedded Systems Requirements for a Seamless Verification Flow". Proc. IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC'2014), Playa del Carmen (Mexico), October 2014.
• [PC14] L.Pierre, M.Chabot : "Customization of the Runtime Verification of Hardware/Software Virtual Platforms in ISIS". Proc. Forum on specification & Design Languages (FDL'14), Munich (Germany), October 2014 (Demo).
• [CP14] M.Chabot, L.Pierre : "A Customizable Monitoring Infrastructure for Hardware/Software Embedded Systems". Proc. 26th IFIP International Conference on Testing Software and Systems (ICTSS'2014), Madrid (Spain), September 2014.
• [PB13] L.Pierre, Z.Bel Hadj Amor : "Automatic Refinement of Requirements for Verification throughout the SoC Design Flow". Proc. International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS'13, Embedded Systems Week), Montreal (Canada), October 2013.
• [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.Pierreimag.fr (Laurence[dot]Pierre[at]univ-grenoble-alpes[dot]fr)
Tel. +33 (0)4 76 57 49 92