caa a22 4500 378864335 CHVBK 20180305123354.0 cr unu---uuuuu 161128e20030401xx s 000 0 eng 10.1524/itit.45.4.219.22731 doi (NATIONALLICENCE)gruyter-10.1524/itit.45.4.219.22731 Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC) [Elektronische Daten] [Daniel Große, Rolf Drechsler] An Approach for Formal Verification of Circuits in SystemC Der vorgestellte Ansatz ermöglicht es, für SystemC-Schaltkreisbeschreibungen, die über einer gegebenen Gatterbibliothek definiert sind, Eigenschaften zu beweisen (engl. property checking). Als Spezifikationssprache wird LTL (linear time temporal logic) verwendet. Für den Beweis einer LTL-Eigenschaft kann die Erfüllbarkeit einer Booleschen Funktion betrachtet werden, die aus der Eigenschaft und der Schaltkreisbeschreibung mittels symbolischer Methoden konstruiert wird. Im Gegensatz zu simulationsbasierten Ansätzen kann dabei Vollständigkeit gewährleistet werden. Anhand einer Fallstudie eines skalierbaren Arbiters wird die Effizienz des Beweisverfahrens untersucht. © 2003 Oldenbourg Wissenschaftsverlag GmbH Communications engineering / telecommunications nationallicence Data in computer systems nationallicence Systems management nationallicence Große Daniel aut Drechsler Rolf aut it - Information Technology (vormals it+ti)/Methoden und innovative Anwendungen der Informatik und Informationstechnik Oldenbourg Wissenschaftsverlag GmbH 45/4/2003(2003-04-01), 219-226 1611-2776 45:4/2003<219 2003 45 itit https://doi.org/10.1524/itit.45.4.219.22731 text/html Onlinezugriff via DOI 1 research article jats NATIONALLICENCE 856 40 https://doi.org/10.1524/itit.45.4.219.22731 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Große Daniel aut NATIONALLICENCE 700 1- Drechsler Rolf aut NATIONALLICENCE 773 0- it - Information Technology (vormals it+ti)/Methoden und innovative Anwendungen der Informatik und Informationstechnik Oldenbourg Wissenschaftsverlag GmbH 45/4/2003(2003-04-01), 219-226 1611-2776 45:4/2003<219 2003 45 itit CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-gruyter