FM8501: a verified microprocessor
From MaRDI portal
Publication:1327711
zbMath0875.68008MaRDI QIDQ1327711
Publication date: 28 June 1994
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Computer system organization (68M99)
Related Items (10)
Gordon's computer: A hardware verification case study in OBJ3 ⋮ Algebraic models of correctness for abstract pipelines. ⋮ Wait-free linearization with a mechanical proof ⋮ Algebraic models of behaviour and correctness of SMT and CMT processors ⋮ Abstraction of hardware construction ⋮ On the comparison of HOL and Boyer-Moore for formal hardware verification ⋮ Unnamed Item ⋮ Algebraic models of microprocessors architecture and organisation ⋮ Symbolic constraint handling through unification in finite algebras ⋮ A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
This page was built for publication: FM8501: a verified microprocessor
