Modelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench
Information Processing LettersPublished 23 January 2004
Hemangee K. Kapoor, Mark B. Josephs
Citations16
SJR quartileQ3
SJR score0.41
SNIP0.73
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
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.
Abstract
The modelling of delay-insensitive asynchronous circuits in the process calculus CCS is addressed. MUST-testing (rather than bisimulation) is found to support verification both of the property of delay-insensitivity and of design by stepwise refinement. Automated verification is possible with a well-known tool, the Edinburgh Concurrency Workbench.
Keywords
Computer Science
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.
OPAL (Open@LaTrobe) (La Trobe University)Algebraic theory of processes
851 Citations1988Matthew Hennessy
Algebraic Theory of Processes provides the first general and systematic introduction to the semantics of concurrent systems, a relatively new research area in computer science, and develops the mathematical foundations of the algebraic approach to the formal semantics of languages.
The MIT Press eBooksTrace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits
510 Citations1989David L. Dill
The problem of receptiveness is proved to be decidable, by reduction to Church's solvability problem, and the resulting verification methodology is naturally hierarchical, because specifications at one level of abstraction can be used as descriptions at higher levels of abstraction.
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.
Acta InformaticaReceptive process theory
86 Citations1992Mark B. Josephs
In essence, this paper reworks Hoare's theory of Communicating Sequential Processes under the above assumption about communication and verifies algebraically the design of a Muller C-element from a majority-element.
PRISM (University of Calgary)Practical verification and synthesis of low latency asynchronous systems
43 Citations1994Graham Birtwistle
A software prototype CAD tool called Analyze was written as part of this dissertation to allow the principles of this work to be tested and applied and to verify when a specification obeys all the burst-mode rules and can be automatically synthesized into an implementation.
An overview of D-I algebra
33 Citations2002Mark B. Josephs, Jan Tijmen Udding
D-I algebra, an algebra for the specification of the safety and progress properties of delay-insensitive circuits in terms of voltage-level transitions on wires, has played an important role both in suggesting decompositions and in verifying them.
IEEE Journal of Solid-State CircuitsReduced complexity two-phase micropipeline latch controller
12 Citations1998G. Taylor, G.M. Blair
A latch control circuit for two-phase micropipelines is presented and compared to previously published alternatives and compares favourably with four-phase latch controllers.
PRISM (University of Calgary)AMULET1: SPECIFICATION AND VERIFICATION IN CCS
11 Citations1995Ying Liu
This dissertation explores the feasibility of applying the CCS process algebra and its supporting tool, the Edinburgh Concurrency Workbench (CWB), to the formal specification and verification of a specific asynchronous microprocessor (AMULET1) developed by the AMULET group at Manchester University.