Automatisierte HW/SW Co-Verifikation von SystemC Modellen mit Hilfe von Timed Automata

Abstract

SystemC hat sich zum de-facto Standard zur Modellierung und Simulation im HW/SW Co-Design entwickelt. Existierende Verifikationstechniken für SystemC sind jedoch meist ad hoc und unsystematisch. Wir präsentieren ein formal fundiertes Framework zur systematischen und umfassenden Co-Verifikation von SystemC Modellen. Das Framework basiert auf einer von uns definierten formalen Semantik für SystemC und verwendet eine Kombination von Model Checking und Konformitätstesten zur automatisierten Qualiätssicherung während des gesamten Entwurfsablaufs. Wir demonstrieren die Leistungsfähigkeit unseres Ansatzes mit einem Packet Switch und einem System zur Anti-Blockier- und Anti-Schlupf-Regulierung.