Design verification using formal techniques

Abstract

Formal techniques are applied to industrial design problems such as verification of a circuit design. Initial decisions may include defining properties to verify the design. An abstraction of the design may be generated and model checking applied to the abstraction. Results obtained using these techniques may be extended by performance analysis and/or verification of sequential operations.

1 . A method of verifying a circuit design comprising: 
 generating a reduced model of a circuit design;    model checking the reduce model; and    conducting performance analysis on the reduced model to verify the circuit design.    
   
   
       2 . The method of  claim 1  wherein conducting performance analysis comprises modifying at least one property.  
   
   
       3 . The method of  claim 2  wherein conducting performance analysis comprises applying the modified at least one property to the reduced model.  
   
   
       4 . The method of  claim 1  wherein conducting performance analysis comprises identifying at least one performance margin.  
   
   
       5 . The method of  claim 1  wherein conducting performance analysis comprises identifying at least one worst case condition.  
   
   
       6 . The method of  claim 1  comprising generating at least one performance analysis result and applying the at least one performance analysis result to the circuit design to verify the circuit design.  
   
   
       7 . The method of  claim 1  comprising identifying at least one margin associated with a learn operation.  
   
   
       8 . The method of  claim 1  comprising identifying at least one margin associated with a lookup operation.  
   
   
       9 . The method of  claim 1  comprising identifying at least one margin associated with an aging operation.  
   
   
       10 . The method of  claim 1  wherein generating a reduced model comprises applying induction to the circuit design.  
   
   
       11 . The method of  claim 1  wherein generating a reduced model comprises reducing a size of a table.  
   
   
       12 . The method of  claim 1  wherein generating a reduced model comprises reducing a size of an address.  
   
   
       13 . The method of  claim 1  wherein generating a reduced model comprises reducing a number of ports.  
   
   
       14 . The method of  claim 1  wherein generating a reduced model comprises ignoring sequential operations.  
   
   
       15 . The method of  claim 1  wherein model checking comprises generating properties associated with the circuit design.  
   
   
       16 . The method of  claim 15  wherein each of the properties is used to verify a unique RTL function.  
   
   
       17 . A method of verifying a circuit design comprising: 
 generating a reduced model of a circuit design;    model checking the reduce model; and    generating at least one model of a sequential operation of the circuit design; and    applying the at least one model to the reduced model to verify the circuit design.    
   
   
       18 . The method of  claim 17  wherein generating at least one model comprises defining a set of internal states comprising initial states and residual states.  
   
   
       19 . The method of  claim 18  wherein generating at least one model comprises defining subsets of the set of internal states.  
   
   
       20 . The method of  claim 19  wherein generating at least one model comprises defining projections of the subsets on internal registers.  
   
   
       21 . The method of  claim 19  wherein applying the at least one model comprises applying the subsets to the reduced model.  
   
   
       22 . The method of  claim 17  wherein the sequential operation comprises a request.  
   
   
       23 . The method of  claim 17  wherein generating a reduced model comprises applying induction to the circuit design.  
   
   
       24 . The method of  claim 17  wherein generating a reduced model comprises reducing a size of a table.  
   
   
       25 . The method of  claim 17  wherein generating a reduced model comprises reducing a size of an address.  
   
   
       26 . The method of  claim 17  wherein generating a reduced model comprises reducing a number of ports.  
   
   
       27 . The method of  claim 17  wherein generating a reduced model comprises ignoring sequential operations.  
   
   
       28 . The method of  claim 17  wherein model checking comprises generating properties associated with the circuit design.  
   
   
       29 . The method of  claim 28  wherein each of the properties is used to verify a unique RTL function.