Database of Case Studies Achieved Using CADP

Asynchronous Circuit Implementing a Memory Protection Unit

Organisation: Tiempo SAS
CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG

Method: SystemVerilog
LNT
MCL

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design.

Period: 2018

Size: 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

Description: 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.

Conclusions: 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.

Publications: [Bouzafour-Renaudin-Garavel-et-al-18] Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, and Wendelin Serwe. 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

Contact:
Marc Renaudin
Tiempo Secure
110, rue Blaise Pascal
Bàtiment Viseo - Inovallée
38330 Montbonnot Saint-Martin
France
Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Thu Feb 11 11:57:43 2021.

Back to the CADP case studies page