Trajectory-Directed discrete state space modeling for formal verification of nonlinear analog circuits

In this paper a novel approach to discrete state space modeling of nonlinear analog circuits is presented, based on the introduction of an underlying discrete analog transition structure (DATS) and the related optimization problem of accurately representing a nonlinear analog circuit with a DATS. Starting from a circuit netlist, a partitioning of the state space to the discrete model is generated parallel and orthogonal to the trajectories of the state space dynamics. Therefore, compared to previous approaches, a significantly higher accuracy of the model is achieved with a lower number of states. The mapping of the partitioning to a DATS enables the application of formal verification algorithms. Experimental validations show the soundness of the approach with an increase in accuracy between a factor of 4 to 10 compared to the state of the art. A model checking case study illustrates the application of the new discretization algorithm to identify a hidden circuit design error.