Intent-driven functional verification of digital designs

Abstract

Method and apparatus are provided for facilitating analysis of the intended behavior of a hardware design. According to one embodiment of the present invention, a language-based representation of a hardware design is received. Multiple design verification checks are generated for use in connection with model checking by applying a set of one or more predetermined properties to the language-based representation of the hardware design. Then, the hardware design, as implemented according to the language-based representation, is verified against intended behavior, represented by the set of one or more predetermined properties, by determining whether one or more of the design verification checks are violated by the hardware design. Finally, results of the verification may be reported.

What is claimed is:  
     
         1 . A method comprising: 
 receiving a language-based representation of a hardware design;    automatically generating a plurality of design verification checks for use in connection with model checking, the plurality of design verification checks based upon application of a set of one or more predetermined properties to the language-based representation of the hardware design;    verifying the hardware design, as implemented according to the language-based representation, against intended behavior, represented by the set of one or more predetermined properties, by determining whether one or more of the plurality of design verification checks are violated by the hardware design; and    reporting results of said verifying.    
     
     
         2 . The method of  claim 1 , wherein the language-based representation of the hardware design comprises Register Transfer Language (RTL) source code.  
     
     
         3 . The method of  claim 2 , wherein the one or more predetermined properties include a block enable property that relates to whether conditions enabling execution of a particular block of code in the RTL source code will never be satisfied.  
     
     
         4 . The method of  claim 2 , wherein the one or more predetermined properties include an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the RTL source code through assignment operations appearing in the RTL source code.  
     
     
         5 . The method of  claim 2 , wherein the one or more predetermined properties include a conflicting assignments property that relates to checking whether it is possible for a wire in the hardware design to be driven by multiple conflicting drivers.  
     
     
         6 . The method of  claim 2 , wherein the one or more predetermined properties include a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value.  
     
     
         7 . The method of  claim 2 , wherein the one or more predetermined properties include a constant value variable property that relates to determining whether a variable in the RTL source code will always hold a constant value.