Abstract:
A method for formally verifying a hardware/software co-design includes providing in a co-design, a first model, and a second model, the first model is one of a hardware model, and the second model is one of a software model, or vice versa, providing a safety property expected to be satisfied by the co-design, combining an abstraction of the first model and the safety property to obtain an abstracted first model, composing the abstracted first model and the second model to obtain a composed model, checking if the composed model satisfies the safety property, and signaling that the hardware/software co-design violates the safety property if the safety property is violated in the composed model.

Description:
BACKGROUND 
       [0001]    The present invention relates to a formal verification of hardware and software co-designs such as embedded systems. 
         [0002]    In general, formal verification of hardware and software designs in the design phase is customary. It is standard to use formal verification in validating complex hardware designs based on a hardware model described in a hardware description language. Further, the importance of software verification has recently increased as software codes are getting more and more complex. 
       SUMMARY 
       [0003]    According to a first aspect a computer implemented method for formally verifying a hardware/software co-design is provided, including the steps of: providing a co-design including a first model and a second model, the first model is one of a hardware model and a software model, and the second model is the other one of the hardware model and the software model, providing a safety property expected to be satisfied by the co-design, combining an abstraction of the first model and the safety property to obtain an abstracted first model, composing the abstracted first model and the second model to obtain a composed model, checking if the composed model satisfies the safety property, and signaling that the hardware/software co-design violates the safety property if the safety property is violated in the composed model. 
         [0004]    According to a further aspect, a computer implemented method for formally verifying a hardware/software co-design is provided, including the steps of: providing in a co-design a first model and a second model, the first model is one of a hardware model and a software model, and the second model is the other one of the hardware model and the software model, providing a safety property expected to be satisfied by the co-design, combining an abstraction of the first model and the safety property to obtain an abstracted first model, generating an abstracted second model, composing the abstracted first model and the abstracted second model to obtain a composed model, checking if the composed model satisfies the safety property, and signaling that the hardware/software co-design violates the safety property if the safety property is violated in the composed model. 
         [0005]    Hardware/software co-designed systems may be decomposed in a hardware component described as a hardware (first/second) model and a software component described as a software (first/second) model. In a verification process, the hardware and the software models of a hardware/software co-design are verified with respect to a safety property to be proved. 
         [0006]    As a means for refinement (abstraction), an interpolation-based transition relation abstraction and refinement may be applied. 
         [0007]    One general approach may include performing model checking of the composed hardware and software models. Given the complexity of designs of hardware and software, the verification of the composed hardware and software models may be complicated and therefore time-consuming and requires high performance verification computing resources. One advantage of the above methods may be that model checking of the composed concrete (non-abstracted) hardware and (non-abstracted) software model is avoided. According to the above method model checking may only be performed on a composed model in which at least one of a hardware model or a software model is abstracted using the transitional relation abstraction. Hence, the verification time for complex hardware/software co-design may be essentially reduced. 
         [0008]    Furthermore, the abstractions of the first model and the second model may be refined, particularly to a lower abstraction level/less abstracted level, as long as the composed model does not satisfy the safety property, the steps of composing the abstracted first model and the second model and of checking if the composed model satisfies the safety property are performed based on the refined first model and the refined second model, respectively. 
         [0009]    It may be provided that the abstractions of the first model and the second model are refined, as long as the error trace resulting from the step of checking in a model checker is not real trace in the non-abstracted first model and non-abstracted second model, respectively. 
         [0010]    Particularly, the abstraction of the first model is refined, as long as the error trace resulting from the step of checking in a model checker is not real. 
         [0011]    According to an embodiment refining may be performed by means of interpolation, particularly Craig interpolation. 
         [0012]    It may be provided that the model checker provides a counterexample resulting from the step of checking, where signaling that the co-design violates the safety property is performed only if the counterexample projected on the non-abstracted first model and the non-abstracted second model is a valid trace in the first model and the second model, respectively. 
         [0013]    It may be checked if the counterexample projected on the non-abstracted first model and the non-abstracted second model is a valid trace in the first model and the second model, respectively, is performed using a SAT solver. 
         [0014]    Furthermore, the hardware model may be described by a hardware-centric language, particularly by a hardware description language. 
         [0015]    The software model may be described by a software-centric language, particularly by a programming language. 
         [0016]    Alternatively or additionally, composing the abstracted first model and the second model may comprise translating the abstracted first model and the safety property into a property specification language which is capable to describe a model environment and properties and by performing a model check using the environment described in a property specification language for the verification of the abstracted or non-abstracted second model, respectively. 
         [0017]    According to a further aspect a system for formal verification of a hardware/software co-design is provided, configured to perform any of the methods described above. 
     
    
     
       BRIEF DESCRIPTION OF THE DRAWINGS 
         [0018]    Embodiments of the present invention are described in more detail in conjunction with the accompanying drawings in which: 
           [0019]      FIG. 1  is an illustration of a hardware/software co-design coupled with an interface to establish a communication between the models, according to an embodiment of the present disclosure; 
           [0020]      FIG. 2  is a flowchart illustrating a method for formal verification of hardware/software co-designs, according to an embodiment of the present disclosure; 
           [0021]      FIG. 3  is an illustration of a resolution refutation of an exemplary CNF formula, according to an embodiment of the present disclosure; 
           [0022]      FIG. 4  is a flowchart illustrating a first alternate method for formal verification of hardware/software co-designs, according to an embodiment of the present disclosure; 
           [0023]      FIG. 5  is a flowchart illustrating a second alternate method for formal verification of hardware/software co-designs, according to an embodiment of the present disclosure; and 
           [0024]      FIG. 6  is a diagram illustrating components of a system for executing the methods illustrated in  FIGS. 2, 4 and 5 , according to an embodiment of the present disclosure. 
       
    
    
       [0025]    The drawings are not necessarily to scale. The drawings are merely schematic representations, not intended to portray specific parameters of the invention. The drawings are intended to depict only typical embodiments of the invention. In the drawings, like numbering represents like elements. 
       DETAILED DESCRIPTION 
       [0026]    Detailed embodiments of the claimed structures and methods are disclosed herein; however, it can be understood that the disclosed embodiments are merely illustrative of the claimed structures and methods that may be embodied in various forms. This invention may, however, be embodied in many different forms and should not be construed as limited to the exemplary embodiments set forth herein. Rather, these exemplary embodiments are provided so that this disclosure will be thorough and complete and will fully convey the scope of this invention to those skilled in the art. In the description, details of well-known features and techniques may be omitted to avoid unnecessarily obscuring the presented embodiments. 
         [0027]    The present invention relates to a formal verification of hardware and software co-designs such as embedded systems. 
         [0028]    A growing problem in hardware/software verification is the combined verification of co-designs of hardware including hardware-specific software (firmware) that interacts with it. The results of separately applying techniques for the formal verification of hardware and software are not satisfying. The hardware/software interface usually acts as a boundary which needs to be synchronized. However, such a synchronization may not be reflected in separate hardware and software verification attempts. Furthermore, the interfaces are usually described in different description languages for hardware and software verification, while the consistency of the semantics of the descriptions of the interfaces is usually not approved. In general, the interaction of hardware interfaces with software interfaces for embedded systems is so complex that validation of the co-design by verifying the hardware and software interfaces separately may not lead to reliable results. A common approach to designing embedded software uses a software-modelled hardware in which the software code may be developed, validated and tested. 
         [0029]    Embedded systems may typically include a hardware component in which a hardware-specific software code (firmware) is carried out. When designing such an embedded system, the hardware component may be described in a hardware-centric language such as a hardware description language (HDL), e.g. VHSIC HDL (Very High Speed Integrated Circuit Hardware Description Language) which may be verified by tools such as RuleBase SixthSense and the like. The hardware-centric language description may include the functions of the hardware component (hardware design) of the embedded system in the form of a hardware model as a part of the system model for which formal verification may be performed. 
         [0030]    A software program code may be encoded in a software-centric language. The software program code may be written in any known programming language including, for example, C++. 
         [0031]    Hardware components and software interact with each other via one or more interfaces (hereinafter “interfaces”). In the common approach of separate verification of the hardware design (hardware model) and the software code (software model), the interfaces may be provided as models in both the hardware description language and the programming language. This may result in an inconsistency. 
         [0032]    Therefore, by performing a verification of a hardware model and a software model in a combined manner, embodiments of the present disclosure may, among other potential benefits, allow a natural decomposition of the co-design system. As such, the present embodiment has the capacity to avoid the state-space explosion problem typical in current hardware/software systems. 
         [0033]    Referring now to  FIG. 1 , a hardware/software co-design coupled with an interface to establish a communication between models is shown, according to an embodiment of the present disclosure. In general, the hardware/software co-design may include a software model, a hardware model, and interface models to establish a communication between the models. The interface models may include a software interface model and a hardware interface model. The software model sw and the software interface model Inter sw  may be regarded as an environment of the hardware and translated into Property Specification Language (PSL). The PSL may be typical and well known to those skilled in the art and it may be used to describe the environment and its properties. By means of the PSL a conventional model checker, like RuleBase may perform composition of the hardware and software models. As a result, a common PSL test bench may contain the software code sw=&lt;P sw , Inter sw &gt; modelled in PSL which forms the environment for the hardware. The abstraction may be given as: 
         [0000]                =( {circumflex over (P)}   sw ,Inter sw ) 
         [0034]    Model checkers like RuleBase may use information from a restricted PSL environment to automatically reduce/abstract the size of the model to be verified, i.e. the composition is taken care of automatically in the model checker. To help abstractions, some signals in the environment may be set to constant values, or may be restricted to some other simple behavior. This reduction is usually done by using vmodes which is a construct in PSL. The safety property φ to be verified may also be modeled in PSL using assertions. 
         [0035]    Hardware model checkers, including RuleBase, may use/compose the environment described in the PSL test bench, the hardware model and check the safety property specified in PSL. The model checking may be performed (e.g. step S 5  in  FIG. 2 ) to approve if the composed hardware and software model fulfill the given safety property, and it may return a corresponding YES/NO answer and a counterexample c in case of a failure (NO) as will be described in detail below. A counterexample c may be described using the variables of the abstracted software model          , i.e. {circumflex over (P)} sw  and the software interface Inter sw  and the hardware hw. 
         [0036]    The counterexample c may be described using the variables of the software model          , i.e. {circumflex over (P)} sw  and the software interface model Inter sw  and the hardware model hw. The counterexample may be either projected on the variables of P hw  or P sw  and Inter sw  and simulated on the same. 
         [0037]    Referring now to  FIG. 2 , a flowchart  200  describing the steps of a method for formal verification of hardware/software co-designs is shown, according to one embodiment of the present disclosure. In this embodiment, a hardware model described in a hardware centric language, e.g. in HDL, and a software model described in a common software-centric language are further specified. 
         [0038]    In step S 1 , the hardware model and the software model may be provided in respective description languages. The hardware model may be described or be translated (by the model checker) into the following representation: 
         [0000]        hw =( I   hw   ,T   hw ) 
         [0039]    where I hw  defines a set of initial states of the hardware model and T hw  a transition relation starting from I hw . 
         [0040]    Furthermore, the software model may be described as: 
         [0000]        sw =( I   sw   ,T   sw ) 
         [0041]    where I sw  defines the set of initial states of the software and T sw  the transition relation starting from I sw . 
         [0042]    In step S 2 , a software abstraction may be created from the software model sw being defined as: 
         [0000]                =( I   sw   ,{circumflex over (T)}   sw ) 
         [0043]    with {circumflex over (T)} sw =TRUE to begin with, where {circumflex over (T)} sw  is defined as the abstracted transition relations. 
         [0044]    In step S 3 , a safety property φ may be specified or provided. The safety property φ may define the conditions which should be satisfied by the combined hardware/software model. The safety property φ is usually defined e.g. by an expert so that design flaws may be revealed. 
         [0045]    In step S 4 , the hardware model HW and the abstracted software model           may be composed. More specifically, the hardware model and the abstracted software model may be analyzed in a combined manner so that it is possible to check if the combined hardware/software model satisfies the safety property φ. 
         [0046]    If in step S 5  of model checking it is found that the composed hardware and software models fulfill the safety property (alternative: Yes), it is signaled in step S 6  that also the composition of the hardware model and the non-abstracted software model fulfill the safety property as: 
         [0000]    
       
      
       hw∥ 
               
       =φ→hw∥sw=φ 
      
     
         [0047]    Thereafter, the method is continued by step S 3 . 
         [0048]    Otherwise (alternative: No), it has to be further checked whether or not the counterexample/error trace returned by the model checker is a concrete/real error trace, i.e., if the error trace is due to the abstraction of the software and the method continues to step S 7 . 
         [0049]    In step S 7 , the counterexample c is projected on the (non-abstracted) software model sw by restricting the state description in c to variables of sw=(I sw , T sw ). In consequence, a sequence of software states as a counterexample projection c sw  may be obtained: 
         [0000]        c   sw   =s   0   ,s   1   ,s   2   , . . . ,s   k . 
         [0050]    It is checked in step S 8 , if the counterexample projection c sw  of the counter-example c on the software model sw provides a valid trace in the software. This may be performed by simulating c sw  on the software using a standard SAT solver as known in the art. 
         [0051]    SAT solvers are known for resolving Boolean satisfiability problems which are decision problem for determining if a satisfying assignment for a given Boolean formula exists. 
         [0052]    A Boolean formula may be generally converted to Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF). A propositional formula is in CNF if it is a conjunction of disjunctions of literals (x′ or x″ where x′, x″ are Boolean disjunctive clauses). For example, the CNF formula: 
         [0000]      ( x   1               x     2 )         ( x   3             x   2 )             x     3               x     1    
         [0053]    In the above formula, x 1             x   2 , x 3            x 2 ,  x   3 ,  x   1  are Boolean clauses. When a Boolean formula is unsatisfiable, most SAT solvers may generate a proof demonstrating its unsatisfiability. The proof may be represented as a counterexample. 
         [0054]    If the condition of step S 8  is fulfilled (alternative: YES), the counter-example c is a concrete error trace in the hardware/software co-design. This outcome leads to a signaling that the safety property is not satisfiable in step S 9  and to a stop of the method. 
         [0055]    Otherwise (alternative: NO), the abstraction {circumflex over (T)} sw  leads to refining in step S 10 . Step S 10  provides to strengthen the abstraction of the software model as a try to eliminate the error trace revealed by the counterexample. 
         [0056]    The refining might be performed by using Craig interpolation. 
         [0057]    Assume that s k ′(k′) is the first invalid state reached in the software model sw. The SAT solver can be used to return refutation proof demonstrating the unsatisfiability of the following formula: 
         [0000]    
       
         
           
             
               BMC 
               k 
             
              
             
               = 
               def 
             
              
             
               
                 I 
                  
                 
                   ( 
                   0 
                   ) 
                 
               
                
               
                 
                   T 
                   sw 
                 
                  
                 
                   ( 
                   
                     0 
                     , 
                     1 
                   
                   ) 
                 
               
                
               
                 
                   T 
                   sw 
                 
                  
                 
                   ( 
                   
                     1 
                     , 
                     2 
                   
                   ) 
                 
               
                
               
                   
               
                
               … 
                
               
                   
               
                
               
                 
                   T 
                   sw 
                 
                  
                 
                   ( 
                   
                     
                       
                         k 
                         ′ 
                       
                       - 
                       1 
                     
                     , 
                     
                       k 
                       ′ 
                     
                   
                   ) 
                 
               
                
               
                 
                   s 
                   
                     k 
                     ′ 
                   
                 
                  
                 
                   ( 
                   
                     k 
                     ′ 
                   
                   ) 
                 
               
             
           
         
       
     
         [0058]    The refutation proof can be used to refine the abstraction of the software model using interpolation. 
         [0059]    Craig Interpolation is well known in the art. Given a propositional formula β, let Var(β) denote the set of propositional variables occurring in β. 
         [0060]    As is defined, an interpolant for a pair of inconsistent propositional formulas (A;B) is a propositional formula I such that: 
         [0061]    1. A→I, 
         [0062]    2. I and B are inconsistent, and 
         [0063]    3. Var(I) ⊂ Var(A)∩Var(B). 
         [0064]    As an example, it is given an unsatisfiable propositional formula A         B such that A=(x 1             x   2 ) and B=(x 3           x 2 )           x   3 . The interpolant for the unsatisfiable pair (A;B) is: x   2 . Simplifying A and B, A=( x   1             x   2 ) and B=( x   2             x   3 ), it can be seen that A→ x   2  is valid and B           x   2  is false. 
         [0065]    Interpolants may be computed efficiently from resolution refutations. Different methods to compute interpolants from proofs are known in the art. 
         [0066]    Herein a slightly extended notion of interpolation is used. Given an indexed set of formulas A=a 1 ; a 2 ; . . . ; an such that          A is unsatisfiable, a symmetric interpolant for A is an indexed set of formulas Â=         ;          ; . . . ;           such that a i →         ; and                               . . .                    =         Â is unsatisfiable. Moreover,          ; is over the common variables in a i  and A\a i . 
         [0067]    In particular, the interpolants are completed between the following pairs: 
         [0000]    
       
         
               
               
               
             
           
               
                   
               
               
                 Interpolant 
                 A 
                 B 
               
               
                   
               
             
             
               
                 {circumflex over (T)} SW  (0, 1) 
                 T SW  (0, 1) 
                 I(0)            T SW (1, 2)            . . .            T SW   
               
               
                   
                   
                 (k′ − 1, k′)            s k′ (k′) 
               
               
                 {circumflex over (T)} SW  (1, 2) 
                 T SW  (1, 2) 
                 I(0)            T SW (0, 1)            . . .            T SW   
               
               
                   
                   
                 (k′ − 1, k′)            s k′ (k′) 
               
               
                 . 
                   
                   
               
               
                 . 
                   
                   
               
               
                 . 
                   
                   
               
               
                 {circumflex over (T)} SW  (k′ − 1, k′) 
                 T SW  (k′ − 1, k′) 
                 I(0)            T SW (0, 1)            . . .            T SW   
               
               
                   
                   
                 (k′ − 2, k′ − 1)            s k′ (k′) 
               
               
                   
               
             
          
         
       
     
         [0068]    The interpolants are shifted in time so that all interpolants are over variables of timeframe  0  and  1 . Thus, the transition relation is: 
         [0000]    
       
         
           
             
               
                 T 
                 . 
               
               sw 
             
             = 
             
               
                 
                    
                   
                     i 
                     = 
                     
                       k 
                       ′ 
                     
                   
                 
                 
                   i 
                   = 
                   0 
                 
               
                
               
                 
                   
                     T 
                     ^ 
                   
                    
                   
                     ( 
                     
                       i 
                       , 
                       
                         i 
                         + 
                         1 
                       
                     
                     ) 
                   
                 
                 i 
               
             
           
         
       
     
         [0069]    where i corresponds to the number of time steps by which the interpolant I is shifted. 
         [0070]    From the properties of symmetric interpolants, it is known that {dot over (T)} sw  admits no path of length k′ to sk′. The refined transition relation of           is: 
         [0000]    
       
      
       {circumflex over (T)} 
       sw 
       ={circumflex over (T)} 
       sw 
               
       {dot over (T)} 
       sw  
      
     
         [0071]    A more detailed explanation for the abstraction, the creation of the error trace simulation and the strengthening of the abstracted software model is given using a simple example. A software model having the following transition relation is given as follows: 
         [0072]    y=x 
         [0073]    z=y 
         [0074]    assert(x=z) 
         [0075]    with the transition relations y1→x0 and z1→y1. 
         [0076]    The transition relations may be abstracted, e.g. by a true *-function, where any variable can take any value. The possible counterexample c may be 
         [0000]    
       
         
           
             
               
                 
                   
                     x 
                      
                     
                         
                     
                      
                     0 
                   
                   = 
                   5 
                 
               
               
                 
                     
                 
               
               
                 
                   
                     y 
                      
                     
                         
                     
                      
                     1 
                   
                    
                   
                     = 
                     * 
                   
                 
               
             
             
               
                 
                   
                     y 
                      
                     
                         
                     
                      
                     0 
                   
                    
                   
                     = 
                     * 
                   
                 
               
               
                 → 
               
               
                 
                   
                     z 
                      
                     
                         
                     
                      
                     1 
                   
                   = 
                   7 
                 
               
             
             
               
                 
                   
                     z 
                      
                     
                         
                     
                      
                     0 
                   
                    
                   
                     = 
                     * 
                   
                 
               
               
                 
                     
                 
               
               
                 
                   
                     x 
                      
                     
                         
                     
                      
                     1 
                   
                    
                   
                     = 
                     * 
                   
                 
               
             
           
         
       
     
         [0077]    Now the counter-example is simulated on the original transition relation as given above: 
         [0000]        x   0 =5           y   1   =x   0             z   1   =y   1             z   1 =7 
         [0078]    where it is checked if the above formula is unsatisfiable. If it is unsatisfiable indicating that the counterexample is not a real execution trace in the original software model. 
         [0079]    The abstraction needs to be strengthened/refined to eliminate the counterexample. One possible way to strengthen the transition relation is using interpolation. As explained before. 
         [0000]    
       
         
           
             
               
                 
                   x 
                   0 
                 
                 = 
                 
                   
                     5 
                      
                     
                       y 
                       1 
                     
                   
                   = 
                   
                     x 
                     0 
                   
                 
               
               
                  
                 A 
               
             
              
             
               
                 
                   z 
                   1 
                 
                 = 
                 
                   
                     
                       y 
                       1 
                     
                      
                     
                       z 
                       1 
                     
                   
                   = 
                   7 
                 
               
               
                  
                 B 
               
             
           
         
       
     
         [0080]    An interpolant is formula I 
         [0081]    1. A→I, 
         [0082]    2. B         I→⊥ 
         [0083]    One possible interpolant is z1=x0 
         [0084]    y 1 =x 0           z 1 =y 1 →z 1 =x 0    
         [0085]    z 1 =x 0           x 0 =5         z 1 =7→⊥ 
         [0086]    Hence, the strengthened transition relation can be found as z 1 =x 0 . In the new strengthened system, the assertion assert (x=z) is never violated. The assignment y=x is abstracted away. 
         [0087]    Referring now to  FIG. 3 , a resolution refutation of the previously described CNF formula including a directed acyclic graph is shown, according to an embodiment of the present disclosure. The internal vertices are generated according to the resolution principle an assignment satisfying the Boolean clauses                    x and                      x  also satisfies                              . For example, the resolvent of          =(x 1             x   2 ) and          =x 3           x 2  is x 1           x 2 . The sink of a resolution refutation is an empty clause, denoted by □. 
         [0088]    Particularly, to check if a counterexample is a real trace in sw the satisfiability of the following formula is checked: 
         [0000]    
       
         
           
             
               BMC 
               k 
             
              
             
               = 
               def 
             
              
             
               
                 I 
                  
                 
                   ( 
                   0 
                   ) 
                 
               
                
               
                 
                   T 
                   sw 
                 
                  
                 
                   ( 
                   
                     0 
                     , 
                     1 
                   
                   ) 
                 
               
                
               
                 
                   T 
                   sw 
                 
                  
                 
                   ( 
                   
                     1 
                     , 
                     2 
                   
                   ) 
                 
               
                
               
                   
               
                
               … 
                
               
                   
               
                
               
                 
                   T 
                   sw 
                 
                  
                 
                   ( 
                   
                     
                       k 
                       - 
                       1 
                     
                     , 
                     k 
                   
                   ) 
                 
               
                
               
                 
                   s 
                   0 
                 
                  
                 
                   ( 
                   0 
                   ) 
                 
               
                
               
                   
               
                
               … 
                
               
                   
               
                
               
                 
                   s 
                   k 
                 
                  
                 
                   ( 
                   k 
                   ) 
                 
               
             
           
         
       
     
         [0089]    where BMC corresponds to a Bounded Model Checking. 
         [0090]    Bounded Model Checking (BMC) leverages the success of fast propositional SAT solvers to model checking. The basic idea behind verifying a system M using Bounded Model Checking is to check if there exists a trace in the system M of a bounded length k that reaches a faulty state. 
         [0091]    In detail, consider a set of states Q, a transition relation T, a set of failure states F, and a constant k≧1. A Bounded Model Checking instance BMC k  from a state Q with bound k checks if Q reaches F in k steps. The corresponding formula BMC k  may be defined as follows: 
         [0000]    
       
         
           
             
               BMC 
               k 
             
              
             
               = 
               def 
             
              
             
               
                 
                   Q 
                    
                   
                     ( 
                     
                       s 
                       0 
                     
                     ) 
                   
                 
                  
                 
                   T 
                    
                   
                       
                   
                    
                   
                     ( 
                     
                       
                         s 
                         0 
                       
                       , 
                       
                         s 
                         1 
                       
                     
                     ) 
                   
                 
                  
                 
                   T 
                    
                   
                       
                   
                    
                   
                     ( 
                     
                       
                         s 
                         1 
                       
                       , 
                       
                         s 
                         2 
                       
                     
                     ) 
                   
                 
                  
                 
                     
                 
                  
                 … 
                  
                 
                     
                 
                  
                 
                   T 
                    
                   
                       
                   
                    
                   
                     ( 
                     
                       
                         s 
                         
                           k 
                           - 
                           1 
                         
                       
                       , 
                       
                         s 
                         k 
                       
                     
                     ) 
                   
                 
                  
                 
                   F 
                    
                   
                     ( 
                     
                       s 
                       1 
                     
                     ) 
                   
                 
               
                
               
                   
               
                
               
                   
               
                
               … 
                
               
                   
               
                
               
                 F 
                  
                 
                   ( 
                   
                     s 
                     k 
                   
                   ) 
                 
               
             
           
         
       
     
         [0092]    If the BMC k  instance is satisfiable, F is reachable from a state in Q in k steps. If BMC k  is unsatisfiable, F is not reachable from a state in Q in ≦k steps. An instance of the BMC problem, denoted as BMC k (M;f) where f is a formal property (F=:f), checks if M           k φ where            k  is the satisfaction relation from the initial states of M up to bounded depth k. 
         [0093]    To check the satisfiability of BMC k , fast propositional SAT solvers are used for which BMC k  is converted into an equisatisfiable CNF formula. 
         [0094]    Referring now to  FIG. 4 , a flowchart  400  describing the steps of a first alternate method for formal verification of hardware/software co-designs is shown, according to an embodiment of the present disclosure. 
         [0095]    It should be noted that the method described above with reference to  FIG. 2  is described with the software model being abstracted and composed with the hardware model. In this embodiment, the hardware model is abstracted and composed with a non-abstracted software model, as described in the flowchart  400 . Hence, steps S 2 ′, S 4 ′, S 5 ′, S 7 ′, S 8 ′, and S 10 ′ differ from the corresponding steps S 2 , S 4 , S 7 , S 8 , and S 10  of the embodiment described in  FIG. 2 . 
         [0096]    In step S 1 , the hardware model and the software model are provided in respective description languages. Then, at step S 2 ′, an abstraction on the hardware model is performed. 
         [0097]    In step S 3 , a safety property φ is specified or provided. The safety property φ may define the conditions which should be satisfied by the combined hardware/software model as described above. 
         [0098]    In step S 4 ′, the software model sw and the abstracted hardware model           may be composed. More specifically, the software model and the abstracted hardware model may be analyzed in a combined manner so that it is possible to check if the combined hardware/software model satisfies the safety property φ. 
         [0099]    If in step S 5 ′ of model checking it is found that the composed hardware and software models fulfill the safety property (alternative: Yes), it is signaled in step S 6  that also the composition of the software model and the non-abstracted hardware model fulfill the safety property. Thereafter, the method is continued by step S 3 . 
         [0100]    Otherwise (alternative: No), it has to be further checked whether or not the counterexample/error trace returned by the model checker is a concrete/real error trace, i.e., if the error trace is due to the abstraction of the hardware and the method continues to step ST. 
         [0101]    In step S 7 ′, the counterexample c is projected on the (non-abstracted) hardware model hw by restricting the state description in c to variables of hw. 
         [0102]    Next, if the condition of step S 8 ′ is fulfilled (alternative: YES), the counter-example c is a concrete error trace in the hardware/software co-design. This outcome leads to a signaling that the safety property is not satisfiable in step S 9  and to a stop of the method. 
         [0103]    Otherwise (alternative: NO), the abstraction {circumflex over (T)} bw  leads to refining in step S 10 ′. 
         [0104]    Referring now to  FIG. 5 , a flowchart  500  describing the steps of an alternate method for formal verification of a hardware/software co-design is shown, according to an embodiment of the present disclosure. More specifically, the present embodiment may combine the described methods of  FIG. 2  and  FIG. 4  by using an abstracted hardware model and an abstracted software model. In an amended step S 2 ″ similar to steps S 2  ( FIG. 2 ) and S 2 ″ ( FIG. 4 ) of previously described embodiments an initial abstraction of the software model sw and the hardware model hw is performed. 
         [0105]    In the amended step S 4 ″, similar to step S 4  the abstracted hardware model           and the abstracted software model           are composed, i.e. the abstracted hardware model           and the abstracted software model           are combined or analyzed in a combined manner so that it is possible to check if the combined abstracted hardware/software model satisfies the safety property φ, as follows: 
         [0000]                ∥         =φ
 
         [0106]    If in amended step S 5 ″ (similar to steps S 5  and S 5 ′ in  FIGS. 2 and 4 , respectively) of model checking it is found that the composed abstracted hardware and abstracted software models fulfill the safety property (alternative: Yes), it is signaled in step S 6  that the composition of the non-abstracted hardware model and the non-abstracted software model fulfill the safety property as: 
         [0000]                ∥         =φ→ hw∥sw=φ 
 
         [0107]    Steps S 7  and S 8  are similar to the corresponding steps of the embodiment of  FIG. 2 . 
         [0108]    If the condition of step S 8  is fulfilled (alternative: YES), it has turned out that the counter-example c is a concrete error trace in the software model. This outcome leads to a continuation of the method in step S 11 . 
         [0109]    Otherwise (alternative: NO), the abstraction {circumflex over (T)} sw  of the software model sw leads to refining in step S 10 ″. Step S 10 ″ provides to strengthen the abstraction of the software model as to eliminate the error trace revealed by the counterexample. Thereafter the method is continued by step S 11 . 
         [0110]    In step S 11  (similar to the step S 7 ′ of the embodiment of  FIG. 4 ), the counterexample c is projected on the (non-abstracted) hardware model hw by determining the states of the hardware by applying c in hw=(I hw , T hw ). One obtains the a number of hardware states as a counterexample projection c hw : 
         [0000]        C   hw   =s′   0   ,s′   1   ,s′   2   , . . . ,s′   k . 
         [0111]    It is checked in step S 12 , if the counterexample projection c hw  of the counter-example c on the hardware model hw provides a valid trace in the hardware. This may be performed by a standard SAT solver as known in the art. 
         [0112]    If the condition of step S 12  is fulfilled (alternative: YES), it has turned out that the counter-example c is a concrete error trace in the hardware module. This outcome leads to a signaling that the safety property is not satisfiable in step S 13  and to a stop of the method. 
         [0113]    Otherwise (alternative: NO), the abstraction {circumflex over (T)} hw  leads to refining in step S 14 . Step S 14  provides to strengthen the abstraction of the hardware model (as a try) to eliminate the error trace revealed by the counterexample. Then, the method is continued with step S 4 ″. 
         [0114]    The present invention may be a system, a method, and/or a computer program product. The computer program product may include a computer readable storage medium (or media) having computer readable program instructions thereon for causing a processor to carry out aspects of the present invention. 
         [0115]    Referring now to  FIG. 6 , computing device  500  includes processor(s)  520 , memory  510 , tangible storage device(s)  530 , network interface(s)  540 , and I/O (input/output) interface(s)  550 . In  FIG. 6 , communications among the above mentioned components of computing device  500  are denoted by numeral  590 . Memory  510  includes ROM(s) (Read Only Memory)  511 , RAM(s) (Random Access Memory)  513 , and cache(s)  515 . 
         [0116]    One or more operating systems  531  and one or more computer programs  533  reside on one or more computer readable tangible storage device(s)  530 . In the exemplary embodiment, the computer implemented method for formally verifying a hardware/software co-design in form of a software resides on one or more computer-readable tangible storage device(s)  530 . 
         [0117]    Computing device  500  further includes I/O interface(s)  550 . I/O interface(s)  550  allow for input and output of data with external device(s)  560  that may be connected to computing device  500 . Computing device  500  further includes network interface(s)  540  for communications between computing device  500  and a computer network. 
         [0118]    As will be appreciated by one skilled in the art, aspects of the present invention may be embodied as a system, method or computer program product. Accordingly, aspects of the present invention may take the form of an entirely hardware embodiment, an entirely software embodiment (including firmware, resident software, and micro-code) or an embodiment combining software and hardware aspects that may all generally be referred to herein as a “circuit,” “module” or “system.” 
         [0119]    The computer readable storage medium can be a tangible device that can retain and store instructions for use by an instruction execution device. The computer readable storage medium may be, for example, but is not limited to, an electronic storage device, a magnetic storage device, an optical storage device, an electromagnetic storage device, a semiconductor storage device, or any suitable combination of the foregoing. A non-exhaustive list of more specific examples of the computer readable storage medium includes the following: a portable computer diskette, a hard disk, a random access memory (RAM), a read-only memory (ROM), an erasable programmable read-only memory (EPROM or Flash memory), a static random access memory (SRAM), a portable compact disc read-only memory (CD-ROM), a digital versatile disk (DVD), a memory stick, a floppy disk, a mechanically encoded device such as punch-cards or raised structures in a groove having instructions recorded thereon, and any suitable combination of the foregoing. A computer readable storage medium, as used herein, is not to be construed as being transitory signals per se, such as radio waves or other freely propagating electromagnetic waves, electromagnetic waves propagating through a waveguide or other transmission media (e.g., light pulses passing through a fiber-optic cable), or electrical signals transmitted through a wire. 
         [0120]    Computer readable program instructions described herein can be downloaded to respective computing/processing devices from a computer readable storage medium or to an external computer or external storage device via a network, for example, the Internet, a local area network, a wide area network and/or a wireless network. The network may comprise copper transmission cables, optical transmission fibers, wireless transmission, routers, firewalls, switches, gateway computers and/or edge servers. A network adapter card or network interface in each computing/processing device receives computer readable program instructions from the network and forwards the computer readable program instructions for storage in a computer readable storage medium within the respective computing/processing device. 
         [0121]    Computer readable program instructions for carrying out operations of the present invention may be assembler instructions, instruction-set-architecture (ISA) instructions, machine instructions, machine dependent instructions, microcode, firmware instructions, state-setting data, or either source code or object code written in any combination of one or more programming languages, including an object oriented programming language such as Smalltalk, C++ or the like, and conventional procedural programming languages, such as the “C” programming language or similar programming languages. The computer readable program instructions may execute entirely on the user&#39;s computer, partly on the user&#39;s computer, as a stand-alone software package, partly on the user&#39;s computer and partly on a remote computer or entirely on the remote computer or server. In the latter scenario, the remote computer may be connected to the user&#39;s computer through any type of network, including a local area network (LAN) or a wide area network (WAN), or the connection may be made to an external computer (for example, through the Internet using an Internet Service Provider). In some embodiments, electronic circuitry including, for example, programmable logic circuitry, field-programmable gate arrays (FPGA), or programmable logic arrays (PLA) may execute the computer readable program instructions by utilizing state information of the computer readable program instructions to personalize the electronic circuitry, in order to perform aspects of the present invention. 
         [0122]    Aspects of the present invention are described herein with reference to flowchart illustrations and/or block diagrams of methods, apparatus (systems), and computer program products according to embodiments of the invention. It will be understood that each block of the flowchart illustrations and/or block diagrams, and combinations of blocks in the flowchart illustrations and/or block diagrams, can be implemented by computer readable program instructions. 
         [0123]    These computer readable program instructions may be provided to the processor  520  of the general purpose computing device  500 , special purpose computer, or other programmable data processing apparatus to produce a machine, such that the instructions, which execute via the processor of the computer or other programmable data processing apparatus, create means for implementing the functions/acts specified in the flowchart and/or block diagram block or blocks. These computer readable program instructions may also be stored as computer readable storage medium in the computer readable tangible storage device(s)  530  that can direct a computer, a programmable data processing apparatus, and/or other devices to function in a particular manner, such that the computer readable storage medium having instructions stored therein comprises an article of manufacture including instructions which implement aspects of the function/act specified in the flowchart and/or block diagram block or blocks. 
         [0124]    The computer readable program instructions may also be loaded onto a computer, other programmable data processing apparatus, or other device to cause a series of operational steps to be performed on the computer, other programmable apparatus or other device to produce a computer implemented process, such that the instructions which execute on the computer, other programmable apparatus, or other device implement the functions/acts specified in the flowchart and/or block diagram block or blocks. 
         [0125]    The flowchart and block diagrams in the Figures illustrate the architecture, functionality, and operation of possible implementations of systems, methods, and computer program products according to various embodiments of the present invention. In this regard, each block in the flowchart or block diagrams may represent a module, segment, or portion of instructions, which comprises one or more executable instructions for implementing the specified logical function(s). In some alternative implementations, the functions noted in the block may occur out of the order noted in the figures. For example, two blocks shown in succession may, in fact, be executed substantially concurrently, or the blocks may sometimes be executed in the reverse order, depending upon the functionality involved. It will also be noted that each block of the block diagrams and/or flowchart illustration, and combinations of blocks in the block diagrams and/or flowchart illustration, can be implemented by special purpose hardware-based systems that perform the specified functions or acts or carry out combinations of special purpose hardware and computer instructions.