An exercise in the automatic verification of asynchronous designs

A.M. Bailey; G.A. McCaskill; G.J. Milne

doi:10.1007/BF01384047

An exercise in the automatic verification of asynchronous designs

A.M. Bailey, G.A. McCaskill, G.J. Milne

Mathematics and Computer Science

Research output: Contribution to journal › Article › Academic › peer-review

13 Citations (Scopus)

Abstract

This paper illustrates the practical application of an automatic formal verification technique to circuit designs of realistic complexity. The Circal System is presented and a number of asynchronous hardware modules are described and formally verified using it. Asynchronous logic is generally considered hard to design and analyse, and this serves as an appropriate demonstration of the features of a formal description and verification system.

Original language	English
Pages (from-to)	213-242
Journal	Formal Methods in System Design
Volume	4
Issue number	3
DOIs	https://doi.org/10.1007/BF01384047
Publication status	Published - 1994

Access to Document

10.1007/BF01384047

Cite this

@article{e5aa1ab5f0db4b4fb8e18d640350b58c,

title = "An exercise in the automatic verification of asynchronous designs",

abstract = "This paper illustrates the practical application of an automatic formal verification technique to circuit designs of realistic complexity. The Circal System is presented and a number of asynchronous hardware modules are described and formally verified using it. Asynchronous logic is generally considered hard to design and analyse, and this serves as an appropriate demonstration of the features of a formal description and verification system.",

author = "A.M. Bailey and G.A. McCaskill and G.J. Milne",

year = "1994",

doi = "10.1007/BF01384047",

language = "English",

volume = "4",

pages = "213--242",

journal = "Formal Methods in System Design",

issn = "0925-9856",

publisher = "Springer",

number = "3",

}

TY - JOUR

T1 - An exercise in the automatic verification of asynchronous designs

AU - Bailey, A.M.

AU - McCaskill, G.A.

AU - Milne, G.J.

PY - 1994

Y1 - 1994

N2 - This paper illustrates the practical application of an automatic formal verification technique to circuit designs of realistic complexity. The Circal System is presented and a number of asynchronous hardware modules are described and formally verified using it. Asynchronous logic is generally considered hard to design and analyse, and this serves as an appropriate demonstration of the features of a formal description and verification system.

AB - This paper illustrates the practical application of an automatic formal verification technique to circuit designs of realistic complexity. The Circal System is presented and a number of asynchronous hardware modules are described and formally verified using it. Asynchronous logic is generally considered hard to design and analyse, and this serves as an appropriate demonstration of the features of a formal description and verification system.

U2 - 10.1007/BF01384047

DO - 10.1007/BF01384047

M3 - Article

SN - 0925-9856

VL - 4

SP - 213

EP - 242

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 3

ER -

An exercise in the automatic verification of asynchronous designs

Abstract

Access to Document

Fingerprint

Cite this