Hierarchical verification of asynchronous circuits using temporal logic
type: Item
instance of: scholarly article
title: Hierarchical verification of asynchronous circuits using temporal logic
zbMATH Open document ID: 0584.94022
DOI: 10.1016/0304-3975(85)90223-3
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: An automatic verification system is described, in which the specifications are expressed in a propositional temporal logic of branching time, called CTL (Computation Tree Logic). The syntax and the semantics CTL, as well as an efficient algorithm, called model checker for verifying temporal properties of an asynchronous circuit are presented. A simple step-by-step method to verify circuits and an example illustrating how some interesting properties of a self-timed FIFO queue element may be obtained, are given. A hierarchical method to verify large and complex circuits is introduced and some properties of the operation of restriction on a Kripke Structure are studied. The paper concludes with a discussion on some shortcomings of the proposed approach and different open problems.
Mathematics Subject Classification ID: 94C10
Mathematics Subject Classification ID: 03B60
zbMATH DE Number: 3937106
zbMATH Keywords: hierarchical verification
zbMATH Keywords: automatic verification system
zbMATH Keywords: propositional temporal logic of branching time
zbMATH Keywords: Computation Tree Logic
zbMATH Keywords: CTL
zbMATH Keywords: efficient algorithm
zbMATH Keywords: self-timed FIFO queue element
zbMATH Keywords: Kripke Structure
author: Bud Mishra
author: Edmund Clarke
reviewed by: Leon Livovschi
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90223-3
OpenAlex ID: W2080641824
cites work: Hardware Specification with Temporal Logic: An Example
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Q3329397
cites work: Q3906386
cites work: Q3318104
cites work: A calculus of communicating systems
description: scientific article; zbMATH DE number 3937106