Formal Verification of Gate-Level Computer Systems

Mark Hillebrand, Sergey Tverdyshev

In: Anna Frid , Andrey Morozov , Andrey Rybalchenko , Klaus W. Wagner (Hrsg.). Computer Science -- Theory and Applications. International Computer Science Symposium in Russia (CSR-09) Fourth August 18-23 Novosibirsk Russia Seiten 322-333 Lecture Notes in Computer Science (LNCS) 5675 Springer 8/2009.


We present the formal verification of a gate-level computer system, in which a complex processor and external devices run in parallel. The system specification is an instruction set architecture with concurrently running visible devices. To the best of our knowledge this is the first formal treatment of integrating devices into a gate-level computer system.


Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence