Automatic Verification of Sequential Circuits Using Temporal Logic

DOI10.1109/TC.1986.1676711zbMath0604.94011MaRDI QIDQ3743249

M. C. Browne, Bud Mishra, Edmund M. Clarke, David L. Dill

Publication date: 1986

Published in: IEEE Transactions on Computers (Search for Journal in Brave)

zbMATH Keywords

hardware verificationpropositional temporal logicasynchronous circuitscorrectness of sequential circuitsstate-transition graphtruth of a temporal formula

Mathematics Subject Classification ID

Related Items

CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Indentification of inductive properties during verification of synchronous sequential circuits, Unified temporal logic, Characterizing finite Kripke structures in propositional temporal logic, The Birth of Model Checking, Reasoning about networks with many identical finite state processes, A model checker for linear time temporal logic, Symbolic model checking: \(10^{20}\) states and beyond, Verification of a multiprocessor cache protocol using simulation relations and higher-order logic, \(\infty\)-regular temporal logic and its model checking problem, Asynchronous Logic Circuits and Sheaf Obstructions, From Philosophical to Industrial Logics, Automatic and hierarchical verification for concurrent systems, From Monadic Logic to PSL