Formal Verification of CHP Specifications with CADP Illustration on an Asynchronous Network-on-Chip
Proceedings of the International Symposium on Advanced Research in Asynchronous Circuits and SystemsPublished 1 March 2007
Gwen Salaün, Wendelin Serwe, Yvain Thonnart, Pascal Vivet
Citations31
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A new approach for the formal verification of asynchronous architectures described in the high-level language CHP, by using model checking techniques provided by the CADP toolbox is described, based on an automatic translation from CHP into LOTOS, the process algebra used in CADP.
Abstract
Few formal verification techniques are currently avail-able for asynchronous designs. In this paper, we describe a new approach for the formal verification of asynchronous architectures described in the high-level language CHP, by using model checking techniques provided by the CADP toolbox. Our proposal is based on an automatic translation from CHP into LOTOS, the process algebra used in CADP. A translator has been implemented, which handles full CHP including the specific probe operator. The CADP toolbox capabilities allow the designer to ver-ify properties such as deadlock-freedom or protocol correct-ness on substantial systems. Our approach has been suc-cessfully applied to formally verify two complex designs. In this paper, we illustrate our technique on an asynchronous Network-on-Chip architecture. Its formal verification high-lights the need to carefully design systems exhibiting non-deterministic behavior. 1.
Keywords
Computer ScienceEngineering
Communication and Concurrency
6,859 Citations1989Robin Milner
This chapter discusses Bisimulation and Observation Equivalence as a Modelling Communication, a Programming Language, and its application to Equational laws.
Computer Networks and ISDN SystemsIntroduction to the ISO specification language LOTOS
1,293 Citations1987Tommaso Bolognesi, Ed Brinksma
IEEE Transactions on Parallel and Distributed SystemsThe odd-even turn model for adaptive routing
848 Citations2000Ge-Ming Chiu
Simulation results show that the even adaptiveness provided by the odd-even turn model makes message routing less vulnerable to nonuniform factors such as hot spot traffic and results in a smaller fluctuation of the network performance with respect to different traffic patterns.
Distributed ComputingCompiling communicating processes into delay-insensitive VLSI circuits
356 Citations1986Alain J. Martin
The circuits obtained are delay-insensitive, i.e., their correct operation is independent of any assumption on delays in operators and wires, except that the delays are finite.
Data Encryption Standard (DES)
321 Citations2011Alex Biryukov, Christophe De Cannière
DES was one of the first commercially developed (as opposed to government developed) ciphers whose structure was fully published and led to a wave of public interest in cryptography, from which much of the cryptography as the authors know it today was born.
An Asynchronous NOC Architecture Providing Low Latency Service and Its Multi-Level Design Framework
236 Citations2005Édith Beigné, F. Clermidy +3 more
The proposed NOC protocol and its asynchronous implementation are presented as well as the multi-level modeling approach using SystemC language and transaction-level-modeling, which shows that the asynchronous NOC can offer 5 Gbytes/s throughput in a 0.13 /spl mu/m CMOS technology.
Pipelined Asynchronous Circuits
215 Citations1998Andrew Lines
A design style for implementing communicating sequential processes (CSP) as quasi delay insensitive asynchronous circuits, based on the compilation method of [1], which can easily implement circuits with some slack between inputs and outputs is presented.
Science of Computer ProgrammingEfficient on-the-fly model-checking for regular alternation-free mu-calculus
159 Citations2002Radu Mateescu, Mihaela Sighireanu
The logic is an extension of the alternation-free µ-calculus with ACTL-like action formulas and PDL- like regular expressions, allowing a concise and intuitive description of safety, liveness, and fairness properties over labeled transition systems.
An overview of CADP 2001
151 Citations2001Hubert Garavel, Frédéric Lang +1 more
CADP is a toolbox for specifying and verifying asynchronous finite-state systems described using process algebraic languages, allowing to deal with communication protocols, distributed systems, embedded software, mobile telephony, asynchronous hardware, cryptography, security, human-computer interaction, etc.
The Computer JournalBalsa: An Asynchronous Hardware Synthesis Language
145 Citations2002D. Edwards
This paper introduces Balsa, a language and framework for synthesizing circuits using a technique of syntax direct translation and introduces the key features of the language.
Distributed ComputingA formal model for defining and classifying delay-insensitive circuits and systems
140 Citations1986Jan Tijmen Udding
Jan Tijmen Udding's research interests are mathematical aspects of VLSI, concurrency, program derivation and correctness, and functional programming.
Kluwer Academic Publishers eBooksSVL: A Scripting Language for Compositional Verification
91 Citations2006Hubert Garavel, Frédéric Lang
The SVL language is presented, which allows compositional verification of Lotos descriptions to be performed simply and efficiently, and a compiler for SVL has been implemented using an original compiler-generation technique based on the Enhanced Lotos language.
Design of On-chip and Off-chip Interfaces for a GALS NoC Architecture
87 Citations2006Édith Beigné, Pascal Vivet
The proposed on-chip interface not only handles the resynchronization between the synchronous and asynchronous NoC domains, but also implements NoC communication priorities, and a new concept of mixed synchronous/asynchronous dual mode NoC port is proposed as an efficient off-chip NoC interface for NoC-based open-platform prototyping.
Lecture notes in computer scienceSlack elasticity in concurrent computing
79 Citations1998Rajit Manohar, Alain J. Martin
Conditions under which the authors can modify the slack of a channel in a distributed computation without changing its behavior can be used to modify the degree of pipelining in an asynchronous system.
Information Processing LettersThe probe: An addition to communication primitives
58 Citations1985Alain J. Martin
Verification of an industrial SystemC/TLM model using LOTOS and CADP
34 Citations2009Hubert Garavel, Claude Helmstetter +2 more
This paper exploits a feature offered by the formal verification toolbox CADP, namely the import of external C code in a LOTOS model, to present an approach to the validation of a SystemC/TLM description by translation into LOTOS, reusing as much as possible of the original system level C++ code.
Lecture notes in computer scienceCompiler Construction Using LOTOS NT
26 Citations2002Hubert Garavel, Frédéric Lang +1 more
Much academic and industrial effort has been invested in compiler construction, and numerous tools and environments have been developed to improve compiler quality while reducing implementation and maintenance costs.
Lecture notes in computer scienceTranslating Hardware Process Algebras into Standard Process Algebras: Illustration with CHP and LOTOS
19 Citations2005Gwen Salaün, Wendelin Serwe
This paper gives a structural operational semantics for value-passing Chp, and describes the translation of Chp into the standard process algebra Lotos, in order to allow the application of the Cadp verification toolbox to asynchronous hardware designs.
The tangram framework (embedded tutorial)
17 Citations2001J. Kessels, A. Peeters
Using the Tangram framework, the design of asynchronous CMOS circuits, such as for instance for pagers and smart cards, which are clearly superior to synchronous designs are designed.
Information Processing LettersModelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench
16 Citations2004Hemangee K. Kapoor, Mark B. Josephs
The modelling of delay-insensitive asynchronous circuits in the process calculus CCS is addressed and MUST-testing (rather than bisimulation) is found to support verification both of file property ofdelay-insensitivity and of design by stepwise refinement.
Practicality of state-machine verification of speed-independent circuits
11 Citations2003Steven M. Nowick, David L. Dill
A state-machine verifier is described for speed-independent control circuits, using as an example an arbiter with reject to verifies the entire implementation of the circuit compared with a specification.
IFIP advances in information and communication technologyVerifying and Testing Asynchronous Circuits Using Lotos
10 Citations2000Ji He, Kenneth J. Turner
It is shown how Dill (Digital Logic in Lotos) can be used to specify, verify and test asynchronous (unclocked) hardware designs and new relations for (strong) conformance are defined.
Kluwer Academic Publishers eBooksValidation of Asynchronous Circuit Specifications Using IF/CADP
10 Citations2006D. Borrione, Menouer Boubekeur +3 more
This work addresses the analysis and validation of modular CHP specifications for asynchronous circuits, using formalisms and tools coming from the field of distributed software, which provides model checking and bi-simulation tools.
Verification and Implementation of Delay-Insensitive Processes in Restrictive Environments
4 Citations2006Hemangee K. Kapoor, Mark B. Josephs +1 more
SPIN as a Hardware Design Tool
3 Citations1995Budi Rahardjo
This paper presents the application of SPIN to verify a hardware design modelled in PROMELA and verified with SPIN, showing the presense of hazard.