Hierarchical verification of asynchronous circuits using temporal logic

DOI10.1016/0304-3975(85)90223-3MaRDI QIDQ1070998zbMATH OpenOpenAlexFDO

Authors Bud Mishra, Edmund Clarke

Publication date 1985

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(85)90223-3

zbMATH Keywords

automatic verification systemComputation Tree LogicCTLefficient algorithmhierarchical verificationKripke Structurepropositional temporal logic of branching timeself-timed FIFO queue element

Mathematics Subject Classification ID

Other nonclassical logic (03B60)

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.

Recommendations

• scientific article; zbMATH DE number 3861073
• Automatic Verification of Sequential Circuits Using Temporal Logic
• An exercise in the automatic verification of asynchronous designs
• scientific article; zbMATH DE number 3932379
• scientific article; zbMATH DE number 1955911

Cites work

• A calculus of communicating systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Hardware Specification with Temporal Logic: An Example
• scientific article; zbMATH DE number 3848604 (Why is no real title available?)
• scientific article; zbMATH DE number 3861073 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)

Cited in

(19)

• Verification of a class of self-timed computational networks
• Characterizing finite Kripke structures in propositional temporal logic
• An exercise in the automatic verification of asynchronous designs
• The complexity of propositional linear temporal logics in simple cases
• Rewriting semantics of production rule sets
• Automatic and hierarchical verification for concurrent systems
• Unified temporal logic
• Towards a unifying CSP approach to hierarchical verification of asynchronous hardware
• scientific article; zbMATH DE number 3861073 (Why is no real title available?)
• Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
• The Birth of Model Checking
• From Philosophical to Industrial Logics
• Automatic Verification of Sequential Circuits Using Temporal Logic
• scientific article; zbMATH DE number 3991420 (Why is no real title available?)
• RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking
• scientific article; zbMATH DE number 139979 (Why is no real title available?)
• Functional and Logic Programming
• Automated Technology for Verification and Analysis
• From Monadic Logic to PSL

This page was built for publication: Hierarchical verification of asynchronous circuits using temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1070998)