Trajectory-Directed discrete state space modeling for formal verification of nonlinear analog circuits
ICCAD（2012）
摘要
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.
更多查看译文
关键词
model checking case study,optimisation,analogue circuits,state-space methods,state space dynamics,formal verification algorithm,state space dynamic,dats,nonlinear network synthesis,circuit netlist,optimization problem,discrete model,state space,trajectory-directed discrete state space modeling,discrete state space modeling,discrete analog transition structure,higher accuracy,hidden circuit design error,underlying discrete analog transition,nonlinear analog circuit,trajectory-directed discrete state space,formal verification,discretization algorithm,mathematical model,monte carlo simulation,analog circuits,trajectory,logic simulation,sampling methods,vectors,redundancy
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要