Hardware Specification with Temporal Logic: An Example

DOI10.1109/TC.1982.1675978MaRDI QIDQ3934310zbMATH OpenOpenAlexFDO

Authors 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

reachability analysisformal verificationVLSI designlivenesssafenesslogic designactive 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)

Cited in

(10)

• The Birth of Model Checking
• Indentification of inductive properties during verification of synchronous sequential circuits
• BDD-based decision procedures for the modal logic K ★
• Newtonian arbiters cannot be proven correct
• An automata theoretic approach to Temporal Logic
• \(\infty\)-regular temporal logic and its model checking problem
• A logical approach to data-aware automated sequence generation
• Hierarchical verification of asynchronous circuits using temporal logic
• Description and reasoning of VLSI circuit in temporal logic
• Specification and verification of decentralized daisy chain arbiters with \(\omega\)-extended regular expressions

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

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