Verification of linear equation sets with dynamic programming techniques

We propose a method for verifying electronic circuits that can be modeled as linear equation sets. Dynamic programming techniques are used to search the feasible solution space. The method can also be used to analyze the circuit for a range of input values and multiple input variables. The complexity of this method is O(n²), which is better than the O(n³) complexity of traditional solvers. This advantage is due to the efficiency of the simplex method in searching for solutions within a bounded space. We show how the method can also be used as a formal verification tool, maximum and minimum values of node voltages can be obtained for the given range of input voltages. In a single run of the solver multiple variables within the circuit can be optimized for all values of the sources within their bounds