Formal verification driven power modeling and design verification

Abstract

A computer-implemented method includes receiving a unit, wherein each unit includes one or more blocks. The computer-implemented method further includes selecting one or more input pins for each of said one or more blocks. The computer-implemented method further includes assigning a numerical value to each of said one or more input pins to yield at least one numerical sequence. The computer-implemented method further includes, for each numerical sequence of the at least one numerical sequence, performing a check on the numerical sequence to yield a number of fails. The computer-implemented method further includes determining a simulation condition for power modeling of the unit based on optimizing a numerical sequence with respect to the number of fails. The computer-implemented method further includes determining a number of design errors of the unit based on the simulation condition. A corresponding computer system and computer program product are also disclosed.

What is claimed is: 
     
         1 . A computer-implemented method comprising:
 receiving a unit, said unit comprising one or more blocks;   selecting one or more input pins for each of said one or more blocks;   assigning a numerical value to each of said one or more input pins to yield at least one numerical sequence;   for each numerical sequence of said at least one numerical sequence, performing a check on said numerical sequence to yield a number of fails;   determining a simulation condition for power modeling of said unit based on optimizing a numerical sequence with respect to said number of fails; and   determining a number of design errors of said unit based on said simulation condition.   
     
     
         2 . The computer-implemented method of  claim 1 , wherein said unit comprises register transfer level content. 
     
     
         3 . The computer-implemented method of  claim 2 , wherein said register transfer level content is expressed in a hardware description language. 
     
     
         4 . The computer-implemented method of  claim 1 , wherein said numerical value is either zero or one. 
     
     
         5 . The computer-implemented method of  claim 1 , wherein said check comprises formal verification of each of said one or more blocks based on said numerical sequence of said one or more input pins. 
     
     
         6 . The computer-implemented method of  claim 1 , wherein said number of fails comprises a count of errors in said numerical sequence of said one or more input pins. 
     
     
         7 . A computer program product, the computer program product comprising one or more computer readable storage media and program instructions stored on said one or more computer readable storage media, said program instructions comprising instructions to:
 receive a unit, said unit comprising one or more blocks;   select one or more input pins for each of said one or more blocks;   assign a numerical value to each of said one or more input pins to yield at least one numerical sequence;   for each numerical sequence of said at least one numerical sequence, perform a check on said numerical sequence to yield a number of fails;   determine a simulation condition for power modeling of said unit based on optimizing a numerical sequence with respect to said number of fails; and   determine a number of design errors of said unit based on said simulation condition.   
     
     
         8 . The computer program product of  claim 7 , wherein said unit comprises register transfer level content. 
     
     
         9 . The computer program product of  claim 8 , wherein said register transfer level content is expressed in a hardware description language. 
     
     
         10 . The computer program product of  claim 7 , wherein said numerical value is either zero or one. 
     
     
         11 . The computer program product of  claim 7 , wherein said check comprises formal verification of each of said one or more blocks based on said numerical sequence of said one or more input pins. 
     
     
         12 . The computer program product of  claim 7 , wherein said number of fails comprises a count of errors in said numerical sequence of said one or more input pins. 
     
     
         13 . A computer system, the computer system comprising:
 one or more computer processors;   one or more computer readable storage media;   computer program instructions;   said computer program instructions being stored on said one or more computer readable storage media;   said computer program instructions comprising instructions to:
 receive a unit, said unit comprising one or more blocks; 
 select one or more input pins for each of said one or more blocks; 
 assign a numerical value to each of said one or more input pins to yield at least one numerical sequence; 
 for each numerical sequence of said at least one numerical sequence, perform a check on said numerical sequence to yield a number of fails; 
 determine a simulation condition for power modeling of said unit based on optimizing a numerical sequence with respect to said number of fails; and 
 determine a number of design errors of said unit based on said simulation condition. 
   
     
     
         14 . The computer system of  claim 13 , wherein said unit comprises register transfer level content. 
     
     
         15 . The computer system of  claim 14 , wherein said register transfer level content is expressed in a hardware description language. 
     
     
         16 . The computer system of  claim 13 , wherein said numerical value is either zero or one. 
     
     
         17 . The computer system of  claim 13 , wherein said check comprises formal verification of each of said one or more blocks based on said numerical sequence of said one or more input pins. 
     
     
         18 . The computer system of  claim 13 , wherein said number of fails comprises a count of errors in said numerical sequence of said one or more input pins.