Method and System for Enhanced Verification Through Structural Target Decomposition

Abstract

A method, system and computer program product for performing verification of an electronic design is disclosed. The method includes receiving a design, wherein the design includes a first target set and a first register set including one or more registers. A structural product extraction is formed from one or more targets from the first target set and the structural product extraction is recursed for one or more next-state functions of a subset of the one or more registers. A sum-of-products form is recursed from the structural product extraction for one or more next-state functions of a subset of the one or more registers and a product-of-sums form of a result of the second recursing is decomposed to generate a decomposition of the product-of-sums form. The decomposition of the product-of-sums form is synthesized into a second target set and a subset of the second target set to recursively decompose is chosen. In response to the subset of the second target set being nonempty, the first target set is recursively decomposed and, in response to the second target set being empty, verification is applied to the second target set.

1 . A system for performing verification of an electronic design, said system comprising: 
 means for receiving a design, wherein said design includes a first target set and a first register set comprising one or more registers;    means for forming a structural product extraction from one or more targets from said first target set;    means for first recursing said structural product extraction for one or more next-state functions of a subset of said one or more registers;    means for second recursing a sum-of-products form from said structural product extraction for one or more next-state functions of a subset of said one or more registers;    means for decomposing a product-of-sums form of a result of said second recursing to generate a decomposition of said product-of-sums form;    means for synthesizing said decomposition of said product-of-sums form into a second target set;    means for choosing a subset of said second target set to recursively decompose;    means for, in response to said subset of said second target set being nonempty, recursively decomposing said first target set; and    means for, in response to said second target set being empty, applying verification to said second target set.    
   
   
       2 . The system of  claim 1 , further comprising: 
 means for ascertaining that all targets of said subset of said second target set are unreachable; and    means for, in response to asecertaining that all targets of said subset of said second target set are unreachable, reporting an unreachability result of said first target set.    
   
   
       3 . The system of  claim 1 , further comprising: 
 means for ascertaining that a target from said subset of said second target set has been hit; and    means for, in response ascertaining that a target from said subset of said second target set has been hit, reporting a hit of said first target set.    
   
   
       4 . The system of  claim 1 , wherein: 
 said means for second recursing said sum-of-product form for one or more next-state functions of a subset of said one or more registers further comprises means for second recursing said sum of product form for one or more next-state functions of an arbitrarily-selected subset of said one or more registers appearing in support of said sum-of-product form by, for one of one or more selected registers in said one or more registers appearing in a third register set, appending a generated register with an initial value onto one or more recursively-obtained sum terms for a next state function of said one of said one or more selected registers in said one or more registers appearing in a third register set; and    said means for first recursing said structural product extraction for one or more next-state functions of a subset of said one or more registers further comprises means for first recursing said structural product extraction for one or more next-state functions of an arbitrarily-selected subset of said one or more registers appearing in support of said structural product extraction by:    for one of one or more selected registers in said one or more registers appearing in a second register set, appending a calculated register with a generated initial value equal to an initial value of said one of one or more selected registers in said one or more registers appearing in a second register set onto one or more recursively-obtained product terms for a next state function of said one of one or more selected registers in said one or more registers appearing in a second register set to generate one or more register-appended recursively-obtained product terms; and    replacing said second register set with said one or more register-appended recursively obtained product terms.    
   
   
       5 . The system of  claim 1 , wherein: 
 said means for synthesizing said decomposition of said product-of-sums form into a second target set, further comprises means for synthesizing said decomposition of said product-of-sums form into a second target set, using AND and OR gates for products and sums, respectively;    said means for identifying a sum-of-product form from said structural product extraction further comprises means for identifying a sum-of-product form from said structural product extraction using structural analysis; and    said means for identifying a product form of one or more targets from said first target set to form a structural product extraction further comprises identifying a product form of one or more targets from said first target set using structural analysis to form a structural product extraction.    
   
   
       6 . The system of  claim 1 , further comprising: 
 means for ascertaining that no targets of said subset of said second target set are hit, and that at least one unhit target of said subset of said second target set was not demonstrated to be unreachable; and    means for, in response to ascertaining that no targets of said subset of said second target set are hit, and that at least one unhit target of said subset of said second target set was not demonstrated to be unreachable, for one or more coverage metrics desired for said first target set, extracting a minimal value for one of said coverage metric across one or more subtargets of said subset of said second target set and reporting said minimal value for one of said coverage metric desired for said first target set.    
   
   
       7 . The system of  claim 1 , wherein said means for decomposing said product-of-sums form to generate said decomposition of said product-of-sums form further comprises: 
 means for choosing one or more decomposition criteria for said sum-of-product form; and    means for decomposing said product-of-sums form based upon said one or more decomposition criteria to generate a decomposition of said product-of-sums form.