Parallel Hierarchical Reachability Analysis for Analog Verification

Formal methods such as reachability analysis often suffer from state space explosion in the verification of complex analog circuits. This paper proposes a parallel hierarchical SMT-based reachability analysis technique based on circuit decomposition. Circuits are systematically decomposed into subsystems with less complex transient behaviors which can be solved in parallel. Then a simulation-assisted SMT-based reachability analysis approach is adopted to conservatively approximate the reachable spaces in each subsystem with support function representations. We formally develop a general decomposition algorithm without overapproxmiation in system reconstruction. The efficiency of this general methodology is further optimized with an efficient parallel implementation strategy.