Transistor sizing for parameter obfuscation of analog circuits
An approach is described for enhancing the security of analog circuits using Satisfiability Modulo Theory (SMT) based design space exploration. The technique takes as inputs generic circuit equations and performance constraints and, by exhaustively exploring the design space, outputs transistor sizes that satisfy the given constraints. The analog satisfiability (aSAT) methodology is applied to parameter biasing obfuscation, where the width of a transistor is obfuscated to mask circuit properties, while also limiting the number of keys that produce the target performance requirements.
1. A method for parameter obfuscation of an analog circuit comprising sizing a transistor using analog satisfiability (aSAT) applied to parameters, wherein the circuit property width of the transistor is obfuscated, wherein the transistor sizing is done using the following aSAT aglorithm:
a constraint formula φ is an input to a satisfiability modulo theory (SMT) solver along with technology dependent parameters;
the satisfiability of a circuit topology using the SMT solver begins by first selecting a random width and performance range (X, Y) for a circuit node along with the corresponding interval range in the decision process;
the SMT solver selects one of the unassigned variables and splits the interval of the variable into two subintervals of the same length;
the solver temporarily discards one of the subintervals and reduces the range of the selected interval;
an interval constraint propagation (ICP) technique is then applied to φ, wherein, If the ICP routine terminates with no conflict, then the algorithm returns to the decision step, and if a conflict exists in the interval due to a reduction of a variable to null, the source of the decision that lead to the conflict is located by the conflict driven clause learning (CDCL) algorithm;
when a union of conflict sources covers an entire search space, the algorithm returns UNSAT, otherwise, a backtrack routine is called and the aSAT algorithm returns to the decision process after adding a conflict clause to φ; and
the union of all the intervals is the superset of the solution space.
2. The method of claim 1 , wherein the analog circuit is a differential amplifier.
3. The method of claim 1 , wherein the analog circuit is a two-stage amplifier.
4. The method of claim 1 , wherein the analog circuit is an operational amplifier.