The SFINCS project investigated and developed 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 was 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 targeted the following designs:
synchronous IPs described at the RT level
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 mainly carried out the following tasks:
implementation of the HORUS technology for building synchronous
monitors and test generators in a mixed signal simulation environment; experiments on a
complex design provided by Thales Communications
complete development of the emerging technique for building asynchronous
monitors
extension to descriptions of complex SoCs written in SystemC at
the TLM (transactional level modelling) level. The technique
has been fully specified, and implemented as a prototype tool (ISIS). Its applicability to
realistic designs has been demonstrated by experiments on a SoC testbench selected
by Thales Communications.
Meetings - Presentations
Kick-off meeting: March 18, 2008 (Grenoble)
Technical meetings TIMA/Dolphin (Task 1): April 1 and May 7, 2008 (Grenoble)
Technical meeting TIMA/Thales (Task 3): April 3, 2008 (Colombes)
Presentation of the short paper "Horus: A tool for Assertion-Based
Verification and on-line testing" at the 6th ACM-IEEE International Conference on
Formal Methods and Models for Codesign (MEMOCODE'2008),
Anaheim, June 2008.
Technical and organisational meetings: July 3 and September 2, 2008 (Grenoble)
Technical meeting (Task 1, synchronous monitors in a mixed signal simulation
environment): November 3, 2008 (Grenoble)
Plenary meeting: December 8, 2008 (Grenoble)
Task 1: Synchronous monitors in a mixed signal simulation environment
+ experiments on Thales problems
Task 2: Current status of the work on asynchronous monitors
Task 3: Current status of the work on TLM-oriented monitors
Presentation of the papers "Assertion-Based Verification and On-line
Testing in Horus" and "Generation of Test Programs for the
Assertion-Based Verification of TLM Models" at the IEEE International Design and Test
Workshop (IDT'08), Monastir, December 2008.
Technical meeting TIMA/Thales (Task 3): March 6, 2009 (Grenoble)
Technical meeting (Task 1, synchronous monitors in a mixed signal simulation
environment): May 14, 2009 (Grenoble)
Technical meeting: July 29, 2009 (Grenoble)
Task 1 (synchronous monitors in a mixed signal simulation environment), improvements for SERE operators
Organisational issues
Project review: September 10, 2009
Presentation of the papers "ISIS: Runtime Verification of TLM Platforms" and
"RAT-based Formal Verification of QDI Asynchronous Controllers" at the Forum on
specification & Design Languages (FDL'09), Sophia-Antipolis (France), September 2009.
Technical meeting: November 6, 2009 (Grenoble)
Task 1: common review of SMASH-Assert
Task 1: technical work about synchronous test generators in SMASH
Plenary meeting: December 7, 2009 (Grenoble)
Organisational aspects
Current status of Task 1 (monitors and generators in SMASH)
Task 1: experiments on Thales problems
Current status of Task 2 (asynchronous monitors)
Participation au Grand Colloque STIC, Paris,
Janvier 2010 (présentation d'un poster)
Technical meeting: May 20, 2010 (Grenoble)
Task 3: common study of a SystemC TLM platform provided by Thales Communications
Organisational issues
Plenary meeting: July 12, 2010 (Grenoble)
Organisational aspects
Current status of Task 1 (monitors and generators in SMASH)
Current status of Task 2 (asynchronous monitors), experiments on Thales examples
Current status of Task 3 (TLM monitors)
Technical meeting TIMA/Dolphin (Task 1): September 16, 2010 (Grenoble)
Technical meetings TIMA/Dolphin (Task 1): February 1, 2011 and March 31, 2011 (Grenoble)
Improvements for the monitors and generators
Experiments with a Thales case study
Technical meetings TIMA/Thales (Task 3): March 29, 2011 (Colombes) and June 7-8, 2011 (Grenoble)
References - Outcomes
M.Liu, D.Borrione, P.Ostier, L.Fesquet: "PSL-based online monitoring of
digital systems". Proc. FDL'05, September 2005.
D.Borrione, M.Liu, K.Morin-Allory, P.Ostier, L.Fesquet: "On-line
assertion-based verification with a proven correct library of monitors".
Proc. 3rd International Conference on Information
and Communication Technology (ICICT2005), December 2005.
K.Morin-Allory, D.Borrione: "Proven correct monitors from PSL specifications".
Proc. DATE'2006, March 2006.
K.Morin-Allory, L.Fesquet, D.Borrione: "Asynchronous Assertion Monitors for
multi-Clock Domain System Verification". Proc. IEEE International Workshop on
Rapid System Prototyping RSP'06, June 2006.
K.Morin-Allory, D.Borrione: "On-line monitoring of properties built on regular
expressions". Proc. FDL'2006, September 2006.
Y.Oddos, K.Morin-Allory, D.Borrione: "On-line vector generation from temporal
constraints written in PSL". Proc. VLSI-SoC'2006, October 2006.
K.Morin-Allory, L.Fesquet, D.Borrione, B.Roustan: "Asynchronous Online-Monitoring
of Logical and Temporal Assertions". Proc. FDL'07, September 2007.
K.Morin-Allory, E.Gascard, D.Borrione: "Synthesis of property monitors for on
line fault detection". Journal of Circuits, Systems, and Computers (JCSC),
Vol. 16 (6), December 2007.
Y.Oddos, K.Morin-Allory, D.Borrione: "Assertion-Based Design with Horus".
Proc. of 6th ACM-IEEE International Conference on Formal Methods and Models for
Codesign (MEMOCODE'2008), Anaheim, June 5-7, 2008 (short paper).
L.Pierre, L.Ferro: "A Tractable and Fast Method for Monitoring SystemC TLM
Specifications". IEEE Transactions on Computers, Vol. 57(10), October 2008.
IEEE page
On the way towards supporting assertion monitors, SMASH provides enhanced debugging
with expression watches, expression breakpoints and breakpoint actions (December 2008):
SMASH 5.12.
Y.Oddos, K.Morin-Allory, D.Borrione: "Assertion-based verification and on-line testing in Horus".
Proc. IEEE International Design and Test Workshop (IDT'08), Monastir (Tunisia), December 2008.
IEEE page
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), Monastir (Tunisia), December 2008.
IEEE page
SMASH now supports the verification of PSL properties using the simple subset with mixed-signal
extensions (June 2009):
SMASH 5.13.
L.Ferro, L.Pierre: "ISIS: Runtime Verification of TLM Platforms".
Proc. Forum on specification & Design Languages (FDL'09), Sophia-Antipolis (France), September 2009.
K.Alsayeg, K.Morin-Allory, L.Fesquet: "RAT-based Formal Verification of QDI Asynchronous Controllers".
Proc. Forum on specification & Design Languages (FDL'09), Sophia-Antipolis (France), September 2009.
Assertion-Based Verification capabilities in SMASH and SLED have been extended through increased PSL
compliance (December 2009):
SMASH 5.14.
L.Ferro, L.Pierre: "Formal Semantics for PSL Modeling Layer and Application to the Verification of Transactional Models".
Proc. DATE'2010, Dresden (Germany), March 2010.
A.Porcher, K.Morin-Allory, L.Fesquet: "Synthesis of Asynchronous Monitors for Critical Electronic Systems".
Proc. IEEE Symposium on Design and Diagnostics of Electronic Systems, Vienna (Austria), April 2010.
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.
Full Assertion-Based Verification support in the bundle of Schematic Link EDitor SLED with the mixed-signal
simulator SMASH, SLASH.
A.Porcher, K.Morin-Allory, L.Fesquet: "Does Asynchronous Technology bring Robustness in
Synchronous Circuit Monitoring?".
Proc. Forum on specification & Design Languages (FDL'11), Oldenburg (Germany), September 2011.
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.
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.
Back to the VDS Home Page
