Symbolic Simulation of SystemC AMS Without Yet Another Compiler
Carna Zivkovic, Christoph Grimm · 2018
Modeling languages first of all support simulation that is considered as reference by designers. Formal verification and synthesis share the same languages. However, they usually require a separate, dedicated compiler. As modeling languages such as SystemC have reached a high complexity, it is very hard to support reasonably large language subsets, and to guarantee consistency with simulation semantics. This paper shows a way to use the simulator itself to generate a formal model of the complete dynamic behavior. Compared with using yet another compiler, this permits to improve consistency with simulation semantics, and to combine simulation with other use-cases. We concretely focus on symbolic simulation of SystemC AMS ([1], [2], IEEE Std 1666.1-2016), for which we generate AADD and BDD for symbolic simulation.