Verification of Analog/Mixed-Signal Systems with AADD

Abstract:
In this paper we give an overview of a tool and method for the verification of AMS systems. The tool turns SystemC AMS into a symbolic simulator using affine arithmetic decision diagrams (AADD). During symbolic simulation, the tool checks assertions on a representation of all possible output trajectories. Focus of the paper are the strategies that we combine to yield scalability and improve applicability in industrial design-flows: First of all, we reduce the problem of computing reachability to an LP-problem that can be solved efficiently. Second, we use SystemC AMS instead as formal methods as an input language. Third, we allow designers to combine concrete and symbolic simulation in the same tool – the SystemC proof-of-concept implementation – and using the same SystemC AMS models.