CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG
CADP (Construction and Analysis of Distributed Processes)
4000 lines of SystemVerilog
9000 lines of LNT
146 concurrent processes, connected through 250 internal channels
660 concurrent units
up to 116,812,174 states and 862,147,515 transitions
184 MCL properties
Asynchronous circuits have key advantages in terms of low energy
consumption, robustness, and security. However, the absence of a
global clock makes the design prone to deadlock, livelock,
synchronization, and resource-sharing errors. Formal verification is
thus essential for designing such circuits, but it is not widespread
enough, as many hardware designers are not familiar with it and few
verification tools can cope with asynchrony on complex designs.
This case study suggests an extension of Tiempo Secure's industrial design flow for asynchronous circuits, based upon the standard HDL SystemVerilog (SV), with the formal verification capabilities provided by CADP. This was achieved by translating SV descriptions into LNT, expressing correctness properties in MCL, and verifying them using the EVALUATOR model checker of CADP. It turned out that the constructs of SV and LNT are in close correspondence (almost line-by-line), and that the synthesizable subset of SV can be entirely translated into LNT. The MCL language was also shown adequate for expressing all property patterns relevant for asynchronous circuits.
The practicality of the approach was demonstrated on an asynchronous circuit implementing a memory protection unit (MPU). The MPU block exhibits a high degree of internal concurrency, comprising 660 parallel execution flows and 250 internal communication channels. The SV code of the MPU was translated manually into LNT; the higher number of lines is due to the absence of hardware specific datatypes, which are predefined in SV, but have to be provided for LNT. The corresponding state space was generated compositionally, by identifying a suitable minimization and composition strategy described in SVL (the largest intermediate state space had 116,812,174 states and 862,147,515 transitions). A set of 184 MCL properties were successfully verified on the state space, expressing the correct initialization of the MPU configuration registers, the mutual exclusion of read and write operations on registers, the correct responses to stimuli, and the security requirements related to the many access-control policies enforced by the MPU.
CADP with its languages LNT and MCL is suitable for the analysis of
complex asynchronous circuits. Due to the similarity of SystemVerilog
and LNT, the formal analysis fits into an industrial design flow, and
is usable by engineers. Thus, the approach has been applied to further
circuits designed by Tiempo.
Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, and
Model-checking Synthesizable SystemVerilog Descriptions of
Asynchronous Circuits. In Proceedings of the 24th IEEE International
Symposium on Asynchronous Circuits and Systems (ASYNC'18), Vienna,
Austria}, pp. 34-42, IEEE, May 2018.
Available on-line at: http://cadp.inria.fr/publications/Bouzafour-Renaudin-Garavel-et-al-18.html
110, rue Blaise Pascal
Bàtiment Viseo - Inovallée
38330 Montbonnot Saint-Martin
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|