Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC)
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 378864335 | ||
| 003 | CHVBK | ||
| 005 | 20180305123354.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 161128e20030401xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1524/itit.45.4.219.22731 |2 doi |
| 035 | |a (NATIONALLICENCE)gruyter-10.1524/itit.45.4.219.22731 | ||
| 245 | 0 | 0 | |a Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC) |h [Elektronische Daten] |c [Daniel Große, Rolf Drechsler] |
| 246 | 1 | |a An Approach for Formal Verification of Circuits in SystemC | |
| 520 | 3 | |a 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. | |
| 540 | |a © 2003 Oldenbourg Wissenschaftsverlag GmbH | ||
| 690 | 7 | |a Communications engineering / telecommunications |2 nationallicence | |
| 690 | 7 | |a Data in computer systems |2 nationallicence | |
| 690 | 7 | |a Systems management |2 nationallicence | |
| 700 | 1 | |a Große |D Daniel |4 aut | |
| 700 | 1 | |a Drechsler |D Rolf |4 aut | |
| 773 | 0 | |t it - Information Technology (vormals it+ti)/Methoden und innovative Anwendungen der Informatik und Informationstechnik |d Oldenbourg Wissenschaftsverlag GmbH |g 45/4/2003(2003-04-01), 219-226 |x 1611-2776 |q 45:4/2003<219 |1 2003 |2 45 |o itit | |
| 856 | 4 | 0 | |u https://doi.org/10.1524/itit.45.4.219.22731 |q text/html |z Onlinezugriff via DOI |
| 908 | |D 1 |a research article |2 jats | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1524/itit.45.4.219.22731 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Große |D Daniel |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Drechsler |D Rolf |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t it - Information Technology (vormals it+ti)/Methoden und innovative Anwendungen der Informatik und Informationstechnik |d Oldenbourg Wissenschaftsverlag GmbH |g 45/4/2003(2003-04-01), 219-226 |x 1611-2776 |q 45:4/2003<219 |1 2003 |2 45 |o itit | ||
| 900 | 7 | |b CC0 |u http://creativecommons.org/publicdomain/zero/1.0 |2 nationallicence | |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-gruyter | ||