Method and system for optimized automated case-splitting via constraints in a symbolic simulation framework

Abstract

A method for performing verification is proposed. The method comprises receiving a design and building an intermediate binary decision diagram for the design containing one or more nodal binary decision diagrams. In response to a size of the intermediate binary decision diagram exceeding a size threshold, a node of the design is selected for case-splitting. A first case-splitting is performed upon the selected node of the design to generate a primary constraint for setting the selected node to a primary value. A first constraining is performed on one of the one or more nodal binary decision diagrams with the primary constraint to generate a primary final binary decision diagram, a first verification of the design is performed using the primary final binary decision diagram.

1 . A system for performing verification, said system comprising: 
 means for receiving a design;    means for building an intermediate binary decision diagram for said design containing one or more nodal binary decision diagrams;    means for, in response to a size of said intermediate binary decision diagram exceeding a size threshold, selecting a node of said design for case-splitting;    means for first case-splitting upon said selected node of said design to generate a primary constraint for setting said selected node to a primary value, wherein said means for first case-splitting upon said selected node comprises means for first case-splitting upon said selected node of said design at an identified time step to generate said primary constraint for setting said determined node to said primary selected value;    means for first constraining one of said one or more nodal binary decision diagrams with said primary constraint to generate a primary final binary decision diagram; and    means for first performing verification of said design using said primary final binary decision diagram.    
   
   
       2 . The system of  claim 1 , further comprising: 
 means for second case-splitting upon said selected node of said design to generate a secondary constraint for setting said determined node to a secondary value;    means for second constraining said one of said one or more nodal binary decision diagrams with said secondary constraint to generate a secondary final binary decision diagram; and    means for second performing verification of said design using said secondary final binary decision diagram.    
   
   
       3 . The system of  claim 2 , wherein: 
 said means for selecting said node of said design for said first case-splitting further comprises means for selecting a set of multiple nodes of said design for said first case-splitting and said second case-splitting; and 
 said system further comprises means for repeating said first case-splitting, first constraining, first performing, second case-splitting, second constraining and second performing steps on each of said set of multiple nodes of said design.  
   
   
   
       4 . The system of  claim 1 , wherein: 
 said means for selecting said node of said design for said first case-splitting further comprises means for selecting a set of multiple nodes of said design for said first case splitting;    said system further comprises means for repeating said first case-splitting, said first constraining, and said first performing stepson each of said set of multiple nodes of said design.    
   
   
       5 . A system for performing verification, said system comprising: 
 means for receiving a design;    means for building an intermediate binary decision diagram for said design containing one or more nodal binary decision diagrams;    means for, in response to a size of said intermediate binary decision diagram exceeding a size threshold, selecting a node of said design for case-splitting;    means for first case-splitting upon said selected node of said design to generate a primary constraint for setting said selected node to a primary value;    means for first constraining one of said one or more nodal binary decision diagrams with said primary constraint to generate a primary final binary decision diagram; and    means for first performing verification of said design using said primary final binary decision diagram;    means for backtracking to a time step of a last case-split;    means for setting said selected node to a next constant; and    means for performing a symbolic analysis of said determined node with said next constant.    
   
   
       6 . The system of  claim 1 , wherein said means for building said intermediate binary decision diagram for said design further comprises: 
 means for combining one or more intermediate binary decision diagrams of one or more child nodes of said selected node;    means for determining that said intermediate binary decision diagram of said selected node is not valid;    means for, in response to determining that said intermediate binary decision diagram of said selected node is not valid, marking a splittable node;    means for setting said splittable node to a value;    means for obtaining one or more third binary decision diagrams by inverting said second binary decision diagrams;    means for storing said one or more third binary decision diagram on a stack;    means for constraining one or more second binary decision diagrams with an inverse of one or more of said one or more third binary decision diagram of said splittable node; and    means for constraining one or more fourth binary decision diagrams with a fifth binary decision diagram of said splittable node.    
   
   
       7 . The system of  claim 6 , further comprising: 
 means for retrieving said third binary decision diagrams said stack;    means for setting said splittable node to a next constant; and    means for performing symbolic analysis of said design with said next constant.    
   
   
       8 . A machine-readable medium having a plurality of instructions processable by a machine embodied therein, wherein said plurality of instructions, when processed by said machine, causes said machine to perform a method comprising: 
 receiving a design;    building an intermediate binary decision diagram for said design containing one or more nodal binary decision diagrams;    in response to a size of said intermediate binary decision diagram exceeding a size threshold, selecting a node of said design for case-splitting;    first case-splitting upon said selected node of said design to generate a primary constraint for setting said selected node to a primary value, wherein said first case-splitting upon said selected node comprises first case-splitting upon said selected node of said design at an identified time step to generate said primary constraint for setting said determined node to said primary selected value;    first constraining one of said one or more nodal binary decision diagrams with said primary constraint to generate a primary final binary decision diagram; and    first performing verification of said design using said primary final binary decision diagram.    
   
   
       9 . The machine-readable medium of  claim 8 , wherein said method further comprises: 
 second case-splitting upon said selected node of said design to generate a secondary constraint for setting said determined node to a secondary value;    second constraining said one of said one or more nodal binary decision diagrams with said secondary constraint to generate a secondary final binary decision diagram; and    second performing verification of said design using said secondary final binary decision diagram.    
   
   
       10 . The machine-readable medium of  claim 8 , wherein the processable instructions are deployed to a server from a remote location.  
   
   
       11 . The machine-readable medium of  claim 8 , wherein the processable instructions are provided by a service provider to a customer on an on-demand basis.  
   
   
       12 . A machine-readable medium having a plurality of instructions processable by a machine embodied therein, wherein said plurality of instructions, when processed by said machine, causes said machine to perform a method comprising: 
 receiving a design;    building an intermediate binary decision diagram for said design containing one or more nodal binary decision diagrams;    in response to a size of said intermediate binary decision diagram exceeding a size threshold, selecting a node of said design for case-splitting;    first case-splitting upon said selected node of said design to generate a primary constraint for setting said selected node to a primary value;    first constraining one of said one or more nodal binary decision diagrams with said primary constraint to generate a primary final binary decision diagram;    first performing verification of said design using said primary final binary decision diagram;    backtracking to a time step of a last case-split;    setting said selected node to a next constant; and    performing a symbolic analysis of said determined node with said next constant.    
   
   
       13 . The machine-readable medium of  claim 8 , wherein said step of building said intermediate binary decision diagram for said design further comprises: 
 combining one or more intermediate binary decision diagrams of one or more child nodes of said selected node;    determining that said intermediate binary decision diagram of said selected node is not valid;    in response to determining that said intermediate binary decision diagram of said selected node is not valid, marking a splittable node;    setting said splittable node to a value;    obtaining one or more third binary decision diagrams by inverting said second binary decision diagrams;    storing said one or more third binary decision diagram on a stack;    constraining one or more second binary decision diagrams with an inverse of one or more of said one or more third binary decision diagram of said splittable node; and    constraining one or more fourth binary decision diagrams with a fifth binary decision diagram of said splittable node.    
   
   
       14 . The machine-readable medium of  claim 13 , further comprising: 
 retrieving said third binary decision diagrams said stack;    setting said splittable node to a next constant; and    performing symbolic analysis of said design with said next constant.