Finite State Machine Vulnerability and Pipeline Analysis Using Satisfiability Modeling
AssigneeBattelle Memorial Institute
InventorsKatie T. Liszewski, Timothy A. McDonley
Life of this patent
Estimating the term…
Abstract
The present disclosure provides a satisfiability modulo theory (SMT) modeling system that includes graphical representation circuitry to generate graphical data representing a circuit design; finite state machine (FSM) discovery circuitry to discover, based on a feedback loop of the circuit design, an FSM contained within the graphical data; SMT assertion generation circuitry to generate an SMT assertion set of the FSM, based on the combinatorial and/or sequential logic elements associated with the FSM; and SMT modeling circuitry to determine a behavior of the FSM by applying one or more logical functions to the SMT assertion set.
Claims17
A satisfiability modulo theory (SMT) modeling system, comprising:
- graphical representation circuitry to generate graphical data representing a circuit design;
- finite state machine (FSM) discovery circuitry to discover, based on a feedback loop of the circuit design, an FSM contained within the graphical data;
- SMT assertion generation circuitry to generate an SMT assertion set of the FSM, based on the combinatorial and/or sequential logic elements associated with the FSM;
- and
- SMT modeling circuitry to determine a state transition behavior of the FSM based on one or more logical functions applied to the SMT assertion set;
- wherein the SMT modelling circuitry is further configured to determine if a desired state of the FSM is reachable within a selected number of clock cycles.
A non-transitory storage device that includes machine-readable instructions that, when executed by one or more processors, cause the one or more processors to perform operations, comprising:
- generate graph-based data to graphically represent a circuit design;
- identify, based on a feedback loop of the circuit design, a finite state machine (FSM) in the graph-based data of the circuit design;
- generate, for the FSM identified in the graph-based data, an satisfiability modulo theory (SMT) assertion set, based on the combinatorial and/or sequential logic elements associated with the FSM;
- model the SMT assert set to determine a state transition behavior of the FSM based on one or more logical functions applied to the SMT assertion set;
- and
- determine if a desired state of the FSM is reachable within a selected number of clock cycles.
A non-transitory storage device that includes machine-readable instructions that, when executed by one or more processors, cause the one or more processors to perform operations, comprising:
- generate graph-based data to graphically represent a circuit design;
- identify, based on a feedback loop of the circuit design, a finite state machine (FSM) in the graph-based data of the circuit design;
- generate, for the FSM identified in the graph-based data, a satisfiability modulo theory (SMT) assertion set, based on the combinatorial and/or sequential logic elements associated with the FSM;
- model, for each of a plurality of clock cycles, the SMT assert set to determine a number of transitions to reach a desired state;
- and
- determine if a desired state of the FSM is reachable within a selected number of clock cycles.
Dependencies are inferred from the claim text.