Hardware Specification with Temporal Logic: An Example
From MaRDI portal
Publication:3934310
DOI10.1109/TC.1982.1675978zbMath0477.94036MaRDI QIDQ3934310
Publication date: 1982
Published in: IEEE Transactions on Computers (Search for Journal in Brave)
liveness; VLSI design; formal verification; reachability analysis; logic design; safeness; active circuits representing processes; finding design errors; self-timed arbiter; specification of memory
03B45: Modal logic (including the logic of norms)
68Q60: Specification and verification (program logics, model checking, etc.)
68N25: Theory of operating systems
Related Items
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, \(\infty\)-regular temporal logic and its model checking problem, Newtonian arbiters cannot be proven correct, Indentification of inductive properties during verification of synchronous sequential circuits, A Logical Approach to Data-Aware Automated Sequence Generation, The Birth of Model Checking, BDD-based decision procedures for the modal logic K ★