Abstract:
A method for verification includes providing an implementation model, which defines model states of a target system and model transitions between the model states, and providing a specification of the target system, including properties that the system is expected to obey. A tableau is created from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties. The tableau transitions are compared to the model transitions to determine whether a discrepancy exists therebetween.

Description:
FIELD OF THE INVENTION 
   The present invention relates generally to design automation and verification, and specifically to hardware verification of integrated circuit design. 
   BACKGROUND OF THE INVENTION 
   Hardware verification is currently the bottleneck and the most expensive task in the design of a semiconductor integrated circuit. Model checking is a method of formal verification that is gaining in popularity for this purpose. The method is described generally by Clarke et 1. in  Model Checking  (MIT Press, 1999). 
   To perform model checking of the design of a device, a verification engineer reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {φ} (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL). A hardware model M (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set, i.e., that M           φ, under all possible input sequences. Such testing is a form of reachability analysis.
   Model checking is preferably carried out automatically by a symbolic model checking program, such as SMV, as described, for example, by McMillan in  Symbolic Model Checking  (Kluwer Academic Publishers, 1993). A number of practical model checking tools are available, among them RuleBase, developed by IBM, which is described by Beer et al. in “RuleBase: an Industry-Oriented Form Verification Tool,” in  Proceedings of the Design Automation Conference DAC&#39; 96 (Las Vegas, Nev., 1996). 
   As hardware devices grow larger and more complex, the set of properties needed for model checking becomes unwieldy. The verification engineer has no systematic way to be sure of whether the property set is complete, in the sense of covering all possible states and transitions that may occur in the model. If the property set is incomplete, a bug in the design may go undetected. The engineer may therefore continue to add more and more properties indefinitely, never knowing whether the set is yet sufficient or not. 
   Coverage metrics have been applied in various fields of simulation-based verification in order to measure and improve the completeness with which a given simulation tool represents the actual behavior of a target system. An application of such a metric to model checking is described by Hoskote et al., in “Coverage Estimation for Symbolic Model Checking,” in  Proceedings of the Design Automation Conference DAC&#39; 99 (IEEE Computer Society Press, 199). This publication presents a method for estimating whether a set of properties is sufficient to cover all possible states of a model. It notes, however, that the disclosed method cannot point out functionality that may be missing in the model, nor can it ensure that all possible paths between the states are covered. The publication also indicates that “path coverage would be an ideal coverage metric because it can provide coverage of actual executions of the circuit over time.” The publication considers that by comparison with state coverage, “path coverage is a much more intractable problem.” 
   SUMMARY OF THE INVENTION 
   It is an object of some aspects of the present invention to provide improved methods and systems for design verification. 
   It is a further object of some aspects of the present invention to provide improved methods and metrics for analyzing the coverage of a set of properties used in model checking, and in particular to provide methods for analyzing path coverage. 
   In preferred embodiments of the present invention, a specification, consisting of properties, is generated to verify a given implementation model of a target system, and a tableau is constructed corresponding to the properties. Such a tableau is defined as a finite state machine that satisfies all of the properties in the specification. The states and transitions of the tableau are compared to those of the model to ascertain that there is full correspondence between the possible states and transitions of the model and those of the tableau. To the extent that there are no substantive differences, it is concluded that the set of properties fully specifies the model. 
   In some preferred embodiments of the present invention, the tableau is compared to the model by inputting the tableau to a model checking program, such as SMV, along with the given model. If for every possible combination of inputs, the tableau gives exactly the same set of outputs as the model, then the specification of the properties is complete. On the other hand, if a difference occurs for some input, it means that the specified properties are insufficient and/or that there is an error in the model. The fact that the outputs of the tableau exactly correspond to those of the model indicates that for every reachable state of the tableau, there is a corresponding state in the model, and for every possible transition in the tableau, there is a corresponding transition between the corresponding states in the model. It also means that there are no excess transitions or spurious initial conditions in the tableau that would allow transitions to be made among states in a way that would not be possible in the model. 
   The methods of the present invention thus inform the user when the specification of properties is complete or, alternatively, provide an indication as to where there may be flaws in the correspondence between the specification and the model. Such flaws typically point either to a state or transition in the tableau that is not implemented in the model, thus warning either that the specification does not adequately constrain the model, or that the model has failed to implement a meaningful state or transition of the target system. By comparison, the method of Hoskote et al. is limited to finding an estimation of state coverage, and not transitions or exact state coverage, and therefore cannot provide a conclusive indication that the set of properties is complete. 
   There is therefore provided, in accordance with a preferred embodiment of the present invention, a method for verification, including: 
   providing an implementation model, which defines model states of a target system and model transitions between the model states; 
   providing a specification of the target system, including properties that the system is expected to obey; 
   creating a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties; and 
   comparing the tableau transitions to the model transitions to determine whether a discrepancy exists therebetween. 
   In a preferred embodiment, creating the tableau includes defining a finite state machine using a hardware description language, wherein the implementation model has model inputs and outputs, and wherein defining the finite state machine includes describing a virtual device having inputs and outputs corresponding to the model inputs and outputs of the implementation model. Preferably, comparing the transitions includes performing a reachability analysis using both the implementation model and the tableau while providing identical inputs to the inputs of both the implementation model and the tableau, and verifying that the outputs are always identical. Most preferably, performing the reachability analysis includes comparing the model and the tableau automatically using a model checker and providing evidence of a tableau transition that is not implemented in the model. 
   In another preferred embodiment, comparing the tableau transitions includes associating model transitions with corresponding tableau transitions, wherein associating the transitions includes defining a reachable simulation preorder relating the model and the tableau. Preferably, associating the transitions includes finding a tableau transition that is not implemented in the model and, most preferably, deriving an indication, based on the unimplemented transition, that the specification is not complete with respect to the model. Alternatively or additionally, finding the tableau transition that is not implemented in the model includes deriving an indication, based on the unimplemented transition, that a transition of the target system is missing in the model. 
   Preferably, the method includes associating model states with corresponding tableau states. Further preferably, associating the model states with the corresponding tableau states includes finding a tableau state that is not implemented in the model and deriving an indication, based on the unimplemented state, that the specification is not complete with respect to the model. Alternatively or additionally, finding the tableau state that is not implemented in the model includes deriving an indication, based on the unimplemented state, that a state of the target system is missing in the model. Further alternatively or additionally, associating the model states with the corresponding tableau states includes finding multiple model states corresponding to a single tableau state. 
   Preferably, creating the tableau includes creating a reduced tableau from which one or more redundant states have been eliminated. 
   Further preferably, comparing the transitions includes verifying that the specification is a complete and correct description of the implementation model responsive to the comparison. 
   There is also provided, in accordance with a preferred embodiment of the present invention, a verification processor, which is configured to receive an implementation model, defining model states of a target system and model transitions between the model states, and to receive a specification of the target system, including properties that the system is expected to obey, and which is operative to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau transitions to the model transitions to determine whether a discrepancy exists therebetween. Preferably, the processor is operative to perform model checking of the implementation model. 
   There is further provided, in accordance with a preferred embodiment of the present invention, a computer software product for verification of a specification of a target system, which specification includes properties that the system is expected to obey, by comparison with an implementation model, which defines model states of the target system and model transitions between the model states, the product including a computer-readable medium having computer program instructions recorded therein, which instructions, when read by a computer, cause the computer to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau transitions to the model transitions to determine whether a discrepancy exists therebetween. 
   Preferably, the program instructions cause the computer to compare the tableau with the model by running a reachability analysis using both the implementation model and the tableau while providing identical inputs to the inputs of both the implementation model and the tableau, and verifying that the outputs are always identical. Most preferably, the reachability analysis is performed using an automatic model checker, and the instructions cause the computer to verify that the specification is a complete description of the implementation model. 
   There is additionally provided, in accordance with a preferred embodiment of the present invention, a method for verification, including: 
   providing an implementation model, which defines model states of a target system and model transitions between the model states; 
   providing a specification of the target system, including properties that the system is expected to obey; 
   creating a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties; and 
   comparing the model and the tableau by inputting the model and the tableau to an automatic model checking program. 
   Preferably, comparing the model and the tableau includes providing evidence of a transition or state in the tableau that is not implemented in the model, most preferably in the form of a counter-example indicative of the unimplemented transition or state. 
   There is moreover provided, in accordance with a preferred embodiment of the present invention, model checking apparatus, which is configured to receive an implementation model, defining model states of a target system and model transitions between the model states, and to receive a specification of the target system, including properties that the system is expected to obey, and which is operative to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau to the model by inputting the model and the tableau to an automatic model checking program. 
   There is furthermore provided, in accordance with a preferred embodiment of the present invention, a computer software product for verification of a specification of a target system, which specification includes properties that the system is expected to obey, by comparison with an implementation model, which defines model states of the target system and model transitions between the model states, the product including a computer-readable medium having computer program instructions recorded therein, which instructions, when read by a computer, cause the computer to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau to the model by inputting the model and the tableau to an automatic model checking program. 
   The present invention will be more fully understood from the following detailed description of the preferred embodiments thereof, taken together with the drawings in which: 

   
     BRIEF DESCRIPTION OF THE DRAWINGS 
       FIG. 1  is a schematic pictorial illustration showing a system for model checking, in accordance with a preferred embodiment of the present invention; 
       FIG. 2  is a block diagram that schematically illustrates an implementation model used in model checking and a corresponding tableau of properties, in accordance with a preferred embodiment of the present invention; 
       FIG. 3  is a state diagram that schematically illustrates a finite state machine corresponding to the tableau of  FIG. 2 , in accordance with a preferred embodiment of the present invention; 
       FIG. 4  is a flow chart that schematically illustrates a method for verifying a set of properties generated for the purpose of model checking, in accordance with a preferred embodiment of the present invention; and 
       FIG. 5  is a flow chart that schematically illustrates another method for verifying a set of properties generated for the purpose of model checking, in accordance with a preferred embodiment of the present invention. 
   

   DETAILED DESCRIPTION OF PREFERRED EMBODIMENTS 
     FIG. 1  is a schematic pictorial illustration of a system  20  for model checking, in accordance with a preferred embodiment of the present invention. System  20  typically comprises a verification processor  22 , typically a general-purpose computer workstation running suitable model checking software, such as the above-mentioned IBM RuleBase, under the control of a verification engineer  24 . The system receives a hardware implementation model  26  of a target system or device  30  in development. Engineer  24  prepares a specification of properties  28 , for use in model checking of model  26 . The completeness and correctness of the specification are verified by system  20  using methods described in detail hereinbelow. 
   Reference is now made to  FIG. 2 , which is a block diagram representing a model of a target hardware device  40 , in this case a simple two-port synchronous arbiter, used hereinbelow to exemplify a method for verifying property set  28 , in accordance with a preferred embodiment of the present invention. Device  40  has two request inputs  42 , labeled REQ0 and REQ1, and two acknowledge outputs  44 , ACK0 and ACK1. The assertion of ACKi is a response to the assertion of REQi. Initially, both outputs of the arbiter are inactive. At any time, at most one acknowledge output may be active. The arbiter grants one of the active requests in the next cycle, and uses a round robin algorithm in case both request inputs are active. In the case of simultaneous assertion (i.e. both requests are asserted and were not asserted in the previous cycle), REQ0 has priority in the first simultaneous assertion occurrence. In any subsequent occurrence of simultaneous assertion the priority rotates with respect to the previous occurrence. 
   An implementation of device  40  in the SMV language is presented below in Table I: 
   
     
       
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
             
             
           
             
             
           
             
             
             
             
           
             
             
           
             
             
             
             
           
             
             
           
             
             
           
             
             
             
             
           
             
             
           
             
             
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
         
             
               TABLE I 
             
             
                 
             
           
           
             
               1) 
               var 
             
           
        
         
             
               1) 
               req0; req1; ack0; ack1; robin : boolean; 
             
           
        
         
             
               3) 
               assign 
             
           
        
         
             
               4) 
               init(ack0) := 0; 
             
             
               5) 
               init(ack1) := 0; 
             
             
               6) 
               init(robin) := 0; 
             
           
        
         
             
               7) 
               next(ack0) := case 
             
           
        
         
             
               8) 
               !req0 
               : 0; 
               - No request results no 
             
           
        
         
             
                 
               ack 
             
           
        
         
             
               9) 
               !req1 
               : 1; 
               - A single request 
             
             
               10) 
               !ack0&amp;!ack1 
               :!robin; 
               - Simultaneous requests 
             
           
        
         
             
                 
               assertions 
             
           
        
         
             
               11) 
               1 
               :!ack0; 
               - Both requesting, toggle 
             
           
        
         
             
                 
               ack 
             
           
        
         
             
               12) 
               esac; 
             
             
               13) 
               next(ack1) := case 
             
           
        
         
             
               14) 
               !req1 
               : 0; 
               - No request results no 
             
           
        
         
             
                 
               ack 
             
           
        
         
             
               15) 
               !req0 
               : 1; 
               - A single request 
             
             
               16) 
               !ack0&amp;ack1 
               : robin; 
               - Simultaneous assertion 
             
             
               17) 
               1 
               : !ack1; 
               - Both requesting, toggle 
             
           
        
         
             
                 
               ack 
             
           
        
         
             
               18) 
               esac; 
             
             
               19) 
               next(robin) :=if req0&amp;req1&amp;!ack0&amp;!ack1 then !robin 
             
           
        
         
             
               20) 
               else robin endif; - Two 
             
           
        
         
             
                 
               simultaneous request 
             
             
                 
                 
             
           
        
       
     
   
   assertions 
   From the functional specification of arbiter  40  given above, the following temporal formulas are derived that describe the properties of the device:
     1. The initial state is          ack0                   ack1.   2. At all times, mutual exclusion holds, i.e.,          ack0                   ack1 (property φ1).   3. At all times one of the following properties should hold:
       a) No requests followed by no acknowledge (property φ2).   b) A single request (when the other request is not active) is served in the following cycle (properties φ3 and φ4).   c) A request active while the alternate channel is being served will be served in the following cycle (properties φ5 and φ6).   d) When a cycle with no active request is followed by a cycle with two active requests, the result will be as follows—
           The first such occurrence will result in acknowledgment to channel  0  (φ0).   Each subsequent occurrence will result in acknowledgment of the channel that was not acknowledged in the previous occurrence (φ7 and φ8).   
           The behavior of the arbiter under these conditions (no active request followed by two active requests)   
       

   is governed by the non-observable variable “robin,” as defined in Table I. 
   The above formulas correspond to the proeprties Φ0, Φ1, . . . , Φ8 listed symbolically below in Table II, which are a complete specification of arbiter  40  written in the form of a safety formula ψ in Universal Computation Tree Logic (known as ACTL). ACTL is a branching-time temporal logic. It is described in detail by Grumberg et al. in “Model Checking and Modular Verification,” in  ACM ransactions on Programming Language and Systems  16(3) (1994), pp. 843–871. As the variable “robin” is not observable, it does not appear explicitly in the properties in Table II. 
                                                                                                 TABLE II                   ψ =            ack0                     ack1                          A[(          req0                    req1            ack0            ack1)W                (req0            req1                    ack0                    ack1            AXack0)]             - φ 0                  AG(                (          ack0                    ack1)              - φ 1             (          req0                    req1 → AX(          ack0                    ack1))              - φ 2             (req0                    req1 → AX ack0)              - φ 3             (          req0            req1 → AX ack1)              - φ 4             (req1            ack0 → AX ack1)              - φ 5             (req0            ack1 → AX ack0)              - φ 6             (req0            req1                     ack0                     ack1 → AX(ack0 →           A[          req0                     req1            ack0            ack1)W                (req0            req1                     ack0                     ack1            AXack1)]))           -φ 7                  (req0            req1                     ack0                     ack1 → AX(ack1 →           A[(z,233 req0                     req1            ack0            ack1)W                (req0            req1                     ack0                     ack1            AXack0)])) ) -φ 8                          
This representation uses the temporal operators X (“next state”), W (“weak until,” i.e., remains true until), and G (“globally”), along with the quantifier A (“for all paths”). It is noted that AGφ≡A[φWfalse].
 
     FIG. 3  is a state diagram that schematically illustrates a tableau  50 , or state machine, corresponding to the properties of the safety formula in Table II, in accordance with a preferred embodiment of the present invention. The tableau is preferably a “reduced tableau,” as defined in Appendix A, which is most preferably constructed automatically, using a computer program that receives the properties as its input and implements the tableau construction algorithm listed in the appendix. The tableau is used, as described further hereinbelow, to verify that the properties completely cover the states and transitions of the device model defined in Table I. 
   Tableau  50  comprises six state groups  52 ,  54 ,  56 ,  58 ,  60  and  62 . Each of the groups includes a number of states  64  that correspond to a particular output condition of device  40 , i.e., in groups  52  and  60 , ack0 is asserted; in groups  54  and  62 , ack1 is asserted; and in groups  56  and  58 , neither output is asserted (!ack0 !ack1). In state groups  52 ,  54  and  56 , the non-observable variable robin=0, whereas in groups  58 ,  60  and  62 , robin=1. As indicated by an arrow  66 , operation of device  40  begins in group  56 , with !ack0, !ack1 and robin=0. Transitions from one state to another depend on the choice of inputs, which are marked in each state  64 . Thus, for example, when req1 is asserted in state group  52 , a transition is invoked to group  54 , in which ack1 is asserted. 
   Tableau  50  is a sort of virtual device, corresponding to actual target device  40 . Appendix B accordingly contains source code in VHDL representing a tableau similar to tableau  50  as a device model. In preferred embodiments of the present invention, this virtual device is tested to determine whether its states and transitions correspond exactly to those of the actual device, or equivalently whether the behavior of the virtual device under all possible combinations of input conditions is identical to that of the model of the actual device. If differences are found, they are then indicative either that the tableau (and hence the specified properties) are incomplete or that the model itself is incomplete. Methods and criteria for testing tableau  50  are described further hereinbelow. 
     FIG. 4  is a flow chart that schematically illustrates a method for verifying a specification of model checking properties by comparing tableau  50  with device  40 , in accordance with a preferred embodiment of the present invention. The method begins with preparation of the specification, such as the formula ψ listed in Table II, and checking the device model M to ensure that the model satisfies the specification, i.e., that M           ψ. The specification is then used to construct the tableau. As shown in  FIG. 2 , tableau  50  as a virtual device model has virtual inputs  72  and outputs  74 , corresponding respectively to inputs  42  and outputs  44  of implementation model  40  of the target device. For the purpose of testing the tableau against the implementation model, the tableau inputs are labeled REQ0_SPEC and REQ1_SPEC, and the tableau outputs are labeled similarly, ACK0_SPEC and ACK1_SPEC.
   These input and output labels are inserted in a representation of the tableau, preferably in the form of suitable program code, as listed in Appendix B. IBM RuleBase, as described hereinabove, is capable of translating the VHDL code in Appendix B into the SMV language used by model checkers. In the example shown in Appendix B, the model of device  40  is simplified, relative to the definition in Tables I and II, in that the non-observable variable “robin” is not used. Instead, ack0 always receives priority when a state in which there is no active request is followed by two active requests. 
   In order to test the tableau against the device model, a new model is created, combining the original implementation model and the virtual device model of the tableau. Inputs  72  of tableau  50  are tied to the corresponding inputs  42  of implementation model  40 , so that the implementation model and the tableau model will receive the same input signals. The new, combined model is then input to an automatic model checking program, such as SMV. The model checker is asked to verify that the following properties regarding the combined model outputs are always true of the combined model: 
   ACK0==ACK0_SPEC 
   ACK1==ACK1_SPEC 
   Alternatively, in certain cases, the two outputs may be checked separately, rather than in a single pass of the model checker, using separate tableaux corresponding to subsets of the specification properties that influence the particular outputs. 
   If the above-mentioned properties of the combined model outputs are confirmed, tableau  50  is assured of representing a complete and correct specification of device  40 . If the tableau specification is not sufficiently detailed, then the tableau outputs ACKi_SPEC will not be as constrained as the model outputs ACKi, and there will be some combination of inputs under which ACKi_SPEC will have two possible values when ACKi can have only one. This outcome will generally lead engineer  24  to conclude that an additional constraint is required, i.e., that a further property is needed in the specification. Typically, a suitable property is added and the specification is re-checked, repeating the steps described above. If now ACKi==ACKi_SPEC, then the specification can be considered complete and correct. Alternatively, it may turn out that evaluation of the model and specification in this manner will lead engineer  24  to conclude that there is an error in the implementation model, such as a missing state or transition, which causes the outputs of the model and the tableau differ. It is a further advantage of automatic model checking programs that they provide evidence of such errors, in the form of “counter-examples,” that assist the engineer in identifying and correcting the error. 
     FIG. 5  is a flow chart that schematically illustrates another method for verifying a model checking specification, in accordance with a preferred embodiment of the present invention. The method begins, like the method of  FIG. 4 , with preparation of a specification of model properties and model checking to determine that the model satisfies the specification. The specification is then used to create a corresponding tableau, which is evaluated against the device implementation model. The method of  FIG. 5  differs from the method of  FIG. 4  in the manner in which the tableau is evaluated, as described hereinbelow. Whereas the method of  FIG. 4  is useful primarily in checking deterministic models, the method of  FIG. 5  can be used for substantially any model, including non-deterministic models. 
   In order to evaluate the tableau against the model, a simulation preorder, SIM, is calculated for the model and the tableau. SIM is a relation between the model M and the tableau T (SIM ⊂ M×T) containing pairs of states (s i , s t ) in M and T, respectively. SIM satisfies the following requirements:
         For every initial state s 0i  of M, there is an initial state s 0t  of T, such that (s 0i , s 0t ) belongs to SIM.   For every pair of states (s i , s t ) in SIM, state s i  is characterized by the same set of atomic propositions as s t  (i.e., the same values of the variables ACKi and REQi in the example of device  40 ).   For every state-to-state transition from state s i , there is a corresponding transition for state s t  (although not necessarily a one-to-one correspondence).       

   Formally, an algorithm for the computation of SIM is presented in Table III, below, in pseudocode form. Here S i (s i ) is the set of all values of states in M, and S t (s t ) is the set of all values of states in T(φ). R i (s i , s i ′) is the transition relation of M, and R t (s t , s t ′) is the transition relation of T(φ). L i (s i ) is a labeling function that computes the values of atomic propositions, AP, of a state s i  of M, while L t (s t ) is a labeling function that computes the values of atomic propositions, AP, of a state s t  of T(φ). 
   
     
       
             
             
           
         
             
                 
               TABLE III 
             
             
                 
                 
             
           
           
             
                 
               Init: 
             
             
                 
               SIM 0 (s i , s t ) := {(s i , s t ) ∈ S i  × S t  | L i (s i ) = L t (s t )}; j := 0 
             
             
                 
               Repeat{ 
             
             
                 
               SIM j+1  := {(s i , s t ) | 
             
             
                 
               ∀s i ′(R i (s i , s i ′) → ∃s t ′(R t (s t , s t ′)            SIM j (s i ′, s t ′)))            SIM j (s i , s t ) 
             
             
                 
               j:=j+1 
             
             
                 
               } until SIM j =SIM j−1   
             
             
                 
               SIM:=SIM j   
             
             
                 
                 
             
           
        
       
     
   
   Preferably, for efficient computation, S i , S t , R i , R t , L i , L t  and SIM j  are all represented as Ordered Binary Decision Diagrams (OBDDs). This type of representation, using connected, directed, acyclic graphs, is hown in the art of model checking. The use of OBDDs in this regard is described, for example, by McMillan in  Symbolic Model Checking  (Kluwer Academic Press, Norwell, Mass., 1993). 
   All of the operations shown in Table III are well known for OBDDs, except for the computation of SIM j+1 . To state this computation in OBDD terms, we define the following OBDD operations: 
   compose({right arrow over (y)}, {right arrow over (u)})≡∃{right arrow over (x)}(a({right arrow over (x)}, {right arrow over (y)})           b({right arrow over (x)}, {right arrow over (u)}))
   compose_odd({right arrow over (y)}, {right arrow over (u)})≡∃{right arrow over (x)}(a ({right arrow over (y)}, {right arrow over (x)})           b({right arrow over (u)}, {right arrow over (x)})
   These two operations operate on two OBDDs, a and b, over three vectors of n variables, {right arrow over (x)}, {right arrow over (y)} and {right arrow over (u)}. In these terms, the computation of SIM j+1  is given by: 
   SIM j+1 ({right arrow over (s)} i , {right arrow over (s)} t ):=           compose_odd(R i ({right arrow over (s)} i , {right arrow over (s)} i ′),          compose_odd(R t ({right arrow over (s)} t , {right arrow over (s)} t ′), SIM j ({right arrow over (s)} i ′, {right arrow over (s)} t ′)))           SIM j ({right arrow over (s)} i , {right arrow over (s)} t )
   Based on the simulation preorder SIM, a reachable simulation preorder for M and T, ReachSIM, is determined. T may contain paths by which a state s is reached from an initial state, which do not have corresponding permissible paths in M. ReachSIM  ⊂  SIM contains only pairs of states (s i , s t ) characterized in that states s i  and s t  are reached by corresponding paths π i  and π t  from corresponding initial states. A path π i =s 0i , s 1i , . . . , s i , and a path π t =s 0t , s 1t , . . . , s t  are considered to correspond if every pair of states (s i , s t ) along the paths belongs to SIM. Details of the computation of ReachSIM are presented in Table IV: 
                           TABLE IV                           Init:           ReachSIM 0  := (S 0i  × S 0t ) ∩ SIM; j := 0           Repeat{           ReachSIM j+1  := {(s i ′, s t ′) | ∃s i , s t (ReachSIM j (s i , s t )            R i (s i , s i ′)                      R t (s t , s t ′)           SIM(s i ′, s t ′)) } ∪ ReachSIM j             j := j+1           } until ReachSIM j  = ReachSIM j−1             ReachSIM := ReachSIM j                          
Here, too, if S i , S t , R i , R t , L i , L t  and ReachSIM j  are all OBDDs, then all of the operations in Table IV are well known, except for the computation of ReachSIM j+1 , which is given in OBDD terms by:
 
ReachSIM j+1 ({right arrow over (s)} i , {right arrow over (s)} t ):=(compose(compose(ReachSIM j ({right arrow over (s)} i , {right arrow over (s)} t ) R i ({right arrow over (s)} i , {right arrow over (s)} i ′)), R t ({right arrow over (s)} t , {right arrow over (s)} t ′))             SIM({right arrow over (s)} i ′, {right arrow over (s)} t ′))          ReachSIM j ({right arrow over (s)} i ′,{right arrow over (s)} t ′)

   ReachSIM thus identifies a set of states in T having transitions that correspond to the actual transitions in M. There may yet be, however, states or transitions in T that do not have corresponding states or transitions in M, meaning that the specification does not constrain the implementation model tightly enough, so that one or more additional properties are needed. Such states and transitions are referred to herein as being “unimplemented.” There may likewise be states in T that correspond simultaneously to two or more states in M. Such discrepancies are detected using ReachSIM to evaluate the following criteria (preferably using OBDD operations), either serially or in parallel:
         Unimplemented start states:
 
{s t εS 0t |∀s i εS 0i [(s i , s t )          ReachSIM]}
    These are initial tableau states that have no corresponding initial states in the model (and therefore are absent from ReachSIM). The existence of an unimplemented start state indicates either that the specification does not adequately constrain the start states, or that the model is lacking a required initial state.   Unimplemented states:
 
{s t εS t |∀s i εS i [(s i ,s t )         ReachSIM]}
    The existence of a state anywhere in the tableau that is not included in ReachSIM indicates either that the specification is lacking in constraints or that a meaningful state of the device is not implemented in the model.   Unimplemented transitions:
 
(s t ,s t ′)εR t |∃s i ,s i ′εS i ,
 
(s i ,s t )εReachSIM,(s i ,s t ′)εReachSIM,(s i ,s i ′)         R i ]}
    These are transitions between states of the tableau for which there is no corresponding transition in the model. The states belong to ReachSIM, so that they have corresponding states in the model, which are reached by corresponding paths. The existence of an unimplemented transition indicates either that the specification is not tight enough or that a required transition, between reachable implementation states, was not implemented in the model. Assuming S i , R i , R t  and ReachSIM are all OBDDs, the set of unimplemented transitions can be represented by the following equation:
 
nimplementedTransition({right arrow over (s)} t ,{right arrow over (s)} t ′):=compose(compose(         R i ({right arrow over (s)} i ,{right arrow over (s)} i ′), ReachSIM({right arrow over (s)} i ,{right arrow over (s)} t )), ReachSIM({right arrow over (s)} i ′,{right arrow over (s)} t ′))         R t ({right arrow over (s)} t ,{right arrow over (s)} t ′)
   Many-to-one mapping:
 
s t εS t |∃s 1i ,s 2i εS i (s 1i ,s t )εReachSIM,(s 2i ,s t )εReachSIM,s 1i ≠s 2i ]
    In this case, there may be a tableau state to which multiple implementation states are mapped, i.e., a state s which is paired in ReachSIM with at least two different model states s i ′ and s j ′. The existence of a many-to-one state indicates either that the specification is not sufficiently detailed, or that the implementation contains redundancies. If ReachSIM and the model states are OBDDs, the set of many-to-one states can be represented by:
 
ManyToOne({right arrow over (s)} t )=∃v 1 (ReachSIM({right arrow over (s)} 1 ,{right arrow over (s)} t )         compose(({right arrow over (s)} 1 ≠{right arrow over (s)} 2 ) ReachSIM({right arrow over (s)} 2 ,{right arrow over (s)} t ))
       

   If the first three of these four criteria return empty results, then T is a complete specification of M. Any dissimilarity between the tableau and the implementation will result in a non-empty result. Preferably, the tableau T that is used in this method is a reduced tableau, as defined in Appendix A, since traditional (non-reduced) tableaux typically contain redundancies, which are removed in the reduced tableau. If the first three of the criteria above hold (i.e., return empty results), T and M are bisimilar, and the fourth criterion is not necessary to establish the completeness of T. It may, however, indicate that there are redundancies in the implementation. 
   As noted hereinabove, verification of specification properties vis-a-vis the implementation model, using any of the methods described herein, is preferably carried out using software for this purpose running on processor  22 . Software for use in such verification is preferably supplied as component of a simulation and model checking software package. Alternatively, the software for tableau construction and verification is provided as an independent software package. In either case, the software may be conveyed to processor  22  in intangible form, over a network, for example, or on tangible media, such as CD-ROM. 
   Although preferred embodiments are described hereinabove with reference to certain methods and languages used in model checking, it will be understood that the application of the present invention is not limited to any particular language or method of implementation. Those skilled in the art will appreciate that the principles of the present invention may similarly be used in other areas of verification, not only for electronic devices, but also in verification of other types of target systems, as well, for example, transportation systems or complex valve manifolds. It will thus be understood that the preferred embodiments described above are cited by way of example, and the full scope of the invention is limited only by the claims. 
   APPENDIX A 
   1 Reduced Tableau for ACTL 
   In this section we define a reduced tableau for the subset of ACTL safety formulas. We follow the definition of the reduced tableau for LTL presented in [3]. A tableau is a special form of a Kripke structure, consisting of states labeled with atomic propositions and transitions between the states. As is often the case with tableaux for temporal logics (e.g. [2, 1]), a state of the tableau consists of a set of formulas that are supposed to hold along all paths leaving the state. Unlike typical tableaux, however, the formulas in the states of the reduced tableau are interpreted over a three-valued domain. Thus, a state may include a formula or its negation, or none of the two. If the latter occurs, it reflects a “don&#39;t care” situation. i.e. the formula may be either true or false in the state. 
   Similarly to [2], we wish the reduced tableau for a formula ψ to satisfy φ. Furthermore, it should be greater by the simulation preorder [4] than any Kripke structure that satisfies ψ. In order to achieve these goals we will adapt both definitions of             and simulation preorder to be applicable to three-valued structures. Below we present the formal definitions of the tableau and of the adapted relations.
   Let AP ψ  be the set of atomic propositions in an ACTL formula ψ. 
   Definition 1.1 (sub-formulas) The set of sub-formulas of ψ is defined recursively as follows: 
   1. sub(p)={p} and sub(           p)={         p}, if pεAP ψ 
   2. sub(φ)={φ}∪sub(g 1 )∪sub(g 2 ), if φ=g 1             g 2  or φ=g 1           g 2 .
   3. sub(AX g 1 )={AX g 1 }∪sub(g 1 ) 
   4. sub(A[g 1  W g 2 ])={A[g 1  W g 2 ], AX A[g 1  W g 2 ]}∪sub(g 1 ) ∪sub(g 2 ) 
   We will distinguish between α-formulas and β-formulas, which are conjunctions and disjunctions, respectively. In the reduced tableau, if a state satisfies a conjunction, then it also satisfies its two conjuncts. On the other hand, if it satisfies a a disjunction, it will usually satisfy only one of the disjunct, leaving the other as “don&#39;t care”. 
   Definition 1.2 (α-formula) 
   A formula gεsub(ψ) is an α-formula if g=g 1             g 2 .
   Definition 1.3 (β-formula) 
   A formula gεsub(ψ) is a β-formula if: 
   1. g=g 1             g 2 ; in which case k 1 (g)={g 1 } and k 2 (g)={g 2 }.
   2. g=A[g 1  W g 2 ], in which case k 1 (g)={g 2 } and k 2 (g)={g 1 , AX A[g 1  W g 2 ]}. 
   Definition 1.4 (            particle) A set of formulas P is a particle if:
   1. P ⊂ sub(ψ) 
   2. pεP→           p         P
   3.            pεP→p         P
   4. P does not contain any α-formula nor any β-formula. 
   Definition 1.5 (Implied successor) A formula g is an implied successor of a particle P if AX gεP. We denote by imps(P) the set of implied successors of P; i.e., imps(P)={g|AX gεP} 
   Note that if P does not include any formula of the form AX g then imps(P)={ }. The particle { } means that the state reached has no commitments to satisfy any of the formulas. Thus, it may be the start of any possible paths. Furthermore, it may simulate any state. We later see that the only son of particle { } is the particle { } itself. 
   function Remove_Redandant(S: Set of Particles): returns Set of Particles return the largest set such that {PεS|∀P i εS i P i             P}
   recursive function cover p (B: Set of formulas) returns: Set of particles 
   if B is not locally consistent then return { }—no particles contain B 
   if there exists some α-formula r=r 1             r 2  in B
       then return cover p (B−{r}∪{r 1 ,r 2 })       

   if there exists some β-formula r such that rεB then return
         cover p (B−{r}∪k 1 (r))∪cover p (B−{r}∪k 2 (r))       

   return {B} −B is a particle 
   end function 
   Definition 1.6 (Successors p (P)) 
   Successors p (P)=Remove_Redandant(cover p (imps(P))). 
   We now describe an iterative algorithm PART_TAB that produces the tableau structure. 
   Algorithm: PART_TAB 
   
     
       
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
         
             
                 
                 
             
           
           
             
                 
               S τ0  := Remove_Redandant(cover p ({ψ})) 
             
             
                 
               S τ  := S τ0   
             
             
                 
               R τ  := ∅ 
             
             
                 
               Mark all particles in S τ  as unprocessed 
             
             
                 
               For each unprocessed particle P in S τ  do 
             
           
        
         
             
                 
               S := successors p (P); 
             
             
                 
               For each Q ∈ S 
             
           
        
         
             
                 
               Add (P,Q) to R τ ; 
             
             
                 
               Define L(P) = P ∩ {p|p ∈ AP ψ } ∩           p|p ∈ AP ψ } 
             
             
                 
               If Q            S τ ; 
             
           
        
         
             
                 
               Add Q to S τ ; 
             
             
                 
               Mark Q as unprocessed; 
             
           
        
         
             
                 
               end for 
             
             
                 
               Mark P as processed; 
             
           
        
         
             
                 
               end for 
             
           
        
         
             
                 
               end for 
             
             
                 
                 
             
           
        
       
     
   
   Note that a state is labeled by propositions from AP and by their negations. Since a state is a particle, it will never contain both a proposition and its negation, but it may contain none of them. 
   We now prune the structure we received, such that any particle has at least one successor. 
   Algorithm: PRUNE_TAB 
   
     
       
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
         
             
                 
                 
             
           
           
             
                 
               Mark all particles in S τ  as unprocessed 
             
             
                 
               Repeat until all particles in S τ  are processed 
             
           
        
         
             
                 
               For each unprocessed particle P in S τ  do 
             
           
        
         
             
                 
               If P has no successors 
             
           
        
         
             
                 
               Remove P from S τ   
             
             
                 
               Remove any edge going to P from R τ   
             
             
                 
               Mark the remaining particles in S τ  as unprocessed 
             
             
                 
               Skip 
             
           
        
         
             
                 
               Mark P as processed; 
             
           
        
         
             
                 
               end for 
             
           
        
         
             
                 
               end Repeat 
             
             
                 
                 
             
           
        
       
     
   
   After activating PART_TAB and PRUNE_TAB we have produced the tableau τ(ψ)=&lt;S τ , S τ0 , R τ , L τ &gt;for ψ. 
   Note that the tableau we construct is total. Any particle that has no successors is removed. 
   REFERENCES 
   
       
       [1] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. L. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ Cache Coherence Protocol. In  Proceedings of the  11 th International Conference on Computer Hardware Description Languages , pages 15–30, 1993. 
       [2] O. Grumberg and D. E. Long. Model checking and modular verification.  ACM Trans. on Programming Languages and Systems,  16(3):843–871, 1994. 
       [3] Z. Manna and A. Pnueli.  Temporal verifications of Reactive Systems—Safety . Springer-Verlag, 1995. 
       [4] R. Milner. An algebraic definition of simulation between programs. In  In proceedings of the  2 nd International Joint Conference on Artificial Intelligence , pages 481–489, September 1971. 
     
  
   APPENDIX B 
   The following is a program listing in VHDL describing a tableau that corresponds generally to the properties of arbiter  40  listed in Table II. As noted hereinabove, however, the listing below is based on a simplified model without the non-observable variable “robin.” In place of the output names ACK0_SPEC and ACK1_SPEC shown in  FIG. 2 , the names ack0_new and ack1_new are used in the listing; and req0 and req1 in the listing correspond respectively to REQ0_SPEC and REQ1_SPEC. 
   
     
       
             
             
           
             
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
             
             
           
         
             
                 
                 
             
           
           
             
                 
               library ieee; 
             
             
                 
               use ieee.std_logic_1164.all; 
             
             
                 
               entity full_spec is 
             
           
        
         
             
                 
               port ( 
                 
             
             
                 
               rb_clock 
               : in std_ulogic; 
             
             
                 
               ack0_new 
               : in std_ulogic; 
             
             
                 
               ack1_new 
               : in std_ulogic; 
             
             
                 
               req0 
               : in std_ulogic; 
             
             
                 
               req1 
               : in std_ulogic; 
             
             
                 
               reset 
               : in std_ulogic; 
             
             
                 
               fails 
               : out 
             
           
        
         
             
                 
               std_ulogic_vector(0 to 5) 
             
           
        
         
             
                 
               ); 
             
           
        
         
             
                 
               end full_spec; 
             
             
                 
               architecture rb of full_spec is 
             
           
        
         
             
                 
               signal not_rb_reset: std_ulogic ; 
             
           
        
         
             
                 
               signal rb_reset 
               : std_ulogic ; 
             
           
        
         
             
                 
               type rb_enum_type is (iu_enum_slash_err, 
             
           
        
         
             
                 
               iu_enum_slash_z); 
             
           
        
         
             
                 
               begin 
             
           
        
         
             
                 
               p: 
             
             
                 
               process 
             
             
                 
               begin 
             
             
                 
               wait until rb_clock&#39;event and rb_clock=‘1’; 
             
             
                 
               not_rb_reset &lt;= ‘1’; 
             
             
                 
               end process; 
             
             
                 
               rb_reset &lt;= reset or (not not_rb_reset); 
             
           
        
         
             
                 
               f1: 
             
           
        
         
             
                 
               fails(0) &lt;= not b21(((((not ack0_new) or (not 
             
           
        
         
             
                 
               ack1_new))) /= ‘0’) 
             
           
        
         
             
                 
               or (rb_reset /= ‘0’) or (rb_clock /= ‘1’)); 
             
             
                 
               f2: 
             
             
                 
               block 
             
           
        
         
             
                 
               constant n: integer := 4; 
             
             
                 
               signal v: std_ulogic_vector(0 to n−1) := 
             
           
        
         
             
                 
               “1110” 
             
           
        
         
             
                 
               signal v_out: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal vnext: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal ok: std_ulogic := ‘1’; 
             
           
        
         
             
                 
               begin 
             
             
                 
               v_out(0) &lt;= ‘0’; 
             
             
                 
               v_out(1) &lt;= v(1) and (‘1’); 
             
             
                 
               v_out(2) &lt;= v(2) and (((not req0) and (not 
             
           
        
         
             
                 
               req1))); 
             
           
        
         
             
                 
               v_out(3) &lt;= v(3) and ((not ((not ack0_new) and 
             
           
        
         
             
                 
               (not ack1_new)))); 
             
           
        
         
             
                 
               vnext(0) &lt;= ‘0’; 
             
             
                 
               vnext(1) &lt;= v_out(1); 
             
             
                 
               vnext(2) &lt;= v_out(1); 
             
             
                 
               vnext(3) &lt;= v_out(2); 
             
           
        
         
             
                 
               p: 
             
             
                 
               process 
             
           
        
         
             
                 
               begin 
             
             
                 
               wait until rb_clock&#39;event and rb_clock=‘1’; 
             
           
        
         
             
                 
               if rb_reset = ‘1’ then 
             
           
        
         
             
                 
               v &lt;= “1110”; 
             
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               else 
             
           
        
         
             
                 
               if (not (v(3) and (not ((not ack0_new) 
             
           
        
         
             
                 
               and (not ack1_new)) 
             
           
        
         
             
                 
               ))) = ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘0’; 
             
           
        
         
             
                 
               elsif ok = ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               end if; 
             
             
                 
               v &lt;= vnext; 
             
           
        
         
             
                 
               end if; 
             
           
        
         
             
                 
               end process; 
             
           
        
         
             
                 
               fails(1) &lt;= not b21 ((ok /= ‘0’) or (rb_reset 
             
           
        
         
             
                 
               /= ‘0’) 
             
           
        
         
             
                 
               or (rb_clock /=‘1’)); 
             
             
                 
               end block; 
             
             
                 
               f3: 
             
             
                 
               block 
             
           
        
         
             
                 
               constant n: integer := 4; 
             
             
                 
               signal v: std_ulogic_vector(0 to n−1) := 
             
           
        
         
             
                 
               “1110”; 
             
           
        
         
             
                 
               signal v_out: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal vnext: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal ok: std_ulogic := ‘1’; 
             
           
        
         
             
                 
               begin 
             
           
        
         
             
                 
               v_out(0) &lt;= ‘0’; 
             
             
                 
               v_out(1) &lt;= v(1) and (‘1’); 
             
             
                 
               v_out(2) &lt;= v(2) and ((req0 and (not ack0_new))); 
             
             
                 
               v_out(3) &lt;= v(3) and ((not ack0_new)); 
             
             
                 
               vnext(0) &lt;= ‘0’; 
             
             
                 
               vnext(1) &lt;= v_out(1); 
             
             
                 
               vnext(2) &lt;= v_out(1); 
             
             
                 
               vnext(3) &lt;= v_out(2); 
             
           
        
         
             
                 
               p: 
             
             
                 
               process 
             
           
        
         
             
                 
               begin 
             
             
                 
               wait until rb_clock&#39;event and rb_clock=‘1’; 
             
           
        
         
             
                 
               if rb_reset = ‘1’ then 
             
           
        
         
             
                 
               v &lt;= “1110”; 
             
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               else 
             
           
        
         
             
                 
               if (not (v(3) and (not ack0_new))) = 
             
           
        
         
             
                 
               ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘0’; 
             
           
        
         
             
                 
               elsif ok = ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               end if; 
             
             
                 
               v &lt;= vnext; 
             
           
        
         
             
                 
               end if; 
             
           
        
         
             
                 
               end process; 
             
           
        
         
             
                 
               fails(2) &lt;= not b21 ((ok /= ‘0’) or (rb_reset 
             
           
        
         
             
                 
               /= ‘0’) 
             
           
        
         
             
                 
               or (rb_clock /= ‘1’)); 
             
           
        
         
             
                 
               end block; 
             
             
                 
               f4: 
             
             
                 
               block 
             
           
        
         
             
                 
               constant n: integer := 4; 
             
             
                 
               signal v: std_ulogic_vector(0 to n−1) := 
             
           
        
         
             
                 
               “1110”; 
             
           
        
         
             
                 
               signal v_out: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal vnext: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal ok: std_ulogic := ‘1’; 
             
           
        
         
             
                 
               begin 
             
           
        
         
             
                 
               v_out(0) &lt;= ‘0’; 
             
             
                 
               v_out(1) &lt;= v(1) and (‘1’); 
             
             
                 
               v_out(2) &lt;= v(2) and (((not req0) and req1)); 
             
             
                 
               v_out(3) &lt;= v(3) and ((not ack1_new)); 
             
             
                 
               vnext(0) &lt;= ‘0’; 
             
             
                 
               vnext(1) &lt;= v_out(1); 
             
             
                 
               vnext(2) &lt;= v_out(1); 
             
             
                 
               vnext(3) &lt;= v_out(2); 
             
             
                 
               p: 
             
             
                 
               process 
             
           
        
         
             
                 
               begin 
             
             
                 
               wait until rb_clock&#39;event and rb_clock=‘1’; 
             
           
        
         
             
                 
               if rb_reset = ‘1’ then 
             
           
        
         
             
                 
               v &lt;= “1110”; 
             
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               else 
             
           
        
         
             
                 
               if (not (v(3) and (not ack1_new))) = 
             
           
        
         
             
                 
               ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘0’; 
             
           
        
         
             
                 
               elsif ok = ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               end if; 
             
             
                 
               v &lt;= vnext; 
             
           
        
         
             
                 
               end if; 
             
           
        
         
             
                 
               end process; 
             
           
        
         
             
                 
               fails(3) &lt;= not b21 ((ok /= ‘0’) or (rb_reset 
             
           
        
         
             
                 
               /= ‘0’) 
             
           
        
         
             
                 
               or (rb_clock /= ‘1’)); 
             
             
                 
               end block; 
             
             
                 
               f5: 
             
             
                 
               block 
             
           
        
         
             
                 
               constant n: integer := 4; 
             
             
                 
               signal v: std_ulogic_vector(0 to n−1) := 
             
           
        
         
             
                 
               “1110”; 
             
           
        
         
             
                 
               signal v_out: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal vnext: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal ok: std_ulogic := ‘1’; 
             
           
        
         
             
                 
               begin 
             
             
                 
               v_out(0) &lt;= ‘0’; 
             
             
                 
               v_out(1) &lt;= v(1) and (‘1’); 
             
             
                 
               v_out(2) &lt;= v(2) and ((req1 and ack0_new)); 
             
             
                 
               v_out(3) &lt;= v(3) and ((not ack1_new)); 
             
             
                 
               vnext(0) &lt;= ‘0’; 
             
             
                 
               vnext(1) &lt;= v_out(1); 
             
             
                 
               vnext(2) &lt;= v_out(1); 
             
             
                 
               vnext(3) &lt;= v_out(2); 
             
           
        
         
             
                 
               p: 
             
             
                 
               process 
             
           
        
         
             
                 
               begin 
             
             
                 
               wait until rb_clock&#39;event and rb_clock=‘1’; 
             
           
        
         
             
                 
               if rb_reset = ‘1’ then 
             
           
        
         
             
                 
               v &lt;= “1110”; 
             
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               else 
             
           
        
         
             
                 
               if (not (v(3) and (not ack1_new))) = 
             
           
        
         
             
                 
               ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘0’; 
             
           
        
         
             
                 
               elsif ok = ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               end if; 
             
             
                 
               v &lt;= vnext; 
             
           
        
         
             
                 
               end if; 
             
           
        
         
             
                 
               end process; 
             
           
        
         
             
                 
               fails(4) &lt;= not b21 ((ok /= ‘0’) or (rb_reset 
             
           
        
         
             
                 
               /= ‘0’) 
             
           
        
         
             
                 
               or (rb_clock /= ‘1’)); 
             
             
                 
               end block; 
             
             
                 
               f6: 
             
             
                 
               block 
             
           
        
         
             
                 
               constant n: integer := 4; 
             
             
                 
               signal v: std_ulogic_vector(0 to n−1) := 
             
           
        
         
             
                 
               “1110”; 
             
           
        
         
             
                 
               signal v_out: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal vnext: std_ulogic_vector(0 to n−1); 
             
             
                 
               signal ok: std_ulogic := ‘1’; 
             
           
        
         
             
                 
               begin 
             
             
                 
               v_out(0) &lt;= ‘0’; 
             
             
                 
               v_out(1) &lt;= v(1) and (‘1’); 
             
             
                 
               v_out(2) &lt;= v(2) and ((req0 and (not req1))); 
             
             
                 
               v_out(3) &lt;= v(3) and ((not ack0_new)); 
             
             
                 
               vnext(0) &lt;= ‘0’; 
             
             
                 
               vnext(1) &lt;= v_out(1); 
             
             
                 
               vnext(2) &lt;= v_out(1); 
             
             
                 
               vnext(3) &lt;= v_out(2); 
             
           
        
         
             
                 
               p: 
             
             
                 
               process 
             
           
        
         
             
                 
               begin 
             
             
                 
               wait until rb_clock&#39;event and rb_clock=‘1’; 
             
           
        
         
             
                 
               if rb_reset = ‘1’ then 
             
           
        
         
             
                 
               v &lt;= “1110”; 
             
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               else 
             
           
        
         
             
                 
               if (not (v(3) and (not ack0_new))) = 
             
           
        
         
             
                 
               ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘0’; 
             
           
        
         
             
                 
               elsif ok = ‘0’ then 
             
           
        
         
             
                 
               ok &lt;= ‘1’; 
             
           
        
         
             
                 
               end if; 
             
             
                 
               v &lt;= vnext; 
             
           
        
         
             
                 
               end if; 
             
           
        
         
             
                 
               end process; 
             
           
        
         
             
                 
               fails(5) &lt;= not b21 ((ok /= ‘0’) or (rb_reset 
             
           
        
         
             
                 
               /= ‘0’) 
             
           
        
         
             
                 
               or (rb_clock /= ‘1’)); 
             
             
                 
               end block; 
             
           
        
         
             
                 
               end rb;