PhD Thesis

< back to PhD thesis

« Asynchronous monitors synthesis from temporal assertions for the robust observation of synchronous circuits ».

Author: A. Porcher
Advisor: L. Fesquet
Co-advisor: K. Morin-Allory
President of jury: I. O'Connor
thesis reviewer(s): H. Mehrez, A. Salem,
These de Doctorat Université de Grenoble
Speciality: Nanoélectronique et Nanotechnologies
Defense: May 03 2012
ISBN: 978-2-84813-187-0


With the advent of complex integrated systems, the assertion based verification (ABV) has emerged as a solution for the semi-formal circuits verification. The ABV is used to validate that a circuit satisfies a property (or assertion). Previous work has shown that it is possible to synthesize these properties in the form of hardware monitors. These can then be embeddded permanantly on a circuit so that they provide monitoring task. With a goal of security and surveillance, the use of such monitors is a plus. Nevertheless, they are as sensitive as the monitored circuits to environmental degradation (voltage, temperature, age, ...). To reduce the risk of failure in monitors, originally designed as synchronous circuits, an asynchronous variant (quasi-delay insensitive) is proposed in this thesis. This work is part of the ANR project SFINCS (Thales, Dolphin Integration, TIMA) and led to the definition of a method for synthesizing asynchronous hardware monitors leveraging the robustness and modularity of asynchronous implementations. The studies focus primarily on the design of a library of basic asynchronous monitors and an ad hoc method of interconnection to build complex monitors. To ensure the robustness of these monitors, a study was conducted using formal verification tool RAT. In particular it was proved that the connection of an asynchronous monitor with a synchronous circuit (to watch) was particularly tricky because the timing assumptions of synchronous circuit impact the asynchronous monitor. It was therefore proposed to introduce a devicet, called "clock stretching", for controlling the clock of the synchronous circuit and relax synchronous timing assumptions that are applied to the asynchronous monitor.