| Autor: |
Hutchison, David, Kanade, Takeo, Kittler, Josef, Kleinberg, Jon M., Mattern, Friedemann, Mitchell, John C., Naor, Moni, Nierstrasz, Oscar, Pandu Rangan, C., Steffen, Bernhard, Sudan, Madhu, Terzopoulos, Demetri, Tygar, Doug, Vardi, Moshe Y., Weikum, Gerhard, Bošnački, Dragan, Edelkamp, Stefan, Traulsen, Claus, Cornet, Jérôme, Moy, Matthieu |
| Zdroj: |
Model Checking Software (9783540733690); 2007, p204-222, 19p |
| Abstrakt: |
SystemC has become a de facto standard for the modeling of systems-on-a-chip, at various levels of abstraction, including the so-called transaction level (TL). Verifying properties of a TL model requires that SystemC be translated into some formally defined language for which there exist verification back-ends. Since SystemC has no formal semantics, this includes a careful encoding of the SystemC scheduler, which has both synchronous and asynchronous features, and a notion of time. In a previous work, we presented a complete chain from SystemC to a synchronous formalism and its associated verification tools. In this paper, we describe the encoding of the SystemC scheduler into an asynchronous formalism, namely promela (the input language for spin). We comment on the possible uses for this new encoding. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
