Hardware Specification with Temporal Logic: An Example

DOI10.1109/TC.1982.1675978zbMath0477.94036OpenAlexW1967686058MaRDI QIDQ3934310

Gregor von Bochmann

Publication date: 1982

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

Full work available at URL: https://doi.org/10.1109/tc.1982.1675978

zbMATH Keywords

livenessVLSI designformal verificationreachability analysislogic designsafenessactive circuits representing processesfinding design errorsself-timed arbiterspecification of memory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items (9)

Specification and verification of decentralized daisy chain arbiters with \(\omega\)-extended regular expressions ⋮ A Logical Approach to Data-Aware Automated Sequence Generation ⋮ Indentification of inductive properties during verification of synchronous sequential circuits ⋮ The Birth of Model Checking ⋮ \(\infty\)-regular temporal logic and its model checking problem ⋮ BDD-based decision procedures for the modal logic K ★ ⋮ Newtonian arbiters cannot be proven correct ⋮ Hierarchical verification of asynchronous circuits using temporal logic ⋮ Description and reasoning of VLSI circuit in temporal logic

This page was built for publication: Hardware Specification with Temporal Logic: An Example