An exercise in the automatic verification of asynchronous designs

DOI10.1007/BF01384047MaRDI QIDQ1329086zbMATH OpenFDO

Authors George A. McCaskill, George J. Milne, Andrew D. Bailey

Publication date 4 September 1994

Published in Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

automatic formal verification techniquecircal systemcircuit designs

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Fault detection; testing in circuits and networks (94C12)

Recommendations

• scientific article; zbMATH DE number 3861073
• scientific article; zbMATH DE number 1796133
• Hierarchical verification of asynchronous circuits using temporal logic
• scientific article; zbMATH DE number 177508
• scientific article; zbMATH DE number 1852152

Cites work

• scientific article; zbMATH DE number 4004126 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3722109 (Why is no real title available?)
• scientific article; zbMATH DE number 8771 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 46118 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 139813 (Why is no real title available?)
• scientific article; zbMATH DE number 139979 (Why is no real title available?)
• scientific article; zbMATH DE number 177245 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• CCS expressions, finite state processes, and three problems of equivalence
• CIRCAL and the representation of communication, concurrency, and time
• Generating BDDs for symbolic model checking in CCS
• Graph-Based Algorithms for Boolean Function Manipulation
• Symbolic model checking: \(10^{20}\) states and beyond
• Testing equivalences for processes

Cited in

(14)

• scientific article; zbMATH DE number 139802 (Why is no real title available?)
• scientific article; zbMATH DE number 3880599 (Why is no real title available?)
• Designing and using a single-step functional model of an asynchronous automaton
• TTL: A modular language for hardware/software systems design.
• Towards a unifying CSP approach to hierarchical verification of asynchronous hardware
• Hierarchical verification of asynchronous circuits using temporal logic
• scientific article; zbMATH DE number 177508 (Why is no real title available?)
• scientific article; zbMATH DE number 1852152 (Why is no real title available?)
• scientific article; zbMATH DE number 139813 (Why is no real title available?)
• On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP
• scientific article; zbMATH DE number 3861073 (Why is no real title available?)
• scientific article; zbMATH DE number 3991420 (Why is no real title available?)
• Verification of building blocks for asynchronous circuits
• scientific article; zbMATH DE number 1852170 (Why is no real title available?)

Describes a project that uses

Uses Software

• HOL

This page was built for publication: An exercise in the automatic verification of asynchronous designs

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