Static Analysis for SystemC with Scoot: From Verification to Simulation
Blanc, Nicolas · Repository for Publications and Research Data (ETH Zurich) · 2010
S YSTEMC is a description language for computer systems that is based on C++.The language is used for modeling electronic devices at arbitrary levels of abstraction.In particular, SystemC can describe models with both hardware and software aspects.As today's electronic designs are incredibly large and complex, validation of new products remains time consuming as ever; hence the need to keep improving state-of-the-art verification techniques.We describe verification solutions for SystemC to improve reliability of computer devices by combining formal reasoning and simulation at high-level of abstraction.In particular, our research indicates that formal methods have applications beyond property checking, namely for code optimizations, simulation, and testing.We show that verification engines can be integreted into compilation flows to compute information valuable at runtime, statically.More specifically, our results demonstrate that an application of formal engines at high abstraction level is practical provided that: