Abstract:
A method for formally verifying the equivalence of an architecture description with an implementation description. The method comprises the steps of reading an implementation description, reading an architecture description, demonstrating that during execution of a same program with same initial values an architecture sequence of data transfers described by the architecture description is mappable to an implementation sequence of data transfers implemented by the implementation description, such that the mapping is bijective and ensures that the temporal order of the architecture sequence of data transfers corresponds to the temporal order of the implementation sequence of data transfers, and outputting a result of the verification of the equivalence of the architecture description with the implementation description.

Description:
CROSS-REFERENCE TO RELATED APPLICATIONS 
     The present application claims the benefit of the filing date of U.S. Provisional Patent Application Ser. No. 61/103,310 filed by the present inventors on Oct. 7, 2008 and U.S. Provisional Patent Application Ser. No. 61/027,635 filed by Jorg Bormann, Sven Beyer and Jens Schönherr on Feb. 11, 2008. The aforementioned provisional patent applications are hereby incorporated by reference in their entirety. 
     STATEMENT REGARDING FEDERALLY SPONSORED RESEARCH OR DEVELOPMENT 
     None. 
     BACKGROUND OF THE INVENTION 
     1. Field of the Invention 
     The present invention relates to the field of the verification of digital hardware. 
     2. Brief Description of the Related Art 
     Functional Hardware Verification 
     The verification of digital hardware is a step in the production of integrated circuits. If the verification of the digital hardware fails to remove all bugs in the digital hardware, a production process for the digital hardware, with its high fixed costs, may need to be restarted and the introduction of a product incorporating the digital hardware into the marketplace will suffer a delay. 
     One step in the design process of digital hardware is functional verification, by which the initial description of a circuit of the digital hardware is checked to see whether the circuit always behaves as intended. A description of the circuit is given as an RTL description in some hardware description language (e.g. VHDL, Verilog, or SystemVerilog). Current verification methods typically do not identify all of the functional bugs in a design of the circuit. The reasons why the functional bugs remain undetected can be classified as follows:
         Unstimulated Bugs: These functional bugs are not found because the stimuli applied to the design of the circuit fail to exercise and propagate the unstimulated bugs to the inputs of a checker of the circuit.   Overlooked Bugs These functional bugs are stimulated and propagated to the inputs of the checker but the checker is not designed to identify the overlooked bugs.   Falsely Accepted Bugs: These functional bugs arise from a consistent misinterpretation of a specification of the design of the circuit by the implementers and the verification engineers.
 
Verification by Simulation
       

     The work horse for functional verification is simulation. Simulation-based verification methods are prone to all three classes of the undetected bugs. Simulation fails to stimulate all of the functional bugs because of the factor of 10 6  or more between the simulator speed and the real-time execution of the circuit under test. Consequently, the simulation cannot deploy all of the stimuli necessary to exhaustively verify the design of the circuit in the project time available. Simulation coverage metrics do not relieve this situation—the simulation coverage metrics can only assist in the allocation of restricted verification capacity across the design of the circuit. 
     The problem of the overlooked bugs is therefore generally handled by verification planning. Verification tasks are identified by examination of the specification of the circuit and the architecture, by relating common design patterns to appropriate assertions, or by asking the designers of the circuit to note particularly important relations between signals in the circuit. The completeness of the resulting verification tasks is typically compromised by human error. Therefore, practitioners keep this verification planning “dynamic” throughout the verification phase in order to capture new insight into unmet verification needs. 
     Formal Functional Verification 
     Formal verification is regarded as an alternative to simulation-based verification. In formal functional verification, so-called properties are proven against the design of the circuit to ensure proper operation of the RTL description. The formal verification uses methods of mathematical proof and therefore acts as though the circuit has been stimulated with all possible input stimuli. See, Browne, Clarke, Dill, Mishra: “Automatic Verification of Sequential Circuits Using Temporal Logic.” Therefore, in the terms of the classification above, the formal verification leads to an avoidance of unstimulated bugs in the design after the formal verification has been completed. 
     Formal verification has recently been complemented by an approach to ensure that a set of the properties precisely examines the entire input/output behaviour of the circuit. The set of properties is then termed “complete”. In the terms of the classification above it avoids overlooked bugs in the design after the verification. 
     Formal Equivalence Verification 
     Besides formal functional verification, there is formal equivalence verification. The goal of the formal equivalence verification is to verify process steps of the design after the RTL description has been designed and verified. The verification of these design process steps requires the comparison of the circuit description before and after the design process step. For example, to verify a synthesis step, the RTL description is formally compared with a synthesized net list. Due to its simple user interface, equivalence checking today is the most widely used approach for comparing two descriptions of the same design. 
     Algorithms used in the formal equivalence verification compare two descriptions of the same design by extracting an automaton from each of these descriptions, by identifying pairs of corresponding input bits, output bits, and state bits in the two automata, and then comparing the next state and output functions of corresponding state and output bits in the two descriptions. This is referred to as combinational equivalence verification. Combinational equivalence verification is only applicable if both circuit representations have the same state encoding. 
     Processor Verification 
     General Task 
     Processors are typically developed such that programmers writing assembler code to be executed by the processor do not need to understand a hardware description of the processor in detail. Instead, it suffices for the programmer to view the processor as though one instruction had been fully executed before the processor begins with the execution of the next instruction. This model of the processor is called the architecture or architecture description of the processor and will be described in more detail below. 
     For reasons of efficiency, the processors are implemented in a way that the processors execute multiple instructions simultaneously, e.g. in a pipeline. This requires that sequentializing mechanisms are designed which make pipeline effects invisible to the user or which secure efficient operation of the processor. Such sequentializing mechanisms are for example forwarding, stalling, or speculative execution and will be described below. These sequentializing mechanisms are represented in the RTL description of the processor. The RTL description will be referred to as the implementation description below. 
     The verification problem for the processors is to show that the implementation indeed executes the programs in the way that the architecture suggests. This verification problem is a functional verification task, as the functional verification task verifies the RTL description including the sequentializing mechanisms. However, this functional verification task can also be viewed as an equivalence verification task between two descriptions of the same circuit, namely the architecture description and the implementation description. Still, this equivalence verification task goes far beyond the approaches of the equivalence verification tasks currently known. The reason for this is that the design step that turns the architecture description of the processor into the implementation description involves human creativity and the introduction of elaborate mechanisms such as pipelining, forwarding, speculative execution of instructions, or stalling. In particular, architecture description and implementation description of the processor differ in the timing of the circuit. The time difference between the completion of one instruction in the implementation description of the processor and the next instruction in the same processor can vary widely. In superscalar processors, the execution of one instruction may even overtake the execution of other instructions in the superscalar processor, such that the order of completion of the instruction execution is different from the sequence of instructions of the program. The detailed temporal relation between the architecture description and the implementation description is typically not important to the programmers. They are interested in a gross average throughput of instructions when writing their programs. 
     The equivalence verification between the implementation description and the architecture description of a processor is exacerbated by interrupts. An interrupt arrives at the processor when the processor receives appropriate values on an input signal. Depending on an internal state of the processor, the processor decides if it accepts the interrupt or not. Upon acceptance of an interrupt, the processor will execute the interrupt. This interrupt execution typically replaces the execution of an instruction, the execution of which was already started by the processor. Part of the interrupt execution is to switch to the execution of another part of the program, the interrupt service routine. 
     During implementation, a decision is made by the designers regarding which of the instructions that the processor executes when an interrupt arrives should be replaced by the execution of the interrupt. This decision must be accounted for during the equivalence verification. 
     Processor Verification 
     In industrial processor verification, the general idea for simulation-based verification is to make both the implementation description and the architecture description execute the same program and then to compare the traffic in the communication between the processor and the data memory in both the implementation description and the architecture description. This approach executes the processor verification by examining the implementation and the architecture based on what is observable at the respective interfaces. Bugs are found when the traffic to the memory of the implementation and the architecture deviate from one another. 
     Programs used to verify the processor are fed into the architecture description and the implementation description. The programs are either specially developed, randomly generated, or derived from application programs, e.g. the booting of an operation system. 
     A problem arising from this so-called “black box” approach is related to interrupts. The comparison requires that the interrupts arrive at the implementation description and the architecture description at corresponding points in time. The exact correspondence between the interrupts in the implementation description and the architecture description is often manually provided by a verification engineers which is tedious and error prone. 
     Often, the simulation-based verification not only examines the processor through its interface signals, but also checks that properties about the relation of internal signals hold. These internal signal properties are temporal logic expressions that are expected to be satisfied for every clock cycle of the implementation and are commonly referred to as assertions. The verification approach using the assertions is termed Assertion Based Verification. The assertions are often provided by the design engineers who develop the implementation description. If the properties are not satisfied, the simulation issues an error or warning message which allows the designer to identify a bug long before the bug becomes observable at the interface signals of the processor. 
     Once a certain level of confidence in the implementation of the processor is reached, self testing programs are also applied which calculate certain results using two different sequences of instructions and compare these certain results. 
     However, as discussed earlier, simulation-based approaches suffer from the risk of undetected bugs, either because the undetected bugs were not stimulated or have been overlooked. 
     Most application of formal verification concentrates on the formal examination of properties which in principle identifies all contradictions to the properties. However formal verification does not account for the underlying problem that the properties may overlook bugs in the sense of the above bug classification. 
     The application of formal verification to processors has already been studied in academia. Burch and Dill developed an idea of control path verification, i.e. verification of those parts in simple pipelines that decide upon how the processor combines which data. See Jerry R. Burch, David L. Dill: Automatic verification of Pipelined Microprocessor Control. CAV 1994: 68-80. However, Burch and Dill did not consider data paths at all, i.e. those parts that actually transfer or combine the data depending on the signals from the control path. The present invention allows for the verification of the entire processor, including the control paths and the data paths. Several extensions to super-scalar or out-of-order processors have been developed. However, the approaches described in these papers only focus on specific parts of specific designs, i.e., they do not offer a complete verification of the implementation description against the architecture description. In addition, automation is typically low and there is no integration with efficient debug environments, as provided in the invention. 
     The most advanced approach to processor verification is based on the completeness approach. To this end, properties that capture the architecture description must be written. These properties are to be proven against the design. It must be shown using the completeness checker that the properties do not overlook bugs. This ensures that upon complete formal verification, no unstimulated or overlooked bugs remain in the design. 
     SUMMARY OF THE INVENTION 
     Formal Verification on an Already Designed Implementation 
     The invention describes a formal verification for the processors that leads to a high quality level with less user input. Instead of developing properties, the designer must only provide the architecture description, protocol information for the communication on a data and instruction bus, and so-called correspondence information that capture information available during the design process. The clear structure of required user inputs allows the formalization, e.g. of the architecture description, in a single work step, which greatly reduces the risk of falsely accepting bugs. 
     The correspondence information is deployed by the method in a failsafe manner: Even if unsuitable correspondence information is provided, verification will not falsely claim that the architecture and the implementation are equivalent. It is to be noted that unsuitable correspondence information can make the verification wrongly report a difference. 
     Formal Verification in Parallel to the Design of the Implementation 
     The resultant verification process can be applied after the processor is fully designed as described in the state of the art. In addition to this post hoc verification, the invention also enables the verification process in parallel with the design process. It allows a step-by-step processor development using a formal proof to verify every step. 
     This approach complements processor development tools that generate the software required to develop programs for the processor from the architecture description [SCLA + 04] [SHNB + 04], as e.g.
         Simulator   Debugger   Assembler   Disassembler   Linker   Compilers
 
Simulation
       

     The method of the invention requires the generation of properties. These generated properties can also be checked in a simulation based approach which is a standard procedure in Assertion Based Verification. This has several benefits over the approach to simulate the architecture description and the implementation description and then to compare the memory traffic in both architecture description and the implementation description:
         A clear and straight-forward mapping of the interrupts of the implementation to the interrupts of the architecture   The identification of the sequence of instructions that the processor executes   If a bug disturbs the execution of an instruction or an interrupt, the bug will be found when the simulator executes the implementation description and evaluates the property that describes the execution of the instruction or the implementation. This is earlier than in the approaches according to state of the art and therefore allows easy debugging. In the state of the art approaches the impact of a bug can be stored in the processor state for a long time before the bug becomes observable which results in ensuing difficulties to locate the bug.   The verification is provably not prone to overlooking bugs in the sense of the classification of undetected bugs.       

     With these characteristics, the approach goes far beyond typical Assertion Based Verification approaches. 
     TERMINOLOGY AND NOTATION 
     The Temporal Logic ITL 
     The invention will be described in the temporal logic ITL which will be presented in the following. However, the invention is not limited to this temporal logic. The procedure of the invention can also be applied using all other linear temporal logics, such as LTL, PSL or SVA. 
     The temporal logic is used for the description of the relationship between behavioural aspects of the implementation description by means of properties. In the following representation, a slight modification of the ITL language, the input language of a property checker [BS01] will be used. In this language, temporal aspects are described by referring to time points. Such time points correspond to cycles in synchronous digital circuits. 
     The core of ITL is comprised of logical lines of one of the following three forms 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 at &lt;time point&gt;: &lt;Boolean condition&gt;; 
               
               
                   
                 during [&lt;time point 1 &gt;, &lt;time point 2 &gt;]: &lt;Boolean condition&gt;; 
               
               
                   
                 within [&lt;time point 1 &gt;, &lt;time point 2 &gt;]: &lt;Boolean condition&gt;; 
               
               
                   
                   
               
             
          
         
       
     
     The first form requires the validity of the Boolean condition at the time point specified, the second for all time points in the interval and the third for at least one time point in the interval. If the interval is empty, the second form is fulfilled trivially and the third is not fulfilled trivially. 
     A Boolean condition at a specific time point T is evaluated for normal operators by evaluating the partial expressions at time T and combining them according to the operator. This evaluation decomposes the partial expressions, until some partial expression is given by some signal, in which case that value of that signal at time T is used. To evaluate a partial expression of the form next(Term, n) or prev(Term, n) the expression Term will be executed at a time point T+n or T−n, respectively. In order to evaluate a partial expression of the form Term @ T′, the term Term is evaluated at the point in time T′. 
     For Boolean expressions, the less or equal operator is written &lt;=, the greater or equal operator is written &gt;=, inequality is written /=, implication is denoted by −&gt;. Intervals are written [a, b] and include the boundaries. For Boolean results, the values 1 and true will be used synonymously, as well as the values 0 and false. 
     Time points are specified relative to an arbitrary but fixed point in time t, or relative to a time variable, which is itself defined relative to t. Time variables are declared by means of a list of expressions 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 T 1  = B 1  + n 1  .. m 1 , 
               
               
                   
                 T 2  = B 2  + n 2  .. m 2 , 
               
               
                   
                 ....; 
               
               
                   
                   
               
             
          
         
       
     
     In these expressions, the B i  are either t or another temporal variable T j  with j&lt;i declared in the above list. An allowed assignment of values to time variables must fulfil the conditions given above, that is B i +n i &lt;=T i &lt;=B i +m i  must be true. m i  can be infinity, in which case the respective declaration is replaced by 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                       T i  &gt;= B i  + n i   
               
               
                   
                 or 
               
               
                   
                       T i  &gt; B i  + n i   
               
               
                   
                   
               
             
          
         
       
     
     Time variables are used to describe how the circuit under examination synchronizes with its environment. For this, expressions of the form 
                                             during [B i  + n i , T i  − 1]:    signal /= value;           at   T i :     signal = value;                        
are used to set a time variable T i .
 
     Logical lines form conditions as follows: In the simplest case, a condition represents a logical line. The succession of two conditions corresponds to their conjunction. 
     The expression 
                                              for each j in m .. n:             Condition(j)           end for each;                        
formed from a parameterized condition should be treated like
 
                                             Condition(m);           Condition(m+1);           ...           Condition(n);                        
It should be the trivially holding condition true, if n&lt;m.
 
     For Boolean expressions, the expression 
                                             for each j in m .. n:             Expression(j)           end for each;                        
should be treated like
 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 Expression(m) and 
               
               
                   
                 Expression(m+1) and 
               
               
                   
                 ... and 
               
               
                   
                 Expression(n); 
               
               
                   
                   
               
             
          
         
       
     
     Partial expressions up to conditions can be summarized in macros, which can have parameters if necessary. 
     A property has the form 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 property &lt;name&gt;; 
               
               
                   
                 for timevars: &lt;time variable declaration&gt;; 
               
               
                   
                 assume: 
               
               
                   
                   &lt;condition 1&gt;; 
               
               
                   
                 prove: 
               
               
                   
                   &lt;condition 2&gt;; 
               
               
                   
                 end property; 
               
               
                   
                   
               
             
          
         
       
     
     &lt;condition 1&gt; is referred to as the assume part, &lt;condition 2&gt; as the proof part of the property. Parts of the assume part will be referred to as assumptions. The property is satisfied, if for all values of t and for all values of the time variables as specified in the &lt;time variable declaration&gt; for which the assume part is satisfied, the proof part is also satisfied. A counter example shows behaviour of the implementation description, a point of time t, and a set of values for the time variables as specified in the &lt;time variable declaration&gt;, that satisfy the assume part but violate the prove part. 
     The logical lines that form an assume part or proof part may be interrupted by cut points of the form “&lt;“&lt;label&gt;”&gt;”. In this case, separate proofs will be executed for every one of the &lt;label&gt; in the assumption. The resultant property is derived by cutting off all ensuing lines in the assume and the proof part. The resulting property will be called a partial property and referred to by &lt;property_name&gt;.&lt;label&gt;. 
     If a property contains an entry “dependencies:” the Boolean macros specified in this entry are to be treated as assumptions for all time points after the reset. 
     left_hook and right_hook are optional entries to the properties. These entries refer to time points with expressions of the form t+&lt;offset&gt; or &lt;TimeVariable&gt;+&lt;offset&gt;. The entries describe, how the properties form chains to match an execution trace in the way described in the next section. 
     TERMINOLOGY 
     The term property will be used for a temporal logic expression that describes behavioural relations between aspects of the circuit behaviour. The examination by a formal verification tool is called a proof. If the formal verification tool decides that the property holds, the circuit shows the behavioural relation for every one of the input stimuli to the circuit. If there is at least one input stimulus that leads to a circuit behaviour that contradicts the behavioural relation, the formal verification tool decides that the property fails. Properties can also be examined by simulation, in which case it cannot be demonstrated that the property holds, because simulation is not strong enough to examine all input stimuli. However, simulation is sufficient to show that a property fails. To examine a property against a design description by a simulator, the design description is simulated with the simulator, and the simulator evaluates the property on the sequences of values generated with the simulator. If the evaluation shows that the property fails, an error message is emitted by the simulator. 
     An execution trace of a circuit is a sequence of values on its inputs, outputs, and internal signals that the circuit can create according to its hardware description. A counter example is an execution trace that contradicts a property. 
     A property is said to match an execution trace for some given instantiation of time variables (including “t”), if both assume and prove part are satisfied by the execution trace for the given instantiation of time variables. If an execution trace is generated by some circuit, and if a property is proven to hold on that circuit, then it suffices to check that the assume part matches to decide whether the whole property matches. 
     A property chain is a sequence of properties P 0 , P 1 , P 2 , . . . . A property chain is said to match an execution trace, if there is an instantiation of all time variables in the properties P 0 , P 1 , P 2 , . . . , such that the properties match the execution trace and such that left hook of property P i+1  equals the right hook of property P i  for every i&gt;=0. 
     An expression E is said to “depend” on some variable V, if V occurs in the syntax that forms the expression E, no matter if V really contributes to the result of the expression. For example, the expression “V and not V or W” depends on V and W. 
     In a preferred embodiment, the present invention is a method for formally verifying the equivalence of an architecture description with an implementation description. The method comprises the steps of reading an implementation description, reading an architecture description, demonstrating that during execution of a same program with same initial values an architecture sequence of data transfers described by the architecture description is mappable to an implementation sequence of data transfers implemented by the implementation description, such that the mapping is bijective and ensures that the temporal order of the architecture sequence of data transfers corresponds to the temporal order of the implementation sequence of data transfers, and outputting a result of the verification of the equivalence of the architecture description with the implementation description. The mapping of the architecture sequence of data transfers to the implementation sequence of data transfers may comprise ensuring that the same data is transferred from or to same address of a data memory. The implementation sequence of data transfers may be described by an access protocol description. The step of demonstrating may comprise during the execution of the same program, behaviour of interrupt signals of the implementation description is demonstrated to be mappable to behaviour of interrupt signals of the architecture description such that the mapping of the architecture sequence signals of data transfers with the mapped interrupt signals corresponds to the implementation sequence of data transfers influenced by the interrupt signals. The step of may also or alternatively comprise the steps of reading correspondence information and generating a plurality of demonstration steps using the read correspondence information, wherein one of the demonstration steps verifies a correspondence of the architecture description with the implementation description subsequent to the execution of a cycle of the same program. The method may use the correspondence information in a way such that the method does not output a false verification for a non-equivalent pair of the architecture description and the implementation description. The correspondence information may include stall conditions of one or multiple pipeline stages of the implementation description, cancel conditions of one or multiple pipeline stages of the implementation description, a classification of one or more of pipeline stages of the implementation description and/or a function for reading a program counter from the implementation description. 
     The correspondence information may comprise one or more virtual registers for mapping values in implementation registers of the implementation description to corresponding architectural registers of the architectural description. The one or more virtual registers may be functions for testing one or more pipeline stages of the implementation description in the order of an instruction sequence, wherein the one or more virtual registers return at least one pipeline value from one of the one or more pipeline stages having relevant data and wherein the one or more virtual registers return, if none of the one or more pipeline stages have relevant data, the value of the implementation register implementing the corresponding architecture register. The one or more virtual registers may be functions generated from one or more sub-functions. The virtual registers may be organized in virtual register files. 
     The demonstration may further comprise checking that each one of cycles of the same program is implemented by a finite number of implementation clock cycles. The cycle of the same program may comprise an instruction or an interrupt. 
     The step of generating the plurality of demonstration steps may comprise the steps of generating properties and verifying the generated properties to either prove all of the generated properties or to identify at least one false one of the generated properties. The step of generating properties may comprise the steps of accessing a property schemata including one or more place holders and replacing the one or more place holders with values from the correspondence information, to thereby generate at least one generated property. The method may cease on the identification of at least one false one of the generated properties. A subset of the generated properties may be created, such that each member property of the subset describes an execution of one of an implementation cycle. The implementation cycle may be either an instruction executed by the implementation description or an interrupt executed by the implementation description. For each one of an implementation cycle there may exist at least one property describing the implementation cycle. The subset of the generated properties may indicate changes in one or more virtual registers as a result of the execution of the implementation cycles. The subset of the generated properties may consist of properties to verify how the implementation requests an instruction, when and how the implementation changes a program counter; if, when and how instruction in the pipeline are cancelled; if, when and which ones of the data transfers of the implementation description are carried out by the implementation; that subsequent to the execution of the instruction the implementation is in a state from which it executes a further implementation cycle. 
     The result of the method may comprise one of: indication of the proof of all of the generated properties, confirmation of the equivalence of the architecture description and the implementation description, and an indication that one of the generated properties is false or a list of the false ones of the generated properties. 
     The architectural description may be an architecture description of a processor and the implementation description may be the implementation description of a processor. 
     The step of reading the implementation description may comprise reading a first portion of the implementation description, the step of reading the architecture description comprises reading a first portion of the architecture description, and the method may further comprise the step of using the correspondence information to verify the equivalence of the first portion of the implementation description with the first portion of the architecture description and, if the equivalence is demonstrated, reading in a further portion of the implementation description and a further portion of the architecture description. 
     In another embodiment, the present invention is a virtual register file that comprises a definition for every stage of a pipeline using signals of an implementation, wherein, when a stage starts executing an instruction, the virtual register file returns one of a special “invalid” value and a value that a corresponding architecture register file has when an architecture description starts executing the instruction. 
     In still another embodiment, the present invention is a method for verifying the equivalence of an architecture description with an implementation description. The method comprises the steps of reading an implementation description, reading an architecture description, reading correspondence information, generating a set of properties, verifying the set of properties to either show that all of the generated properties hold or to identify at least one false one of the generated properties, and outputting a result of the verification of the equivalence of the architecture description with the implementation description. The verifying demonstrates that during execution of a same program with same initial values an architecture sequence of data transfers described by the architecture description is mapped to an implementation sequence of data transfers implemented by the implementation description, such that the mapping is bijective and ensures that the temporal order of the architecture sequence of data transfers corresponds to the temporal order of the implementation sequence of data transfers. The verifying the set of properties comprises simulating the implementation properties on a result of the simulation. The mapping of the architecture sequence of data transfers to the implementation sequence of data transfers comprises ensuring that the same data is transferred from or to same address of a data memory. The implementation sequence of data transfers is described by an access protocol description. The demonstrating may comprise during the execution of the same program, behaviour of interrupt signals of the implementation description is demonstrated to be mappable to behaviour of interrupt signals of the architecture description. 
     In yet another embodiment, the present invention is a method for the generation of a full set of functional coverage points for simulation based verification of a processor implementation. The method comprises the steps of reading the architecture description, reading an access protocol description, reading correspondence information, generating a set of coverage points, turning the set of coverage points into simulation monitors and including the simulation monitors in a simulation. 
     Still other aspects, features, and advantages of the present invention are readily apparent from the following detailed description, simply by illustrating a preferable embodiments and implementations. The present invention is also capable of other and different embodiments and its several details can be modified in various obvious respects, all without departing from the spirit and scope of the present invention. Accordingly, the drawings and descriptions are to be regarded as illustrative in nature, and not as restrictive. Additional objects and advantages of the invention will be set forth in, part in the description which follows and in part will be obvious from the description, or may be learned by practice of the invention. 
    
    
     
       BRIEF DESCRIPTION OF THE DRAWINGS 
       For a more complete understanding of the present invention and the advantages thereof, reference is now made to the following description and the accompanying drawings, in which: 
         FIG. 1  shows an exemplary process according to the invention. 
         FIG. 2  shows the timing in the property scheme simple instruction. 
         FIG. 3  shows the timing relation of the jump instruction. 
         FIG. 4  shows the timing structure of a possible generated interrupt property. 
         FIG. 5  shows two of the main properties P j  and P j+1  generated from the property schemata simple instruction. 
         FIG. 6  shows the general case of the property generated from property schemata&#39;s reset. 
         FIG. 7  shows the general case of one of the properties generated from the property schemata&#39;s. 
         FIG. 8  shows the design of a processor 
     
    
    
     DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENTS 
     Conceptual Background of the Invention 
     Architecture Description 
     The architecture description of a processor presents a view provided by, for example, the programmer&#39;s manual. The architecture description takes the view of the processor in which the processor executes every instruction fully before the processor starts with the next instruction. The architecture description can therefore be viewed as a synchronous automaton that executes one instruction in every clock cycle. Besides instructions, the architecture also executes interrupts. Interrupts are signalled to the architecture description by the architecture interrupt signals. If the processor accepts an interrupt, the processor executes the interrupt instead of the instruction. The execution of one interrupt or one instruction will be termed an “architecture cycle”. 
     The interface of the architecture is given by signals that communicate with the data memory or the instruction memory, by interrupt signals, and the reset signal. The state of the architecture description typically contains
         a program counter that provides the address of the instruction to be executed.   one or multiple register files upon which the instructions act. These register files are arrays of registers and may degenerate to a single register. The register files store, for example, data with which the processor deals. Another example is the program status word with Boolean variables that provide information about the last execution of an instruction (e.g., a Boolean variable to highlight that the last instruction execution generated an overflow, or a Boolean variable to show that the result of the last instruction is zero). The register files may also store information required to decide upon acceptance of interrupts or to execute interrupts as e.g. the interrupt priority, an interrupt mask (to switch off some interrupts) etc.       

     The instructions of the architecture description can be classified into simple instructions and jump instructions. For simple instructions, the program counter is updated similarly to a counter. Jump instructions often specify a condition about the state of the architecture description. During the execution of jump instructions, the condition will be evaluated on the state of the architecture description. If the condition is satisfied, the architecture program counter will be set to some fresh value specified in the instruction. In the case that the condition of the jump instruction is satisfied the jump is referred to as being “taken”. If the condition is not satisfied, the jump is referred to as being “not taken”. In this latter case the architecture program counter is updated such as the update by a simple instruction. 
     Similarly, the execution of an interrupt makes the architecture description set the architecture program counter to the start address of the interrupt service routine. 
     Implementation 
     Processors are typically not implemented by the automaton described in the architecture description. Instead, the instruction execution is pipelined. The RTL implementation is therefore capable of handling multiple ones of the instructions simultaneously, each ones of the instructions being in different phases of their execution. A common class of processors consists of one pipeline, and this is the class upon which the invention will be exemplified.  FIG. 8  shows such a processor consisting of a single pipeline. It should be noted that the invention is not limited to such pipelines. 
     The pipeline is said to consist of stages 1 . . . n. Stage 1  301  is chosen, such that stage 1 contains the program counter. The execution of an instruction consists of phases and each phase is executed in one stage of the pipeline stages. For example, stage 1 issues the read request to the instruction memory  312 . Stage 2  302  receives the instruction  313  that the instruction memory returns. Furthermore, stage 2 reads the operands  310  that an instruction is going to combine. 
     Stage 3  303  combines the operands according to the instruction specification. This gives a result that is stored in stage 4  304  until the result is written back to the implementation register file  305 . 
     An instruction is executed by the implementation by moving along the pipeline stages and executing the related phases of the instruction execution. It is said that an instruction is in a stage when the signals that implement this stage are controlled by the execution of the instruction. Therefore, the instruction is first in stage 1, then the instruction moves to stage 2, then to stage 3 and so forth until the instruction reaches the last pipeline stage, at which the instruction execution is finished. If an instruction is allowed to move from a stage s to the next stage s+1 is determined by stall signals  307 . If the stall signals are 0, the instruction may move from stage s to the next pipeline stage, otherwise the instruction has to remain in the pipeline stage s. 
     Processor pipelines execute interrupts by replacing the execution of an instruction with the execution of an interrupt that is signalled by interrupt inputs  314 . Some stage is designed such that it is responsible for accepting an interrupt, and if the interrupt is accepted, the execution of the instruction in that stage and the execution of all instructions in stages with lower stage numbers is cancelled by activating the cancel signals  308 . Cancelling means that the processor acts after the cancelling, as if the instructions had never been present. The interrupt is then executed in phases instead of the highest instruction that is cancelled. 
     The execution of one instruction or of one interrupt will be referred to as an implementation cycle. A program cycle shall be the collective term for an implementation or an architecture cycle 
     Processor implementations contain register files which will be referred to as the implementation register files  305 . These implementation register files will be updated with the results of an implementation cycle when the instruction execution or interrupt execution is in the stage  304  at which this update should happen. This stage is referred to as the writeback stage of the implementation register file. The operands for an instruction are generally read from the implementation register file. Exceptions are related to pipeline hazard that will be described below. 
     Results of the instructions are often computed in a stage before the writeback stage. Then the result needs to be shifted through the stages between the stage where the result is computed and the writeback stage. This is done by some of the signals that implement the stages. 
     Because of this shifting of the result through the pipeline stages, the result is written back into an implementation register file  305  some time after the result was created. This may lead to the situation that an instruction after the instruction that generated the result needs the result before the result is written into the implementation register file. This situation is referred to as a pipeline hazard. To resolve the pipeline hazard, special forwarding hardware  309  is required to make such results still residing in the pipeline available to the next instruction. If the result is not yet produced, the execution of the second instruction must be delayed. This is achieved by stalling the pipeline. 
     Most jump instructions of a processor are conditional, i.e. a condition decides whether the PC is incremented in the normal way or is set to a new address. Consequently, the processor is uncertain about the next instruction after the jump until the condition is executed. The execution of the condition may be in a later stage. To avoid wasting time, the processor may speculate about the next instructions and remove them if the condition execution shows that this speculation is incorrect. This removal is achieved by cancelling the instruction from the stages. Cancelling also ensures that interrupts modify the sequence of instructions appropriately. 
     Equivalence 
     The invention verifies the equivalence between the architecture description and the implementation description. The exact notion of equivalence will be presented here. 
     To define the equivalence between the architecture description and the implementation description, the architecture description will be treated like a synchronous circuit that executes exactly one instruction or interrupt every clock cycle (referred to as an architecture cycle). The architecture cycles will be numbered starting with the architecture state AS @1 after reset. After the i-th (i=1, 2, 3, . . . ) architecture cycle, the processor is in architecture state AS @ i+1. 
     The architecture description and the implementation description start from equal reset states and execute the same program, i.e. both obtain the same instructions from the same addresses of the instruction memory. Moreover, the data memories initially store the same data at the same addresses, such that the architecture description and the implementation description receive the same data from the same data memory addresses until the architecture description and the implementation description write to these addresses. As long as no interrupts arrive, the implementation description is said to be equivalent to the architecture description if both the architecture description and the implementation description create the same sequence of requests to the data memory for every possible program stored in the instruction memory. This means, that there must be a mapping from the sequence of data transfers described by the architecture description to the sequence of data transfers described by the implementation description. This mapping must map the i-th data transfer of the architecture description to the i-th data transfer of the implementation description. The mapping must ensure that every data transfer described by the architecture description and the mapped data transfer of the implementation description execute the data transfers in the same direction, to the same address, and they transfer the same data in case of write requests. 
     If such a mapping exists, the sequence of data transfers described by the architecture description and by the implementation differ in timing and with respect to the protocol, but are equal with respect to the direction of the requests (whether read or write), the addresses of the requests, and the data written by write requests. 
     This notion of equivalence must be refined to accommodate interrupts. There must be an interrupt mapping that maps a behaviour (i.e. signal values over time) on the interrupt input signals irpt of the implementation description to a behaviour on the interrupt input signals IRPT of the architecture description. 
     This mapping must be such that the implementation that receives the behaviour of the interrupt input signals irpt and the architecture that is interrupted by interrupt signals IRPT both produce the same sequence of requests to the data memory. If there is such a mapping, then the implementation description is said to be equivalent to the architecture description. The invention is capable of describing the mapping once the mapping has been shown to exist. 
     Approach 
     To verify the equivalence, the approach generates properties that fully describe how a single instruction is executed by the whole pipeline or how an interrupt is executed by the whole pipeline. These generated properties (including a property about reset) will be termed “main properties” below. There might be several main properties for one given instruction or interrupt if the execution is best described using different cases (e.g. conditional jump where the condition is satisfied or not satisfied). 
     Besides main properties, auxiliary properties and lifeness properties are generated. An aspect of this invention is that the auxiliary properties and the main properties generated by this approach fit together in a well-defined way: Given any legal input trace, it is possible to predict the implementation behaviour based only on the generated main properties and the generated auxiliary properties. This is a general quality criterion. Its advantages and requisite tools have been documented in European Patent Application 05 020 124.3 about the completeness checker. For the purpose of this invention, the dedicated application of completeness checking tools is not necessary, because the properties satisfy this criterion by construction. 
     The contents of each generated main property include that the generated main property:
         assumes that the processor is in a state from which the processor can start with the execution of an instruction;   proves the generation of accesses to instruction memory;   assumes that the fetched instruction and a state of the processor satisfy the conditions about the situation for which the property is made;   proves that the program counter is correctly updated;   proves that the processor returns into a state from which it can execute the next instruction;   proves that the result is computed according to the architecture description and that the signals that control the forwarding are correctly set;   proves that the program status word is correctly modified;   proves that the result is correctly written back to the appropriate register file (or register); and   proves that the implementation correctly determines direction of data bus transfers, its addresses and—in case of write transfers—the write data.
 
Virtual Registers and Register Files
       

     A further element in the invention is the “Virtual Register” or the “Virtual Register File”. This concept serves to verify all issues related to architecture registers such as program status word, register file, or even interrupt configuration registers. 
     Throughout this description, architecture registers are regarded to be organized in arrays, the register files. If a register is not organized in an array, it will be treated as if it belonged to a register file with only one element. Consequently virtual registers are organized in virtual register files. 
     A virtual register file is a macro that maps the implementation state to the registers of the architecture state. For an instruction in a stage s the virtual register provides the register file values that the instruction in the stage s observes in the architecture before the instruction in the stage s gets executed. Therefore, the virtual register file is defined depending on the pipeline stages. 
     The virtual register file is built so that the virtual register file tests the pipeline stages in the order in which the instructions in the pipeline stages appear in the program. Each stage is examined to see whether the stage contains data for the implementation register that is not yet written back. The data found in the first stage is returned. It may be that one of the stages contains an instruction that announces the creation of data as the instruction proceeds further through the pipeline. In this case, the virtual register returns a special value “invalid” that denotes that the respective data is currently not available. If none of the examined stages contains or at least announces data, the data from the corresponding implementation register is returned. 
     For single pipeline processors, the stages are examined in order of ascending numbers, starting with stage s+1, because there cannot be any other instruction sequence. Therefore, the virtual register file need not be provided by the user. For more elaborate superscalar processors with multiple ones of the pipeline stages and the possibility that one instruction overtakes another one of the instructions executed in another one of the pipelines, the instruction sequence must be deduced from the processor state. 
     An exemplary process according to this invention is shown in  FIG. 1 . In a first step  201  the implementation description is read in and transformed into an internal format  202 . The implementation description may be given by some hardware description language that, for example, represents RTL. Other implementation descriptions could be net lists or cycle-accurate behavioural descriptions. 
     The architecture description is read in step  203 . The content of the architecture description follow the rules described below. In step  204 , the correspondence information  204  is read in. The correspondence information describes design decisions and establishes the correspondence between the implementation description and the architecture description and will be described below. In a property generation step  205  a set of properties  206  is generated from the architecture description, the implementation description  202  and the correspondence information read in previously. 
     The set of generated properties is then verified against the implementation description in step  207 . The verification step  207  can be executed with a formal verification tool, e.g. a model checker or property checker, but the invention also covers any other means to verify properties against an implementation, e.g. simulation. For the formal verification, the verification step  207  may terminate, once a property of the set of generated properties is found that cannot be proven to hold. The steps  204 ,  205 , and  207  demonstrate the equivalence between architecture description and the implementation description. 
     The result of the verification is displayed in steps  209  in case of equivalence between the architecture description and the implementation description and in step  208  in case of one of the properties failing the proofs that potentially indicates a lack of equivalence between the architecture description and the implementation description. In the latter case, i.e. lack of equivalence, diagnosis information is returned to allow the designer to identify bugs in the implementation description or the architecture description or in the correspondence information. 
     Usage Models 
     For formal verification of a previously designed implementation, the method of  FIG. 1  will be executed once and the verification step  207  will be implemented by a property checker. 
     For the formal verification in parallel with the design of the implementation, the process of  FIG. 1  will be executed repeatedly with the same correspondence information and an increasing number of instructions described in the architecture description. The number of instructions described in the architecture description entries mirrors the state of the development of the implementation. With this approach, the development of a processor may start with central mechanisms such as forwarding and the generation of stalls, and then stepwise extend the development with support of interrupts and with instructions. The advantage of this example is that every step of the processor design can thus be verified and errors in the processor design can be corrected early in the design cycle of the processor. 
     For simulation-based verification, the step  207  is implemented by checking the generated properties in a simulation with procedures common to Assertion Based Verification. 
     Architecture Description 
     The architecture description represents an automaton with inputs in, outputs out, states AS (composed of a plurality of architecture registers and the program counter), a next state function NSTATE, and an output function OUT. 
     The automaton starts with a state AS @1 with initialization values, and receives inputs in @1, in @2, in @3, . . . . The automaton defines a sequence of state values AS @2, AS @3, . . . and a sequence of output values out @1, out @2, out @3, . . . by out @ i=OUT(AS @ i, in @ i) and AS @ i+1=NSTATE(AS @ i, in @ i). The transitions of the automaton will be referred to as architecture cycles. The j-th architecture cycle is the one that consumes the input in @ j and produces the state AS @ j+1 and the output out @ j. 
     The architecture description contains the following inputs and outputs, grouped into interfaces: 
     Instruction Memory Interface 
     IMEM_ADDRESS: an output providing an instruction address to the instruction memory. It is assumed that under this instruction address, an instruction can be found. 
     IW: An input providing the instruction word read from the instruction memory for the instruction address IMEM_ADDRESS that was presented in the same memory transaction. 
     Data Memory Interface
         DMEM_ADDRESS: An output providing the data address to the data memory.   DMEM_ACCESS_VALID: A bit output to validate an access to the data memory.   DMEM_RW: A bit output to differentiate between read (‘0’) and write (‘1’) accesses to the data memory.   DMEM_WDATA: An output providing the data written to the data memory in that cycle.   DMEM_RDATA: An input providing the data returned from the data memory for the access in the same memory transaction, in case that DMEM_RW is ‘0’.
 
The behaviour on this data memory interface is captured in the macros:
       

     
       
         
               
               
             
               
               
             
               
               
             
               
               
             
           
               
                   
               
             
             
               
                 DMEM_IDLE := 
                 DMEM_ACCESS_VALID = ‘0’; 
               
               
                 DMEM_READ(addr) := 
                 DMEM_ACCESS_VALID = ‘1’ 
               
             
          
           
               
                   
                 and 
               
               
                   
                 DMEM_ACCESS_RW = ‘0’ and 
               
               
                   
                 DMEM_ADDRESS = addr; 
               
             
          
           
               
                 DMEM_WRITE(addr, wdata) := 
                 DMEM_ACCESS_VALID = ‘1’ 
               
             
          
           
               
                   
                 and 
               
               
                   
                 DMEM_ACCESS_RW = ‘1’ and 
               
               
                   
                 DMEM_ADDRESS = addr and 
               
               
                   
                 DMEM_WDATA = wdata; 
               
               
                   
                   
               
             
          
         
       
     
     Interrupt Interface 
     IRPT: An set of input signals related to interrupts, such as e.g. the signal over which interrupts arrive. 
     Architectural States 
     The states of the automaton are given by architecture register files (which are arrays of architecture registers that may degenerate to a single architecture register) and the architecture program counter PC. Elements of architecture register files will be referred to as R[k]. 
     Architecture Transitions, i.e. Instructions Interrupts and Initialization 
     The transactions of the automaton are given by the list of architecture description entries. There is one architecture description entry for initialization, one architecture description entry for interrupt execution, and multiple numbers of architecture description entries to describe instruction execution. 
     All of the architecture description entries consist of a condition TRIGGER m  and an activity block ACT m . The activity block describes if and how the architecture registers and the program counter are updated if the condition TRIGGER m  is satisfied. The architecture description entry for m=0 describes the interrupt execution, the architecture description entries for m&gt;0 describe the execution of instructions, and the architecture description entry consisting of ACT init  and TRIGGER init  describe the initialization of the processor. 
     The architecture description entry for the initialization contains a condition TRIGGER init  with a reset behaviour and an activity block of the form 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 ACT init  = 
               
               
                   
                   PC = init PC  and 
               
               
                   
                 R 1 [k 1 ] = init R1,k1  and 
               
               
                   
                 R 2 [k 2 ] = init R2,k2  and 
               
               
                   
                 ... 
               
               
                   
                   
               
             
          
         
       
     
     The architecture description entry for the initialization provides the initialization values for the architecture state, i.e. AS @1, consisting of the initialization value for the architecture program counter PC @1 and all initialization values for all architecture registers R[k] @1. 
     The interrupt architecture description entry contains a condition TRIGGER 0  that may depend on the architecture registers and the interrupt inputs IRPT of the architecture, but not on PC, IW or DMEM_RDATA. The corresponding activity block ACT 0  has the form of a conjunction. This conjunction contains one of the following two register file entries for every register file, and update entry for the PC, and one of the three possible data memory entries, as described in the following. The register file entry for register file R either defines that R gets updated at register address INDEX 0,R  with value UPDATE 0,R : 
                                             ASSIGN 0,R  :=           for each k in the index_range of R             if k = INDEX 0,R               then next(R[k]) = UPDATE 0,R               else next(R[k]) = R[k]           end for each                        
where INDEX 0,R  and UPDATE 0,R  may depend on the architecture registers, the PC, DMEM_RDATA and on the architecture interrupt inputs IRPT, or it defines that the register file preserves its value
 
                                             NO_ASSIGN R  :=           for each k in the index_range of R             next(R[k]) = R[k]           end foreach                        
The update entry for the PC is of the form
 
                                             ASSIGN 0,PC  :=           next(PC) = UPDATE 0,PC                          
where UPDATE 0,PC  may depend on the architecture registers, DMEM_RDATA and on the architecture interrupt inputs IRPT.
 
     The data memory entries are either of the form 
                                                 DMEM_IDLE           or               DMEM_READ(ADDR 0 )           or               DMEM_WRITE(ADDR 0 , WDATA 0 )                        
with data memory addresses ADDR 0  and write data WDATA 0  that may depend on the architecture registers, the PC, and on the architecture interrupt inputs IRPT.
 
     DMEM_RDATA may only occur in the activity block ACT 0 , if DMEM_READ(ADDR 0 ) is specified in this activity block. 
     The instruction entries (m&gt;=1) consist of a condition TRIGGER m  and an activity block ACT m . The condition is of the form 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER m  := 
               
               
                   
                 not TRIGGER 0  and 
               
               
                   
                 TRIGGER_IW m  and 
               
               
                   
                 TRIGGER_STATE m   
               
               
                   
                   
               
             
          
         
       
     
     TRIGGER_IW m  may only depend on the architecture instruction word IW. TRIGGER_STATE m  may only depend on the architecture registers, the PC, DMEM_RDATA, and IW. 
     TRIGGER_IW m  describes how the opcode of the instruction is decoded from IW. If the description of the instruction execution requires further subdivisions depending on the architecture state, conditions about the architecture state are captured in TRIGGER_STATE m . Such subdivision is necessary to describe the jump instructions or the instructions that could jump into error correction routines in case the instructions cannot be properly executed. 
     The activity block is similar to the form described above for the activity block of interrupts, except that all of the macros, and in particular the macros INDEX m,R , UPDATE m,R , ADDR m , and WDATA m  may depend on all architecture registers, the PC, and IW and must not depend on the architecture interrupt inputs IRPT. INDEX m,R  and UPDATE m,R  may additionally depend on DMEM_RDATA, if the activity block specifies DMEM_READ(ADDR m ). 
     UPDATE m,PC  may depend on all architecture registers, the PC, and IW, but not on DMEM_RDATA. 
     The references to any register file in the TRIGGER_STATE m , INDEX m,R , UPDATE m,R , UPDATE m,PC , ADDR m  and WDATA m  functions for one architecture specification entry shall be enumerated as follows: The macros TRIGGER_STATE m , INDEX m,R , UPDATE m,R , UPDATE m,PC , ADDR m  and WDATA m  are decomposed into sub expressions. Some of these sub expressions will be references to an architecture register file, i.e. they are of the form R[&lt;index function&gt;]. These references will be enumerated for every architecture entry m. The index function &lt;index function&gt; will be referred to as VINDEX m,i , where i is the number of the enumerated register file accesses. 
     For example, the function UPDATE m,R =R1[IW[3:0]]+R2[IW[7:4]] has two register file accesses, one to R1 and one to R2, with the functions VINDEX m,i =IW[3:0] and VINDEX m,i+1 =IW[7:4]. 
     The architecture description must satisfy a consistency condition of the form that the architecture description is complete for every instruction. This consistency condition requires, that the conditions TRIGGER_STATE about the architecture state of all architecture description entries that belong to the same TRIGGER_IW form a full case split, i.e. disjunction of the conditions TRIGGER_STATE that belong to the same TRIGGER_IW is always satisfied. 
     Constraint no_reset 
     A Boolean macro no_reset that describes how the reset is kept inactive must be provided. This Boolean macro will be assumed in all proofs, except for the proof about the reset behaviour. 
     Access Protocol Description for Instruction and Data Memory 
     The implemented pipeline is expected to have two memory ports, one port to read instructions and one port to read or write data. The protocol at both ports is described in relation to the pipeline operation. For each one of the port, the number of a pipeline stage has to be provided together with macros that yield direction, address, and—if applicable—write data when the stage does not stall. Moreover, a possibly different stage has to be provided together with macros that yield the read data in case of a read access. 
     For simple protocols, the requested macros can be defined depending on the processor inputs and the processor outputs that form the instruction or data bus. More complex protocols require bus interface modules between the pipeline and the bus ports. In this case the interface between the pipeline and the bus interface modules will be characterized with the access protocol description. If desired, a verification of the bus interface modules could be executed to show that addresses and data are correctly transferred. 
     The access protocol description must describe the pipeline stages involved and the signal behaviour. The pipeline stages are provided by a constant. To this end, the pipeline stages are assumed to be numbered consecutively from 1 to n
         The constant ia denotes the number of the stage at which the instruction address is sent to the instruction bus. It is &gt;=1.   The constant iv is to be chosen &gt;=ia. The constant iv denotes the number of the stage at which the instruction returns from the instruction bus. Often the constant iv is equal to ia+1. In the context of asynchronous memory, the constant iv could take the value of the constant ia.   The constant da describes the number of the stage at which the data memory accesses are started, and at which the address and—if applicable—the write data is provided. As memory accesses cannot be cancelled, it is necessary that the stage da cannot be cancelled neither by interrupts nor by jump instructions.   The constant dv describes the number of the stage at which the read data returns from the data memory. For asynchronous memories, the constant dv may be equal to the constant da, otherwise it will take the value &gt;=da.       

     For the instruction fetch, a Boolean macro ibus_read(address) must be provided to describe the behaviour of the instruction memory interface signals at the time when the instruction is in the stage ia and is allowed to move to the next stage. This Boolean macro ibus_read(address) may only depend on the interface signals to the instruction memory. A Boolean macro ibus_idle describes the behaviour of these interface signals at any time point, if no read request is to be started. A macro iw specifies the signal or expression that forms the instruction word at the clock cycle, when the instruction is in stage iv and is allowed to move to the next stage. 
     Whenever the stage iv is allowed to move its instruction forward and at this time point the macro ibus_read(address) is satisfied, the implementation executes a read access on the interface to the instruction memory. 
     The situation is similar for the data transfers. A Boolean macro dbus_read(address) must be defined describing the behaviour of the data memory interface signals at the time point when the instruction is in the da stage and is allowed to move to the next stage. The write is described by a Boolean macro dbus_write(address, wdata), and the macro dbus_idle describes the inactivity. A macro dbus_rdata specifies the signal or expression that forms the data read in at the time when the instruction is in a stage dv and is allowed to move forward. 
     Whenever the stage dv of the implementation allows the movement of the instruction forward that the stage dv currently processes and at this point of the macro dbus_read(address) is satisfied, the implementation executes a read data transfer from the given address in the data memory. Whenever the stage dv allows the movement of the current instruction forward and the macro dbus_write(address, wdata) is satisfied, the implementation executes a write data transfer with the given address and the write data wdata. In all other cases, no data transfer is executed. This allows the extraction of the sequence of data transfers of the implementation as required by the definition of equivalence. 
     External Stall Conditions 
     The processor may be halted by the environment. Reasons for halting the processor could be wait states of the instruction or data memory. To halt the processor, the processor receives one or multiple halt signals from the environment. The conditions under which these halt signals yield the need to halt the processor must be input into the verification by the definition of the macro external_stall by the designer. 
     The verification will assume that the external stall condition external_stall will never be active forever. 
     Correspondence Information 
     The following describes the correspondence information that the designer must provide in step  204  of  FIG. 1 . This correspondence information captures implementation decisions and is easily available from the design process. Moreover, this correspondence information is fail safe in the sense that the correspondence information gets checked by the verification. For the formal verification based examples of the invention, this means that unsuitable correspondence information can make the verification falsely fail, but not falsely succeed. 
     Classification of Pipeline Stages 
     Let the stages of the pipeline be numbered from 1 to n. The roles of the pipeline stages will be described as follows:
         dec is the stage at which the instruction execution really starts. This stage is often the place to which forwarding paths are targeted. Depending on the timing at the instruction bus, the stage dec is often the stage iv or the stage iv+1. In any case the number of the stage dec will be &gt;=iv.   jmp m : For every architecture description entry m, the stage at which the program counter is set to the value of the next instruction is specified. For simple instructions (like arithmetic instructions), this will be 1; for jumps and interrupts, it will be/=1.   int=jmp 0 . This describes the stage that decides if an interrupt is accepted. It has the value jmp m &lt;=int for all m. As access to the data bus cannot be cancelled, it is necessary that the number of the stage da&gt;=int.   vstage m,i : For m&gt;=1 this provides information to the verification about the stage at which the i-th register file access of architecture specification entry m is made, i.e. the register file access that is related to VINDEX m,i . In many cases, all of the forwarding paths target the decode stage of the processor. In this case, the stage vstage m,i =dec for all m and i. However, more elaborate processors allow forwarding to later stages than the stage dec. In this case vstage m,i  may be set to values&gt;dec. It is necessary that vstage 0,i =int for all register values read in TRIGGER 0 , and vstage 0,i &gt;=int for all registers referenced in ACT 0 , the activity block that describes interrupt execution.   writeback R : For every architecture register file R, a write back stage must be provided in the sense of the virtual register file above. This example of the invention requires int&lt;=writeback R  for all register files R.
 
Stall Conditions
       

     For every stage s in [1, n], the condition under which this stage s stalls must be provided in a macro stall s . This macro stall may depend on all implementation signals. 
     If the macro takes the value 1, the stage s stalls which means that the stage s continues processing the current instruction additionally in the next implementation clock cycle. If the macro takes the value 0, the stage s does not stall (sometimes being referred to by “the stage has a nostall”). This means that the stage s passes the current instruction to the next stage (or drops the current instruction, if the stage s is the last stage n in the pipeline). 
     Cancel Conditions 
     For every stage s in [1, n], the condition under which the stage s is cancelled must be provided in a macro cancel s . This macro cancel s  may depend on all of the implementation signals. 
     If the macro takes the value 1, the stage s is cancelled, which means that the instruction is removed from the stage s and the ensuing operation of the implementation pretends that the instruction was never available. 
     It is necessary that if a stage s is cancelled, all stages 1, . . . s−1 are also cancelled. 
     In the following, the abbreviation primary_cancel s =not cancel s+1  and cancel s  will be used for s in [1, n−1]. 
     Full 
     For every stage s in [2, n] a macro full, must be provided that takes the value 1 when the stage s currently executes an instruction or an interrupt and 0 otherwise. The macro full may depend on all implementation signals. 
     Start State 
     A Boolean macro process_new_instruction_state that describes states in which the processor implementation starts the new instructions is provided. 
     Program Counter 
     A macro pc must be provided that maps the implementation states to the value of the implementation program counter pc. This macro pc will typically be defined to be equal to some implementation signal that stores the implementation program counter. 
     Virtual Register File 
     The following information is to be provided for all of the architecture register files R:
         An implementation register file current R (k), at which k is the index to the architecture register file.   A stage writeback R  that provides the stage from which the value will be written into the implementation register file current R .   For every stage s between (and including) dec+1 and the stage writeback R  
           A Boolean macro result_write R,s  that is true if the instruction in stage s will create new data. This macro result_write R,s  returns false when the stage s is empty.   A macro result_dest R,s : If the macro result_write R,s  is true, this macro result_dest R,s  contains the register file address to which the instruction in the stage s write.   A Boolean macro result_valid R,s  that is true if the instruction in stage s has already produced new data, which is now shifted through the pipeline. This macro result_valid R,s  is false when the stage s is empty.   A macro result_data R,s  that yields the result for R of the instruction that is currently in stage s, if the macro result_valid R,s  is true.   
               

     From these macros the verification process creates the virtual register functions as follows: The k-th element of the virtual register file for architectural register file R for an instruction in stage s is given by 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                     data R,writebackR (k) @ t = current R (k) @ t 
               
               
                   
                 and   data R,s (k) @ t = 
               
               
                   
                       (if result_write R,s+1  and result_dest R,s+1  = k 
               
               
                   
                       then result_data R,s+1   
               
               
                   
                       else data R,s+1 (k)) @ t 
               
               
                   
                 for the stages s in [dec, writeback R  − 1]. 
               
               
                   
                   
               
             
          
         
       
     
     The rationale behind this definition is that the stages are checked in increasing order. If a value is still to be written into the implementation register file, this value will nonetheless be the value of the corresponding architecture state. Thus, this function takes part in the verification of forwarding. 
     However, virtual registers may be invalid. This is the case when some of the instructions requires multiple stages to compute a result according to the architecture description. Then it may be that one instruction already requests the value while the current instruction is still in a stage that did not produce this requested value. In this case, the virtual register returns a special invalidity value. A separate macro is used to flag such situations. The separate macro is 
                                 valid R , writebackR (k) @ t = true       valid R,s (k) @ t =           (if (result_write R,s+1  and result_dest R , s+1  = k)           then result_valid R , s+1             else valid R,s+1 (k)) @ t  for the stages s in [dec, writeback R  − 1]         and       valid R,s (k) @ t = false for the stages s in [1, dec−1].                    
Property Generation
 
     The following is a description of the property generation step  205  of  FIG. 1  in which properties are generated. To this end, property schemata are provided. A property schemata is a description of how a property is to be generated. To this end, the property schemata includes meta commands to replicate certain parts of a text of the property or to write other parts of the property text only if a particular condition is satisfied. Moreover, a property schemata provides placeholders for the constants and macros that constitute the access protocol description and the correspondence information. 
     The property generation step  205  can be executed if a specific architecture description and a specific implementation description exists. The property generation step  205  is accompanied with a related correspondence information and a related access protocol description. Then the property generation step comprises: 
     1. Executing all of the meta commands, i.e. replicate or omit parts of the property text as prescribed by the meta commands. 
     2. Instantiating the placeholders with macros of the same name. These macros are provided by the correspondence information, the access protocol description, or the macros are derived from the architecture description in a way that is related to the property schemata.
 
3. replacing all of the placeholders for the numbers of pipeline stages, e.g. ia, iv, da, dv, int, jmp m , that occur in the property text or the macro text, by the actual numbers provided in the access protocol description or the correspondence information.
 
     This provides the generated properties that are to be proven to demonstrate equivalence. 
     Property Schemata for a Simple Instruction 
     For every architecture description entry m&gt;0 with jmp m =1, a property is generated according to the property schemata simple_instruction which will be discussed in this section. 
     The property schemata simple_instruction introduces time points t 1 , t 2 , t 3 , . . . that describe the time points when the pipeline stages that currently execute the current instruction do not stall and allow the current instruction to move forward. 
     An example for an instruction that is handled in this section is an add instruction, for which the architecture description describes that the add instruction sums up the contents of two architecture registers from the architecture register file and writes the result back into the architecture register file 
     To describe the related property, macros trigger 0 , trigger_iw m , trigger_state m , update m,R , index m,R , update m,PC , vindex m,i , addr m  and wdata m  depending on the implementation state are derived from the architecture description macros TRIGGER 0 , TRIGGER_IW m , TRIGGER_STATE m , UPDATE m,R , INDEX m,R , UPDATE m,PC , VINDEX m,i , ADDR m  and WDATA m . 
     The macro triggers is derived from the macro TRIGGER 0 , as follows: The expression of the macro TRIGGER 0  is syntactically decomposed until sub expressions are reached that either reference architecture interrupt inputs from the signal IRPT or one of the enumerated architecture register file accesses of the form R[VINDEX 0,i ], or constants. According to the definition of TRIGGER 0 , these are all possible sub expressions. If the sub expression is a constant, the sub expression is not replaced. If the sub expression is R[VINDEX 0,i ], it is replaced by the expression data R,int (vindex 0,i ), consisting of the virtual register function data R,int  and an address function vindex 0,i  that is generated recursively from VINDEX 0,i  in the way how triggers is generated from TRIGGER 0 . Every reference to an architecture interrupt input is replaced by the corresponding reference to a corresponding implementation interrupt input. The set of all architecture interrupt signals IRPT is replaced by the set of all implementation interrupt signals irpt. The expression with the replaced sub expressions then forms the property macro tigger 0 . 
     The other macros trigger_iw m , trigger_state m , update m,R , index m,R , update m,PC , vindex m,i , addr m  and wdata m  are derived from the macros TRIGGER_IW m , TRIGGER_STATE m , UPDATE m,R , INDEX m,R , UPDATE m,PC , VINDEX m,i , ADDR m  and WDATA m  as follows: The expressions are again syntactically decomposed, until sub expressions are obtained, that are either constants, IW, PC, DMEM_RDATA, or references to architecture register files of the form R[VINDEX m,i ]. If the subexpression is a constant, it will not be replaced. If the subexpression is IW, it will be replaced by iw @ t iv , and iv will be replaced by the number of the pipeline stage according to the access protocol description. If it occurs, the subexpression DMEM_RDATA is replaced by dbus_rdata @ t dv , and dv will be replaced by the number of the pipeline stage according to the access protocol description. PC is replaced by pc @ t 0 +1. R[VINDEX m,i ] is replaced by the virtual register file function data R,vstage(m,i) (vindex m,i ) @ t vstage(m,i)  (to keep the expression legible, vstage(m,i) is written instead of vstage m,i ), where vstage m,i  is specified in the correspondence information. The expression VINDEX m,i  is processed recursively in the same way to create vindex m,i . The expression with the replaced sub expressions then forms the derived macro. 
     The following example illustrates a property schemata, i.e. the example provides a description of how, given the above replacements and the above correspondence information, the property is to be generated. Meta commands are provided to specify repeated or conditional creation of property code. Such meta commands are preceded by #, whereas explaining text will be preceded by //. Regular repetitions are also denoted with “ . . . ”. The lines of the property schemata are numbered to ease reference. 
     The graphical impression of this property is given in  FIG. 2  and shows how the instruction moves down the pipeline according to the stall signals. 
     The entry “dependencies: no_reset” highlights the fact that this property is to be proven under the additional assumption that the reset is kept inactive. Line numbers are introduced to allow reference of parts of the property schemata. 
     The related property schemata reads 
     
       
         
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
               
             
           
               
                   
               
             
             
               
                   
                 property simple_instruction; 
               
               
                   
                 dependencies: no_reset; 
               
               
                   
                 for time_points: 
               
               
                 5 
                   t 0  = t, 
               
               
                   
                   t 1  &gt; t 0 , 
               
               
                   
                   t 2  &gt; t 1 , 
               
               
                   
                   ... 
               
               
                   
                   t n  &gt; t n−1 ; 
               
               
                 10 
               
               
                   
                 assume: 
               
               
                   
                 // The time points where the instruction moves forward 
               
             
          
           
               
                   
                 at  t 0 : 
                 stall 1  = 0 || cancel 1  = 1; 
               
               
                   
                 during [t 0 +1, t 1 −1]: 
                 stall 1  = 1; 
               
               
                 15 
                 at  t 1 : 
                 stall 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 −1]: 
                 stall 2  = 1; 
               
               
                   
                 at  t 2 : 
                 stall 2  = 0; 
               
               
                   
                 during [t 2 +1, t 3 −1]: 
                 stall 3  = 1; 
               
               
                   
                 at  t 3 : 
                 stall 3  = 0; 
               
               
                 20 
                 ... 
               
               
                   
                 at  t n : 
                 stall n  = 0; 
               
             
          
           
               
                   
                 // assume that no preceding property cancelled this one 
               
             
          
           
               
                   
                 during [t 0 +1, t 1 ]: 
                 cancel 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 ]: 
                 cancel 2  = 0; 
               
               
                 25 
                 during [t 2 +1, t 3 ]: 
                 cancel 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: 
                 cancel n  = 0; 
               
             
          
           
               
                 30 
                 // assume that the processor is ready to execute next instruction 
               
             
          
           
               
                   
                 at  t 0 : 
                 process_new_instruction_state; 
               
             
          
           
               
                   
                 // assume that instruction execution is not interrupted. 
               
             
          
           
               
                   
                 during [t 0 +1, t int ]: 
                 not trigger 0 ; 
               
             
          
           
               
                 35 
                   
               
               
                   
                 &lt;fetch&gt; // This is a cut point, see ITL section 
               
               
                   
                 // Assume that iw contains the instruction 
               
               
                   
                 // that should be handled in this property. 
               
             
          
           
               
                 40 
                 at  t iv : 
                 trigger_iw m ; 
               
               
                   
                 &lt;validate_regs&gt; 
               
               
                   
                 at  t dec : 
                 trigger_state m ; 
               
               
                 45 
               
               
                   
                 prove: 
               
               
                   
                 at  t ia : 
                 ibus_read(pc @ t 0 +1); 
               
               
                   
                 &lt;fetch&gt; 
               
               
                 50 
               
             
          
           
               
                   
                 // Prove that the virtual register file values are valid 
               
               
                   
                 // whenever they are to decide upon trigger_state. 
               
               
                   
                 # for each reference z to an architecture register file in 
               
               
                   
                   # TRIGGER_STATE m : 
               
             
          
           
               
                 55 
                   at t vstage(m,z) : 
                 valid R,vstage(m,z) (vindex m,z ); 
               
             
          
           
               
                   
                 # end for each; 
               
               
                   
                 &lt;validate_regs&gt; 
               
               
                 60 
                 // Prove that the virtual register file values are valid 
               
               
                   
                 // whenever they are required. 
               
               
                   
                 # for each reference z to an architecture register file in 
               
               
                   
                   # UPDATE m,R , INDEX m;R , ADDR m , or WDATA m : 
               
             
          
           
               
                   
                   at t vstage(m,z) : 
                 valid R,vstage(m,z) (vindex m,z ); 
               
               
                 65 
                 # end for each; 
               
               
                   
                 at  t 1 : 
                 process_new_instruction_state; 
               
               
                   
                 at  t 1 +1: 
                 pc = update m,PC ; 
               
             
          
           
               
                 70 
                 // Prove that the full signals are correctly created. 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 ]: 
                 full 2  = 1; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 full 3  = 1; 
               
               
                   
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: 
                 full n  = 1; 
               
             
          
           
               
                 75 
                   
               
               
                   
                 // Prove that this instruction will not initiate cancels. 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 ]: 
                 primary_cancel 1  = 0; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 primary_cancel 2  = 0; 
               
               
                   
                 ... 
               
               
                 80 
                 during [t n−1 +1, t n ]: 
                 primary_cancel n−1  = 0; 
               
             
          
           
               
                   
                 // For all registers that get updated, prove their correct 
               
               
                   
                 // handling in the pipeline. 
               
               
                 85 
                 # for each register file R with ASSIGN m,R  in the architecture 
               
               
                   
                   # description entry: 
               
               
                   
                   # for each stage s = dec + 1, dec + 2, ... writeback R −1 
               
             
          
           
               
                   
                     at t s : 
                 if result_valid R,s  = 1 
               
               
                   
                   
                 then next(result_valid R,s+1 ) = 1 
               
               
                 90 
                   
                 end if; 
               
             
          
           
               
                   
                   # end for each stage 
               
               
                   
                   # for each stage s = dec + 1, dec + 2, ... writeback R   
               
             
          
           
               
                   
                     during [t s−1 +1, t s ]: 
                 result_write R,s  = 1; 
               
               
                   
                     during [t s−1 +1, t s ]: 
                 result_dest R,s  = index m,R ; 
               
               
                 95 
                     during [t s−1 +1, t s −1]: 
                 if (result_valid R,s  = 1) 
               
               
                   
                   
                 then next(result_valid R,s ) = 1 
               
               
                   
                   
                 end if; 
               
               
                   
                     during [t s−1 +1, t s ]: 
                 if (result_valid R,s  = 1) 
               
               
                   
                   
                 then result_data R,s  = update m,R ; 
               
               
                 100 
                   
                 end if; 
               
               
                   
                   # end for each stage 
               
               
                   
                   at t writebackR   +1:   
                 current R (index m,R ) = update m,R   
               
             
          
           
               
                   
                 # end for each register 
               
               
                   
                 # for each register file R with NO_ASSIGN R  in the arch. entry: 
               
               
                 105 
                   # for each stage s = dec + 1, dec + 2, ... writeback R   
               
             
          
           
               
                   
                     during [t s−1 +1, t s ]: 
                 result_write R,s  = 0; 
               
             
          
           
               
                   
                   # end for each stage 
               
               
                   
                 # end for each register 
               
               
                   
                 # if the architecture description entry contains 
               
               
                   
                 DMEM_READ(ADDR m ) 
               
             
          
           
               
                 110 
                   at  t da : 
                 dbus_read(addr m ); 
               
             
          
           
               
                   
                 # else if it contains DMEM_WRITE(ADDR m , WDATA m ) 
               
             
          
           
               
                   
                   at  t da : 
                 dbus_write(addr m , wdata m ); 
               
             
          
           
               
                   
                 # else // it contains DMEM_IDLE 
               
             
          
           
               
                   
                   at  t da : 
                 dbus_idle; 
               
               
                 115 
                 # end if; 
               
             
          
           
               
                   
                 left_hook: 
                 t 0 ; 
               
               
                   
                 right_hook: 
                 t 1 ; 
               
               
                   
                 end property; 
               
               
                   
                   
               
             
          
         
       
     
     Lines 5 to 9 introduce the time variables t 0 , t 1 , t 2  until t n . The lines 12 to 21 relate these time variables t 0 , t 1 , t 2  until t n  to the points of time when the instruction execution is allowed to move forward. This is done for every stage. The stalls conditions and the cancel 0  condition are provided in the correspondence information. 
     The lines 24 to 28 require that no stage is cancelled while the stage executes the instruction. Again, the requirement is specified for every one of the stages. The cancel i  entries are from the correspondence information. 
     Line 31 is to be filled with the correspondence information. It focuses the examination on the states of controllers that allow the instruction to be started. 
     Line 34 requires that no interrupt is accepted. trigger 0  is to be derived according to the description above. 
     The cut point fetch in line 36 together with its sole proof part in line 47 ensures that the reading of the instruction bus is independent from the actual instruction that is being read. 
     This instruction is decoded by trigger_iw m  in the line 40. trigger_iw m  is defined in the section above. The decoding is related to the time point where the stage does not stall, in which the instruction arrives from the instruction memory. 
     This again introduces a cut point validate_regs, and the related property proves the lines 46 to 56 of the property schemata. These lines ensure that the virtual register file values that are evaluated by the condition trigger_state m  are valid independently from this decision. If trigger_state m  is trivially true, there is nothing more to prove than with the preceding property generated from cut point fetch, because then lines 54 to 55 specify that no entry will be made. 
     Line 62 to 65 of the proof part requires that the virtual register file used to compute the result of the instruction must be valid from the first stage onwards where the pipelined execution of the instruction needs them. 
     Lines 67 ensure that the instruction evaluation returns to the state where the next instruction can be started. Line 68 ensures that this next instruction will be fetched from the right address. 
     Lines 71 to 74 range across all stages and prove that the related full s  macros from the correspondence information yield 1 to show that the instruction is executed. 
     Lines 77 to 80 range across all stages and prove that this instruction will never issue a cancel to the previous stages. 
     Lines 85 to 103 ensure that a virtual register file of every register file that is assigned a value according to the architecture description really receives the right value and correctly propagates it through the pipeline. The corresponding functions are correspondence information. 
     Line 105 to 107 ensures that a register file that does not get updated will be correctly handled. 
     Lines 85 to 107 range across all possible register files. 
     Lines 109 to 115 ensure the right communication with the memory. 
     Jump Instructions 
     For every architecture description entry m&gt;0 with jmp m /=1 a property is generated according to the property schemata jump_instruction. 
     Jump instructions etc. will often lead to two parts of the architecture description. One part of the architecture description describes the behaviour if the condition is satisfied and the jump is taken, the other part of the architecture description describes the behaviour if the condition is not satisfied and the jump is not taken. If the jump is not taken, the program counter PC will be updated in the usual way, i.e. by the number of the bytes that the instruction occupies in the instruction memory. 
     If the jump is taken, the program counter pc will be updated differently. This update of the program counter must wait until the jump instruction is in the pipeline stage jmp m  at which the jump instruction decides whether to take the jump or not. If the jump instruction decides to take the jump, there may be wrongly speculated instructions in the pipeline stages &lt;jmp m  which must be removed by cancelling the wrongly speculated instructions in the pipeline stages &lt;jmp m . 
     Besides the non default update to the program counter pc, the architecture description may specify that the jump instruction updates architecture registers and execute memory traffic in the form described above for simple instructions. Therefore, large parts of the property schemata for the instructions simple_instructions will also occur in the property schemata for the instructions jump instructions. 
     The macros trigger 0 , trigger_iw m , trigger_state m , update m,R , index m,R , update m,PC , vindex m,i , addr m  and wdata m  are derived as described for the property schemata simple_instructions. 
       FIG. 3  shows the timing relation of the jump instruction. The timing relation is shown when the pipeline stages execute the jump instruction. The figure will also show when the pipeline stages are cancelled to remove instructions the execution of which was speculatively started by the processor. 
     To simplify reading, jmp is written in the indices instead of jmp m . 
     
       
         
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
               
             
           
               
                   
               
             
             
               
                 1 
                 property jump_instruction; 
               
               
                   
                 dependencies: no_reset; 
               
               
                   
                 for time_points: 
               
               
                 5 
                   t 0  = t, 
               
               
                   
                   t 1  &gt; t 0 , 
               
               
                   
                   t 2  &gt; t 1 , 
               
               
                   
                   ... 
               
               
                   
                   t n  &gt; t n−1 ; 
               
               
                 10 
               
               
                   
                 assume: 
               
               
                   
                 // The time points where the instruction moves forward 
               
             
          
           
               
                   
                 at  t 0 : 
                 stall 1  = 0 || cancel 1  = 1; 
               
               
                   
                 during [t 0 +1, t 1 −1]: 
                 stall 1  = 1; 
               
               
                 15 
                 at  t 1 : 
                 stall 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 −1]: 
                 stall 2  = 1; 
               
               
                   
                 at  t 2 : 
                 stall 2  = 0; 
               
               
                   
                 during [t 2 +1, t 3 −1]: 
                 stall 3  = 1; 
               
               
                   
                 at  t 3 : 
                 stall 3  = 0; 
               
               
                 20 
                 ... 
               
               
                   
                 at  t n : 
                 stall n  = 0; 
               
             
          
           
               
                   
                 // assume that no preceding property cancelled this one 
               
             
          
           
               
                   
                 during [t 0 +1, t 1 ]: 
                 cancel 1  = 0; 
               
               
                 25 
                 during [t 1 +1, t 2 ]: 
                 cancel 2  = 0; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 cancel 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: 
                 cancel n  = 0; 
               
             
          
           
               
                 30 
                 // assume that the processor is ready to execute next instruction 
               
             
          
           
               
                   
                 at  t 0 : 
                 process_new_instruction_state; 
               
             
          
           
               
                   
                 // assume that instruction execution is not interrupted. 
               
             
          
           
               
                   
                 during [t 0 +1, t int ]: 
                 not trigger 0 ; 
               
             
          
           
               
                 35 
                   
               
               
                   
                 &lt;fetch&gt; // This is a cut point, see ITL section 
               
               
                   
                 // Assume that iw (the freeze variable) contains the instruction 
               
               
                   
                 // that should be handled in this property. 
               
             
          
           
               
                 40 
                 at  t iv : 
                 trigger_iw m ; 
               
               
                   
                 &lt;validate_regs&gt; 
               
             
          
           
               
                   
                 at  t dec : 
                 trigger_state m ; 
               
               
                 45 
               
               
                   
                 prove: 
               
             
          
           
               
                   
                 at  t ia : 
                 ibus_read(pc @ t 0 +1); 
               
             
          
           
               
                   
                 &lt;fetch&gt; 
               
               
                 50 
               
               
                   
                 // Prove that the virtual register file values are valid 
               
               
                   
                 // whenever they are to decide upon trigger_state. 
               
               
                   
                 # for each reference z to an architecture register file 
               
               
                   
                 # in TRIGGER_STATE m : 
               
             
          
           
               
                 55 
                   at t vstage(m,z) : 
                 valid R,vstage(m,z) (vindex m,z ); 
               
             
          
           
               
                   
                 # end for each; 
               
               
                   
                 &lt;validate_regs&gt; 
               
               
                 60 
                 // Prove that the virtual register file values are valid 
               
               
                   
                 // whenever they are required. 
               
               
                   
                 # for each reference z to an architecture register file 
               
               
                   
                   # in UPDATE m,R , INDEX m,R , ADDR m , or WDATA m : 
               
             
          
           
               
                   
                   at t vstage(m,z) : 
                 valid R,vstage(m,z) (vindex m,z ); 
               
               
                 65 
                 # end for each; 
               
               
                   
                 at t 1 : 
                 process_new_instruction_state; 
               
               
                   
                 at t jmp +1: 
                 pc = update m,PC ; 
               
             
          
           
               
                 70 
                 // Prove that the full signals are correctly created. 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 ]: 
                 full 2  = 1; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 full 3  = 1; 
               
               
                   
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: 
                 full n  = 1; 
               
             
          
           
               
                 75 
                   
               
               
                   
                 // Prove that wrongly fetched instructions are cancelled. 
               
             
          
           
               
                   
                 at  t jmp : 
                 primary_cancel jmp−1  = 1; 
               
             
          
           
               
                   
                 // Prove that the cancel creates empty stages 
               
             
          
           
               
                 80 
                 at  t jmp  + 1: 
                 full 2  = 0; 
               
               
                   
                 at  t jmp  + 1: 
                 full 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 at  t jmp  + 1: 
                 full jmp  = 0; 
               
               
                 85 
                 . 
               
             
          
           
               
                   
                 // Prove that this instruction will not initiate further cancels. 
               
               
                   
                 during [t jmp +1, t jmp+1 ]: primary_cancel jmp  = 0; 
               
               
                   
                 during [t jmp+1 +1, t jmp+2 ]:primary_cancel jmp+1  = 0; 
               
               
                   
                 during [t jmp+2 +1, t jmp+3 ]: primary_cancel jmp+2  = 0; 
               
               
                 90 
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]:   primary_cancel n−1  = 0; 
               
               
                   
                 // For all registers that get updated, prove their correct 
               
               
                 95 
                 // handling in the pipeline. 
               
               
                   
                 # for each register file R with ASSIGN m,R  in the architecture 
               
               
                   
                   # description entry: 
               
               
                   
                   # for each stage s = dec + 1, dec + 2, ... writeback R −1 
               
             
          
           
               
                   
                     at  t s : 
                 if result_valid R,s  = 1 
               
               
                 100 
                   
                 then next(result_valid R,s+1 ) = 1 
               
               
                   
                   
                 end if; 
               
             
          
           
               
                   
                   # end for each stage 
               
               
                   
                   # for each stage s = dec + 1, dec + 2, ... writeback R   
               
             
          
           
               
                   
                     during [t s−1 +1, t s ]: 
                 result_write R,s  = 1; 
               
               
                 105 
                     during [t s−1 +1, t s ]: 
                 result_dest R,s  = index m,R ; 
               
               
                   
                     during [t s−1 +1, t s −1]: 
                 if (result_valid R,s  = 1) 
               
               
                   
                   
                 then next(result_valid R,s ) = 1 
               
               
                   
                   
                 end if; 
               
               
                   
                     during [t s−1 +1, t s ]: 
                 if (result_valid R,s  = 1) 
               
               
                 110 
                   
                 then result_data R,s  = update m,R ; 
               
               
                   
                   
                 end if; 
               
               
                   
                   # end for each stage 
               
               
                   
                   at t writeback,R +1: 
                 current R (index R ) = update m,R ; 
               
             
          
           
               
                   
                 # end for each register 
               
               
                 115 
                 # for each register file R with NO_ASSIGN R  in the 
               
               
                   
                 architecture entry: 
               
               
                   
                   # for each stage s = dec + 1, dec + 2, ... writeback R   
               
             
          
           
               
                   
                     during [t s−1 +1, t s ]: 
                 result_write R,s  = 0; 
               
             
          
           
               
                   
                   # end for each stage 
               
               
                   
                 # end for each register 
               
               
                 120 
                 # if the architecture description entry contains 
               
               
                   
                 DMEM_READ(ADDR m ) 
               
             
          
           
               
                   
                   at t da : 
                 dbus_read(addr m ); 
               
             
          
           
               
                   
                 # else if it contains DMEM_WRITE(ADDR m , WDATA m ) 
               
             
          
           
               
                   
                   at t da : 
                 dbus_write(addr m , wdata m ); 
               
             
          
           
               
                   
                 # else // it contains DMEM_IDLE 
               
             
          
           
               
                 125 
                   at t da : 
                 dbus_idle; 
               
               
                   
                 # end if 
               
             
          
           
               
                   
                 left_hook: 
                 t 0 ; 
               
               
                   
                 right_hook: 
                 t jmp ; 
               
               
                 130 
                 end property; 
               
               
                   
               
             
          
         
       
     
     Lines 1 to 71 are equal to the property schemata simple_instruction and are explained there. 
     Line 77 proves that all stages with numbers below the one that currently executes the jump instruction are cancelled. This follows from the definition of primary_cancel given in the section about the cancel macros in the correspondence information. 
     The lines 80 to 83 range across the stage 1 to the stage jmp m  and prove that the cancelled stages are indeed empty. 
     Lines 87 to 91 range across the stages jmp m  to n−1 and ensure that this jump instruction will not issue any further cancel. 
     The lines 94 to 130 in this property schemata equal the lines 84 to 120 in the preceding property schemata and are explained there. 
     Interrupts 
     For the architecture description entry 0 about interrupts, several properties are to be generated according to the property schemata interrupts. This is described by an additional variable h, that takes the values h=1, 2, . . . . 
     An interrupt arrives from outside the processor. In the simplified view of the architecture description, the interrupt arrives simultaneously with some instruction Inst. Whether or not the interrupt is accepted by the processor is decided by the macro TRIGGER 0  (introduced previously) using status of the architecture at a time point before the instruction Inst is executed. The status of the architecture may, for example, indicate whether the interrupt is to be masked (i.e. not observed). 
     The mapping to the implementation description is not straightforward. The pipeline acts on multiple ones of the instructions simultaneously. A determination needs to be carried out which ones of the instructions will be regarded as being the instruction that is to be replaced by the execution of the interrupt. The approach is to define a stage int at which the interrupt is accepted. This stage int is typically the last from which any of the jump instruction can cancel other stages. Therefore, it is necessary that the value of jmp m &lt;=int for all jmp m . 
     If the stage int is full when the interrupt is accepted by the processor, the instruction in this stage int will be replaced. If the stage int is empty, the instruction in the non-empty stage with the highest number&lt;int will be replaced. This highest number of the non-empty stages will be denoted with h below. Note that stage 1 is regarded as being always full (i.e. non-empty). 
     The macro triggers is derived from TRIGGER 0  in the way described for property schemata simple_instruction. The time point when the macro triggers accepts an interrupt will be denoted t irpt . After this time point, the pipeline executes the interrupt in the pipeline stages int, int+1 etc. t int , t int+1 , . . . denote the time points when the interrupt execution is in the respective one of the stages int, int+1, . . . and is allowed to move forward by the stall signals. In many cases t irpt  will be t int , but this is not required. Before t irpt , the time points t 1 , t 2 , . . . t h−1  reflect the time points where the instruction that is in stage h at time t irpt  is allowed to move forward by the stall signal of the respective stage. Moreover, for the ensuing proof, the time points t h , t h+1 , . . . t int−1  are defined to be t irpt . 
     The macros update 0,R , index 0,R , update 0,PC , vindex 0,z , addr 0 , and wdata 0  are again derived from the architecture description macros as follows: 
     UPDATE 0,R , INDEX 0,R , UPDATE 0,PC , VINDEX 0,z , ADDR 0 , and WDATA 0  are decomposed into sub expressions. By definition, these sub expressions are constants, register file accesses of the form R[VINDEX 0,z ], PC, DMEM_RDATA, or the architecture interrupt inputs IRPT. To obtain the derived macros, these sub-expressions are replaced as follows:
         constants are not changed   R[VINDEX 0,z ] is replaced by data R,vstage(0,z) (vindex 0,z ) @ t vstage(0,z) , where vindex 0,z  is generated from VINDEX 0,z  by recursively applying the procedure described here (Note that vstage 0,z  is required to be &gt;=int).   PC is replaced by pc @ t 0 +1 (Note that this is always the program counter PC of the oldest instruction that gets removed by the interrupt).   DMEM_RDATA is replaced by dbus_rdata @ t dv .   An architecture interrupt signal from IRPT is replaced by the corresponding signal in irpt @ t irpt .       

     The expression with the replaced sub expressions then forms the derived macro. 
     The timing structure of a possible generated interrupt property is represented in  FIG. 4 . It shows that the interrupt need not occur together with a stall. 
     There is one property schemata for every value that h can take, i.e. h=1 . . . int. 
     
       
         
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
           
               
                   
               
             
             
               
                 1 
                 property interrupt h ; 
               
               
                   
                 dependencies: no_reset; 
               
               
                   
                 for time_points: 
               
               
                 5 
                   t 0  = t, 
               
               
                   
                   t 1  &gt; t 0 , 
               
               
                   
                   t 2  &gt; t 1 , 
               
               
                   
                   ... 
               
               
                   
                   t h−1  &gt; t h−2 , 
               
               
                 10 
               
               
                   
                   t irpt  &gt; t h−1 , 
               
               
                   
                   t h  = t irpt , 
               
               
                   
                   t h+1  = t irpt , 
               
               
                 15 
                   .., 
               
               
                   
                   t int−1  = t irpt , 
               
               
                   
                   t int &gt;= t   irpt , 
               
               
                 20 
                   t int+1  &gt; t int , 
               
               
                   
                   ... 
               
               
                   
                   t n  &gt; t n−1 ; 
               
               
                   
                 assume: 
               
             
          
           
               
                 25 
                 at  t 0 : 
                 stall 1  = 0 || cancel 1  = 1; 
               
               
                   
                 during [t 0 +1, t 1 −1]: 
                 stall 1  = 1; 
               
               
                   
                 at  t 1 : 
                 stall 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 −1]: 
                 stall 2  = 1; 
               
               
                   
                 at  t 2 : 
                 Stall 2  = 0; 
               
               
                 30 
                 during [t 2 +1, t 3 −1]: 
                 stall 3  = 1; 
               
               
                   
                 at  t 3 : 
                 stall 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 during [t h−2 +1, t h−1 −1]: 
                 stall h−1  = 1; 
               
               
                   
                 at  t h−1 : 
                 stall h−1  = 0; 
               
               
                 35 
               
               
                   
                 during [t h−1 +1, t irpt −1]: 
                 stall h  = 1 and not trigger 0 ; 
               
               
                   
                 at  t irpt : 
                 trigger 0 ; 
               
               
                   
                 during [t irpt , t int −1]: 
                 stall int  = 1; 
               
               
                   
                 at  t int : 
                 stall int  = 0; 
               
               
                 40 
                 during [t int +1, t int+1 −1]: 
                 stall int+1  = 1; 
               
               
                   
                 at  t int+1 : 
                 stall int+1  = 0; 
               
             
          
           
               
                   
                 during [t int+1 +1,t int+2 −1]:stall int+2  = 1; 
               
             
          
           
               
                   
                 at  t int+2 : 
                 stall int+2  = 0; 
               
               
                   
                 ... 
               
               
                 45 
                 during [t n−1 +1, t n −1]: 
                 stall n  = 1; 
               
               
                   
                 at  t n : 
                 stall n  = 0; 
               
               
                   
                 during [t 0 +1, t 1 ]: 
                 cancel 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 ]: 
                 cancel 2  = 0; 
               
               
                 50 
                 during [t 2 +1, t 3 ]: 
                 cancel 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 during [t h−1 +1, t irpt −1]: 
                 cancel h  = 0; 
               
               
                   
                 during [t irpt +1, t int ]: 
                 cancel int  = 0; 
               
               
                   
                 during [t int +1, t int+1 ]: 
                 cancel int+1  = 0; 
               
               
                 55 
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: 
                 cancel n  = 0; 
               
             
          
           
               
                   
                 // assume that the processor is ready to execute next instruction 
               
             
          
           
               
                   
                 at  t 0 : 
                 process_new_instruction_state; 
               
             
          
           
               
                 60 
                   
               
               
                   
                 // Focus h on the highest nonempty stage. 
               
             
          
           
               
                   
                 at  t irpt : 
                 full h+1  = 0; 
               
               
                   
                 at  t irpt : 
                 full h+2  = 0; 
               
               
                   
                 ... 
               
               
                 65 
                 at  t irpt : 
                 full int  = 0; 
               
               
                   
                 prove: 
               
               
                   
                 at t int : 
                 process_new_instruction_state; 
               
             
          
           
               
                 70 
                 // New PC from interrupt 
               
             
          
           
               
                   
                 at t int +1: 
                 pc = update 0,PC ; 
               
             
          
           
               
                   
                 // Prove that the full signals are correctly created. 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 ]: 
                 full 2  = 1; 
               
               
                 75 
                 during [t 2 +1, t 3 ]: 
                 full 3  = 1; 
               
               
                   
                 ... 
               
               
                   
                 during [t h−1 +1, t irpt −1]: 
                 full h  = 1; 
               
               
                   
                 during [t irpt +1, t int ]: 
                 full int  = 1; 
               
               
                 80 
                 during [t int +1, t int+1 ]: 
                 full int+1  = 1; 
               
               
                   
                 during [t int+1 +1, t int+2 ]: 
                 full int+2  = 1; 
               
               
                   
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: 
                 full n  = 1; 
               
             
          
           
               
                 85 
                 // Prove that all instructions in the pipeline get removed 
               
             
          
           
               
                   
                 at  t irpt : 
                 primary_cancel int−1  = 1; 
               
               
                   
                 at  t irpt +1: 
                 full 2  = 0; 
               
               
                   
                 at  t irpt +1: 
                 full 3  = 0; 
               
               
                 90 
                 ... 
               
               
                   
                 at  t irpt +1: 
                 full int−1  = 0; 
               
               
                   
                 at  t irpt +1: 
                 if prev(stall int ) = 0 
               
               
                   
                   
                 then full int  = 0 
               
               
                 95 
                   
                 end if; 
               
             
          
           
               
                   
                 // Prove that the virtual register file values are valid 
               
               
                   
                 // whenever they are required. 
               
               
                   
                 // In the index subscripts vstage R,k  will be written vstage(R,k). 
               
               
                 100 
                 # for each reference to an architecture register file in 
               
               
                   
                   # UPDATE 0,R , INDEX 0,R , ADDR 0 , or WDATA 0 : 
               
             
          
           
               
                   
                   at t vstage(0,z) : 
                 valid R,vstage(0,z) (vindex 0,z ); 
               
             
          
           
               
                   
                 # end for each; 
               
               
                 105 
                 // Prove that there will not be a second interrupt. 
               
             
          
           
               
                   
                 during [t irpt +1, t int ]: 
                 trigger 0  = 0; 
               
             
          
           
               
                   
                 // For all registers that get updated, prove their correct 
               
               
                   
                 // handling in the pipeline. 
               
               
                 110 
                 # for each register file R with ASSIGN 0,R  in the architecture entry: 
               
             
          
           
               
                   
                   at  t int : 
                 if (t irpt /= t int  and result_valid R,int  = 1) 
               
               
                   
                   
                 then next(result_valid R,int+1 ) = 1 
               
               
                   
                   
                 end if; 
               
             
          
           
               
                 115 
                   # for each stage s = int+1, int+2, ... writeback R −1 
               
             
          
           
               
                   
                     at  t s : 
                 if result_valid R,s  = 1 
               
               
                   
                   
                 then next(result_valid R,s+1 ) = 1 
               
               
                   
                   
                 end if; 
               
             
          
           
               
                   
                   # end for each stage 
               
             
          
           
               
                 120 
                   
                   
               
               
                   
                   during [t irpt +1, t int −1]: 
                 if (result_valid R,int  = 1) 
               
               
                   
                   
                 then next(result_valid R,int ) = 1 
               
               
                   
                   
                 end if; 
               
               
                   
                   during [t irpt +1, t int ]: 
                 result_write R,int  = 1; 
               
               
                 125 
                   during [t irpt +1, t int ]: 
                 result_dest R,int  = index 0,R ; 
               
             
          
           
               
                   
                   # for each stage s = int + 1, int + 2, ... writeback R   
               
             
          
           
               
                   
                     during [t s−1 +1, t s ]: 
                 result_write R,s  = 1; 
               
               
                   
                     during [t s−1 +1, t s ]: 
                 result_dest R,s  = index 0,R ; 
               
               
                 130 
                     during [t s−1 +1, t s −1]: 
                 if (result_valid R,s  = 1) 
               
               
                   
                   
                 then next(result_valid R,s ) = 1 
               
               
                   
                   
                 end if; 
               
               
                   
                     during [t s−1 +1, t s ]: 
                 if (result_valid R,s  = 1) 
               
               
                   
                   
                 then result_data R,s  = update 0,R ; 
               
               
                 135 
                   
                 end if; 
               
               
                   
                   # end for each stage 
               
               
                   
                   at t writebackR +1: 
                 current R (index 0,R ) = update 0,R ; 
               
             
          
           
               
                   
                 # end for each register 
               
               
                 140 
                 # for each register file R with NO_ASSIGN R  in the spec entry: 
               
               
                   
                   # for each stage s = dec + 1, dec + 2, ... writeback R   
               
             
          
           
               
                   
                     during [t s−1 +1, t s ]: 
                 result_write R,s  = 0; 
               
             
          
           
               
                   
                   # end for each stage 
               
               
                   
                 # end for each register 
               
               
                 145 
                 # if the interrupt description contains DMEM_READ(ADDR 0 ) 
               
             
          
           
               
                   
                 at t da : 
                 dbus_read(addr 0 ); 
               
             
          
           
               
                   
                 # else the interrupt description contains 
               
               
                   
                   # DMEM_WRITE(ADDR 0 , WDATA 0 ) 
               
             
          
           
               
                   
                   at t da : 
                 dbus_write(addr 0 , wdata 0 ); 
               
             
          
           
               
                 150 
                 # else // no transaction to the data memory 
               
             
          
           
               
                   
                   at t da : 
                 dbus_idle; 
               
               
                   
                 # end if 
               
               
                   
                 left_hook: t0; 
               
               
                 155 
                 right hook:t int ; 
               
               
                   
                 end property; 
               
               
                   
               
             
          
         
       
     
     The generated property describes how an instruction begins executing but is then replaced by the execution of an interrupt. 
     Lines 6 to 9 range across the stages 1 to h−1 and introduce the time variables for the time points when the instruction that is later replaced is allowed to move forward in the pipeline. If h=1, these lines specify no entry. 
     Line 11 introduces the time variable t irpt  at which the interrupt is accepted. Lines 13 to 16 range across all stages from h to int−1 and introduce the related time variables t s . If h=int, these lines 13 to 16 specify no entry. 
     Line 17 specifies the time variable t int  at which the interrupt execution moves forward into the next pipeline stage. This time variable is allowed to coincide with t irpt . 
     Note that all time points of the form t plus some index except t irpt  refer to one of the time points t 0 , t 1 , . . . t n  by evaluation of the index according to the constants introduced in the access protocol description and the correspondence information. But t irpt  is a separate time point that need not be equal to any of the other time points. 
     The lines 20 to 22 range over all stages between int+1 and n and introduce the points of time when the interrupt execution is shifted to the next stage. 
     Correspondingly, the lines 25 to 46 instantiate the time variables with the appropriate time points according to the signal behaviour: The lines 26 to 34 range across the stages 1 to h−1 and degenerate to no entry, if h=1, lines 36 and 37 introduce t irpt  as being the point of time of the interrupt that is accepted when the instruction to be replaced is in stage h. Lines 38 and 39 describe how the interrupt execution waits in stage int until it is shifted forward. Lines 40 to 46 range over the stages int+1 to n and describe how the interrupt execution is shifted forward. 
     Line 69 assumes that the generated property starts in a state from which a new instruction can be executed. 
     Lines 62 to 65 range across the stages h+1 to int and may degenerate to no entry, if h=int. It ensures that the instruction in stage h is indeed the highest one. The full s  macros are specified in the correspondence information. 
     In the proof part, it will be shown in Line 69 that the circuit returns to the state from where new instructions are to be executed. 
     Lines 74 to 77 range over the stages 2 to h and degenerate to no entry, if h=1. They show how the pipeline stages are filled by the instruction that is later replaced by the interrupt execution. The full s  macros come from the correspondence information. 
     The lines 79 to 83 describe how the stages are filled by the execution of the interrupt. 
     Line 86 shows how all stages below the stage int are cancelled. Lines 88 to 93 range over all of the stages 2 to int−1 and prove that the cancel instruction indeed emptied this stage. Line 93 extends the effect of the cancel instruction to stage int, if the interrupt is accepted when the stall macro of stage int is 0. 
     The values of the virtual registers referenced in the macro trigger 0  need to be valid always. This is proven by a separate property according to property schemata interrupt_regs_valid R,k  below. Therefore, it is sufficient to require that the values in the other architecture description macros are valid in the stage where they are needed. This is done in the lines 100 to 103. 
     Line 106 requires that there is some mechanism that prevents the acceptance of another interrupt before the current one shifts to the next stage int+1. 
     Lines 108 to 156 deal with the impact of interrupt execution on the register files and data bus transfers in a manner similar to that described for the lines 84 to 120 of property schemata simple_instruction. 
     Reset 
     To generate the property about the reset values of the implementation, the macro trigger init  was derived from the macro TRIGGER init  by replacing the architecture reset signal with the implementation reset signal. 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 property reset; 
               
               
                   
                 assume: 
               
               
                   
                 at  t: trigger init ; 
               
               
                   
                 prove: 
               
               
                   
                 at  t+1: full 2  = 0; 
               
               
                   
                 at  t+1: full 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 at  t+1: full n  = 0; 
               
               
                   
                 # For each register R[k] 
               
               
                   
                   at t+1:   current R (k) = init_val R,k ; 
               
               
                   
                 # end for each register; 
               
               
                   
                 at  t+1: PC = init_val PC ; 
               
               
                   
                 at  t+1: dbus_idle; 
               
               
                   
                 at  t+1: process_new_instruction_state; 
               
               
                   
                 right_hook: t+1; 
               
               
                   
                 end property; 
               
               
                   
                   
               
             
          
         
       
     
     For use in the proof below, the generated reset property is associated with points t 1 , t 2 , . . . t n  defined to be equal to t. 
     Auxiliary Property Schemata&#39;s 
     Restrictions about the macros from the correspondence information are captured in the following property schemata&#39;s. For all these property schemata&#39;s the macro triggers is derived from the macro TRIGGER 0  in the way presented for the property schemata simple_instruction. 
     cancel_correct: The property that is generated from this schemata ensures that the correspondence information for the cancel s  instruction is correctly formed: If one stage is cancelled, all of the preceding stages must also be cancelled. 
     
       
         
               
               
             
               
               
               
             
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 property cancel_correct; 
               
               
                   
                 dependencies: no_reset; 
               
               
                   
                 prove: 
               
             
          
           
               
                   
                 at  t: 
                 for each i in 2..n: 
               
               
                   
                   
                   if cancel i  = 1 
               
               
                   
                   
                   then cancel i−1  = 1 
               
               
                   
                   
                   end if; 
               
               
                   
                   
                 end for each; 
               
             
          
           
               
                   
                 end property; 
               
               
                   
                   
               
             
          
         
       
     
     stall_empty: This property schemata ensures that stages that do not execute an instruction are correctly flagged as empty by the correspondence information corresponding to the fulls macro. The macro triggers is the macro used in the properties above. 
     
       
         
               
             
               
               
             
               
             
           
               
                   
               
             
             
               
                 property stall_empty; 
               
               
                 dependencies: no_reset; 
               
               
                 prove: 
               
             
          
           
               
                 at  t: 
                 for each i in 2 .. n 
               
               
                   
                   if (not (full i−1  or (i−1 = int and trigger 0 )) or stall i−1 ) and 
               
               
                   
                     (not (full i  or (i = int and trigger 0 )) or not stall i ) 
               
               
                   
                   then 
               
               
                   
                     next(full i ) = 0; 
               
               
                   
                   end if; 
               
               
                   
                 end for each; 
               
             
          
           
               
                 end property; 
               
               
                   
               
             
          
         
       
     
     stall_full: This property schemata ensures that two instructions in adjacent ones of the stages will not merge. 
     
       
         
               
               
             
               
               
               
             
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 property stall_full; 
               
               
                   
                 dependencies: no_reset; 
               
               
                   
                 prove: 
               
             
          
           
               
                   
                 at  t: 
                 for each i in 2 .. n: 
               
               
                   
                   
                   if ( 
               
               
                   
                   
                     (full i  or (i = int and trigger 0 )) and 
               
               
                   
                   
                     (full i−1  or (i−1 = int and trigger 0 )) and 
               
               
                   
                   
                     not stall i−1 ) 
               
               
                   
                   
                   then stall i  = 0 
               
               
                   
                   
                   end if; 
               
               
                   
                   
                 end for each; 
               
             
          
           
               
                   
                 end property; 
               
               
                   
                   
               
             
          
         
       
     
     full_slot: This property schemata ensures that the full, correspondence information correctly flags the stages that execute an instruction. 
     
       
         
               
             
               
               
             
               
             
           
               
                   
               
             
             
               
                 property full_slot; 
               
               
                 dependencies: no_reset; 
               
               
                 prove: 
               
             
          
           
               
                 at  t: 
                 full 1  = 1 and 
               
               
                   
                 for each i in 1 .. n−1: 
               
               
                   
                   if ((full i = 1 or (i = int and trigger 0 )) and stall i  = 0 and 
               
               
                   
                   cancel i  = 0) 
               
               
                   
                   then next(full i+1 ) = 1 
               
               
                   
                   end if; 
               
               
                   
                 end for each and 
               
               
                   
                 for each i in 2 .. n: 
               
               
                   
                   if ((full i = 1 or (i = int and trigger 0 )) and stall i  = 1 and 
               
               
                   
                   cancel i  = 0) 
               
               
                   
                   then next(full i ) = 1 
               
               
                   
                   end if; 
               
               
                   
                 end for each; 
               
             
          
           
               
                 end property; 
               
               
                   
               
             
          
         
       
     
     empty_write: This property schemata ensures that an empty pipeline stage cannot write to a virtual register file. The empty_write property schemata must be replicated for every one of the architecture register files. 
     
       
         
               
             
               
               
             
               
             
           
               
                   
               
             
             
               
                 # for each register R file in the architectural state 
               
               
                 property empty_write R ; 
               
               
                 dependencies: no_reset; 
               
               
                 prove: 
               
             
          
           
               
                 at  t: 
                 if (full dec+1  = 0) then result_write R,dec+1  = 0 end if and 
               
               
                   
                 if (full dec+2  = 0) then result_write R,dec+2  = 0 end if and 
               
               
                   
                 ... 
               
               
                   
                 if (full writebackR  = 0) then result_write R,writebackR  = 0 end if; 
               
             
          
           
               
                 end property; 
               
               
                 # end for each register; 
               
               
                   
               
             
          
         
       
     
     write_back: This property schemata ensures that the implementation register file current R (k) for every architecture register file will not change if it is not updated. 
     
       
         
               
               
             
               
               
               
             
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 # for each register R file in the architectural state 
               
               
                   
                 property write_back R ; 
               
               
                   
                 dependencies: no_reset; 
               
               
                   
                 prove: 
               
             
          
           
               
                   
                 at  t: 
                 for each k in &lt;index range of Ri&gt; 
               
               
                   
                   
                   if (stall writebackR  = 1 or result_write R,writebackR  = 0 or 
               
               
                   
                   
                     result_dest R,writebackR  /= k) 
               
               
                   
                   
                   then next(current R (k)) = current R (k) 
               
               
                   
                   
                   end if; 
               
               
                   
                   
                 end for each; 
               
             
          
           
               
                   
                 end property; 
               
               
                   
                 # end for each register; 
               
               
                   
                   
               
             
          
         
       
     
     empty_cancel: The property schemata empty_cancel states that the empty stages cannot initiate a cancel instruction. Moreover, the stages int and beyond cannot initiate a cancel instruction at all. This is a consequence from the relations between the stages. 
     
       
         
               
             
               
               
             
               
             
           
               
                   
               
             
             
               
                 property empty_cancel; 
               
               
                 dependencies: no_reset; 
               
               
                 prove: 
               
             
          
           
               
                 at  t: 
                 if (not full 2 ) then primary_cancel 1  = 0 end if and 
               
               
                   
                 if (not full 3 ) then primary_cancel 2  = 0 end if and 
               
               
                   
                 ... 
               
               
                   
                 if (not full int−1 ) then primary_cancel int−2  = 0 end if and 
               
               
                   
                 if (not (full int  or trigger 0 )) then primary_cancel int−1  = 0 end if 
               
               
                   
                 and 
               
               
                   
                 cancel int  = 0 and 
               
               
                   
                 cancel int+1  = 0 and 
               
               
                   
                 ... and 
               
               
                   
                 cancel n  = 0; 
               
             
          
           
               
                 end property; 
               
               
                   
               
             
          
         
       
     
     interrupt_regs_valid: This property schemata requires that the values required to determine whether the interrupt is accepted are always valid. 
                                             # for each register R[k] evaluated in TRIGGER 0 .           property interrupt_regs_valid R,k ;           dependencies: no_reset;           prove:           at  t:  valid R,int (k);           end property;           # end for each                        
Liveness Properties
 
     The proofs above show the equivalence between the architecture and the implementation only if the stall signals will never generate a stall forever. The ensuing section is dedicated to the property schemata&#39;s from which the properties are generated that show that no stall will last forever, and that consequently, the execution of every interrupt or instruction takes only a finite number of clock cycles of the implementation. 
     There are algorithms available in the state of the art, which can prove such properties directly. However, these algorithms are limited with respect to complexity. 
     Let w 1 , w 2 , w 3 , . . . w n  be a set of weights with w k &gt;w k+1  and 0&lt;w 1 . The exact choice is not important. In the following, we chose the assignment w n-k =k+1. 
     The total weight total s  after the stage s in the pipeline is the sum of the weight of all full stages &gt;s:
 
total s =full s+1   *w   s+1 +full s+2   *w   s+2 + . . . full n   *w   n  
 
     With the help of this definition of the total weight total s , the following property schemata&#39;s are used to generate properties in order to show that the stalls in the stage s do not last forever. 
     
       
         
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 property liveness_stall s ; 
               
               
                   
                 assume: 
               
             
          
           
               
                   
                 at t: 
                 external_stall = 1; 
               
               
                   
                 prove: 
               
               
                   
                 at t+1: 
                 (total s  &lt;= prev(total s )) or stall s =0; 
               
             
          
           
               
                   
                 end property; 
               
               
                   
                 property liveness_nostall s ; 
               
               
                   
                 assume: 
               
             
          
           
               
                   
                 at t: 
                 external_stall = 0; 
               
               
                   
                 prove: 
               
               
                   
                 at t+1: 
                 (total s  &lt; prev(total s )) or stall s  = 0; 
               
             
          
           
               
                   
                 end property; 
               
               
                   
                   
               
             
          
         
       
     
     These properties schemata&#39;s show that each time there is no external stall, the total weight total s  either actually decreases or there is no stalls of pipeline stage s in the sense of the correspondence. In the case of an external stall, the total weight total s  can only increase if there is no stall s . In other words, if stalls were active forever and the external stalls are not active forever, the total weight total s  would have to become a negative number, which is a contradiction. Thus, the above two property schemata&#39;s prove generally that the stall signal to the stage s is not active indefinitely if the environment does not stall the processor indefinitely. Note that the property schemata&#39;s do not require explicit user input on the exact forwarding paths that are implemented. In other words, the user does not have to tediously model the exact condition when the instructions are stalled and when the instructions are not stalled. The above property schemata&#39;s form the minimum requirements that any pipelined processor has to fulfil. 
     In fact, these two property schemata&#39;s even prove liveness of a processor without any forwarding at all—the weight total s  will decrease until it reaches 0. In that case, there are no more instructions in front of the stage s and hence there is no more internal reason to stall the stage s. In the absence of a memory stall, the instruction in stage s will therefore proceed to stage s+1. 
     Proof 
     This section shows that the proof of all generated properties is sufficient to prove equivalence between the architecture description and the implementation. 
     The Concept of the Proof 
     The situation examined by the proof follows the definition of the equivalence of the architecture description and the implementation description. An instruction memory with the same contents of the instructions is connected to both the implementation and the architecture. The instruction memory is treated as if the instruction memory were an asynchronous memory for the architecture. This means that the instruction memory returns the requested information from the instruction memory to a requester in the same cycle. For the implementation description, the instruction memory may have some latency that the implementation accounts for with stalls or by issuing the address and reading the instructions in different ones of the stages in the pipeline. 
     Similarly, a data memory is given for the architecture and the implementation with the same initial values. Again, in the view of the architecture description, the data memory is asynchronous and returns read data in the cycle in which the read data was requested. The data is written such that the data is available in the next cycle. For the implementation, the data memory might have some latency that is accounted for with stalls or by handling the address data and the read data in different ones of the pipeline stages. 
     It is assumed that the properties are generated according to the invention and that all of the properties were proven to hold on the implementation with a formal verification tool, as e.g. a property checker. 
     The proof will examine how the generated properties match execution traces of the implementation. These execution traces include the memory traffic and the behaviour on the interrupt signals irpt. The execution traces start with a reset behaviour according to the macro trigger init , and provide no further activation of the reset later on. The proof will show that every execution trace can be matched (in the sense of the section on Terminology) with a chain P 0 , P 1 , P 2 , P 3 , . . . of properties generated from the following property schemata&#39;s: reset, simple_instruction, jump_instruction, and interrupt h . These generated properties will be called main properties below. 
     It will be further shown that the behaviour of the implementation can be uniquely predicted solely on the base of the properties. Once the properties are proven against the implementation description, the implementation description could be discarded and it is possible to predict the implementation behaviour by reasoning about the properties, taking into account their logical interaction. The logical interaction between the generated properties uniquely predicts the accesses to the data memory and the instruction memory, given only the implementation interrupts irpt, the contents of the instruction memory represented by the input iw, the contents of the data memory represented by the read data input dbus_rdata, the behaviour of the stalls conditions, and the reset behaviour according to the restrictions from the last paragraph. For this part of the proof, the chain P 0 , P 1 , P 2 , P 3 , . . . of the main properties serves as a basic structure that is filled in with the properties generated from the auxiliary property schemata&#39;s from the section above. These properties will be called auxiliary properties below. 
     If the generated properties are verified by simulation this close logical interaction interrelation between the properties has the effect that one of the bugs in the implementation that corrupts the execution of the instruction or the interrupt will be identified by the respective property, at least if this one of the bugs may impact the execution of any ensuing instruction or interrupt. 
     The chain of main properties P 0 , P 1 , P 2 , P 3 , . . . that matches an execution trace relates to a sequence of architecture description entries about the reset behaviour (P 0 ), and the execution of instructions and interrupts (P i  for i&gt;0). This allows the definition of an interrupt mapping of the implementation interrupt inputs irpt to the interrupt inputs IRPT of the architecture. To this end it should be noted, that the matching of the chain of main properties P 0 , P 1 , P 2 , P 3 , . . . involves an instantiation of the time variables of each of the properties P 0 , P 1 , P 2 , P 3 , . . . . For every property P j  generated from property schemata interrupt h  in the execution sequence, the interrupt input IRPT @ j becomes irpt @ t irpt , where t irpt  is the time variable from the property schemata that underlies P j . This time variable is instantiated to one time point by the way the chain of properties P 0 , P 1 , P 2 , P 3 , . . . is matched with the execution trace. 
     For every property P j  generated from the property schemata&#39;s simple_instruction or jump_instruction, IRPT @ j becomes irpt @ t init . This shows the existence of an interrupt mapping that is required by the definition of equivalence between implementation and architecture. 
     The proof will show that, if the architecture starts from the reset state defined in the architecture description and is provided with interrupt signals IRPT as defined above, the architecture will execute the same sequence of architecture description entries. The proof will also show that this execution deals with the same data according to an interpretation that is derived from the virtual register file and will be described in the course of the proof. 
     From this it is possible to deduce that the data memory accesses will be made with the same address data and the same write data, and in the same sequence. This in turn enforces that the same data is read in every one of the read transactions. This concludes the equivalence proof. 
     Data after a Property 
     It will now be shown how the implementation state is mapped to the architecture state by means of the virtual register file defined in the correspondence information. As a consequence of the mapping, each main property describes how the virtual register files become modified by the execution of the instruction or the interrupt that is described by that main property. 
     To this end, the stage function S is introduced: For a given finite sequence of time points t 1 , t 2 , . . . t w , with t 1 &lt;=t 2 , t 2 &lt;=t 3 , . . . t w-1 &lt;=t w , as the sequence of time points t 1 , t 2 , . . . t w , occurs in the main properties a function S(t) is defined such that the function S(t) returns 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 -)  the value 1, if t &lt;= t 1 , 
               
               
                   
                 -)  the value i, if t lies in the interval [t i−1 +1, t i ], 
               
               
                   
                 -)  w+1, if t &gt; t w.   
               
               
                   
                   
               
             
          
         
       
     
     In the context of the property schemata&#39;s simple_instruction and jump_instruction, the function S(t) returns the number of the stage at which the instruction is executed in dependency of the time, provided that t lies between t 1  and t n . This is why this function S(t) is called the stage function for the sequence t 1 , t 2 , . . . t w  of time points. 
     In the context of the property schemata interrupt h , S(t) returns the number of the stage, at which the interrupt is executed in dependency of the time, provided that t&gt;=t irpt . 
     It will be shown that for every property in a chain of main properties that covers an execution trace, for all architecture register files R, and for all time points v and w, right_hook&lt;v&lt;w&lt;=t writebackR +1, the following consistency expressions for virtual register files hold 
     
       
         
               
               
             
           
               
                   
               
             
             
               
                   
                 valid R,S(v)−1 (k) @ v -&gt; valid R,S(w)−1 (k) @ w 
               
               
                 and 
                 valid R,S(v)−1 (k) @ v -&gt; (data R,S(v)−1 (k) @ v = data R,S(w)−1 (k) @ w) 
               
               
                   
               
             
          
         
       
     
     Once this is shown, further conclusions are: Since the expression valid R,writebackR (k)=1 by definition, the expression valid R,s(u)-1 (k) at time point u becomes true at least for the time point u=t writebackR +1. If the expression valid R,witebackR (k) becomes true at an earlier time point, the data R,s(u)-1 (k) at time point u will be constant from this time point u onwards until the time point t writebackR +1. It is therefore correct to speak of the one dedicated value that the virtual register file has after the virtual register file becomes valid as being the value of the virtual register file after a main property. 
     Main Induction Hypothesis 
     The proof is performed by induction. The induction hypothesis is that for all j&gt;=0 the following conjectures hold: 
     1. For every execution trace following the reset restrictions from the section about the Proof Concept, there is a finite chain P 0 , P 1 , P 2 , . . . , P j  of main properties that matches an initial part of the execution trace. 
     2. The consistency expressions for virtual register files hold for the main property P j . 
     3. The value of every architecture register R[k] @ j+1 equals the value of the virtual register file after the main property P j . 
     4. After the j-th architecture cycle the value of the architecture program counter PC @ j+1 equals the value of the implementation program counter pc at the time point right_hook+1 that is provided by the way the main property P j  matches the execution trace of the implementation.
 
5. P j  and the j-th architecture cycle describe the same transaction from or to the data memory.
 
6. Moreover, there is no interrupt accepted in the interval [right_hook+1, t int ] of P j , i.e. trigger 0 =false for all time points in this interval.
 
     This induction hypothesis will be referred to as the main induction hypothesis in the following. 
     Base Case 
     The base case is about the reset of both the architecture and the implementation. The reset of the architecture provides register file values according to ACT init , the activity block of the reset in the architecture description. This gives the register file values R[k] @1 and in addition the program counter value PC @1. The register values and the value of the program PC form the first architectural state AS 1.\   
     The application of the reset property onto the implementation sets all time points t 1 , t 2 , . . . t n  to t, the time point where the reset is activated. Consequently, the reset state of the implementation is reached at the time point t+1.\ 
     Conjecture 1 of the main induction hypothesis is trivial in this context, because every execution trace is required to start with reset behaviour according to the function trigger init . Therefore, the property P 0  generated from property schemata reset fits. Furthermore, the property P 0  describes no data memory access. 
     Conjecture 2 of the main induction hypothesis is trivial in this context, because in this case the interval [right_hook, t writebackR +1] contains only one element. 
     Conjecture 3 is a direct consequence of the fact that all of the architecture registers are reset in the architecture to the same values as current R  @ t+1 in the implementation. 
     Conjecture 4 holds because of the resetting of the program counter in both architecture and implementation. 
     Conjecture 5 holds, because the reset issues no data bus request. 
     Conjecture 6 holds, because the interval [right_hook+1, t int ] is empty. 
     The base case is verified by property schemata reset. It ensures that pc and all virtual register files contain the same values as the architecture after reset. 
     Induction Step 
     The induction step assumes that the induction hypothesis holds for j architecture cycles. It now has to be shown that the induction step also holds for the j+1 st  architecture cycle and the main property P j+1 . To this end it must be shown that there is a main property P j+1  for every execution trace such that the chain P 0 , P 1 , P 2 , . . . P j+1  of main properties matches an initial part of the execution trace. It must then be shown that the architecture executes the related architecture description entry and produces the same data. 
     The time points of main property P j  will be denoted T 0 , T 1 , T 2 , . . . T n  in the following. q will be chosen such that it is the highest index less or equal n with T q =right_hook of the main property P j . 
     Candidates for P j+1    
     Because of the liveness of the stall signals, there is a first time point t′ 1 &gt;T q  with stall 1  @ t′ 1 =0, and a second time point t′ 2 &gt;t′ 1  with stall 2  @ t′ 2 =0 and so forth for the time points t′ 3 , . . . t′ n . If the macro trigger 0  is satisfied somewhere in the interval [T int +1, t′ int −1], then there is at least one interrupt accepted in this interval [T int +1, t′ int −1]. Let t irpt  be the first time point in that interval where an interrupt is accepted, i.e. the first time point such that trigger 0  @ t irpt =1. In this situation, the only candidate that could become P j+1  is one of the main properties generated from property schemata interrupt h , where h=S(t irpt ), with S being the stage function for t′ 1 , t′ 2 , . . . t′ n . However, the applicability of such a property still needs confirmation. To ease this confirmation, the time points t 0 , t 1 , . . . t n  is defined in the way used in this property schemata, i.e. t 0 =T q , t 1 =t′ 1 , t′ 2 =t′ 2 , . . . t h−1 =t′ h−1 , t h =t irpt , t h+1 =t irpt , . . . t int−1 =t irpt , t int  is the first time point &gt;=t irpt  with stall int  @ t int =0, t int+1  the first time point &gt;t int  with stall int+1  @ t int+1 =0 and so forth for t int+2 , t int+3 , . . . t n . 
     If the macro trigger 0  is 0 on the whole interval [T int +1, t′ int −1], the interrupt mapping is defined such that IRPT @ j+1 becomes irpt @ t′ int . In this situation irpt @ t′ int  may or may or may not yield an accepted interrupt, depending on whether trigger 0  @ t′ int  is 1 or 0. If there is an interrupt accepted, the property generated from property schemata interrupt int  with t irpt =t int  is the candidate for P j+1 . If there is no interrupt, a property generated from property schemata simple_instruction or jump_instruction is the candidate for P j+1 . However, the applicability of such a property still needs confirmation. To ease this confirmation the time points t 0 , t 1 , . . . t n  is defined to be t 0 =T q , t 1 =t′ 1 , t 2 =t′ 2 , . . . t n =t′ n . 
     Once the proof is finished the section above provides a mapping from the interrupt inputs of the implementation to the interrupt inputs of the architecture as required by the definition of equivalence. 
     Empty Region 
     The timing relations between P j  and the candidate for P j+1  are exemplified in some figures:
           FIG. 5  shows two of the main properties P j  and P j+1  generated from the property schemata simple_instruction.     FIG. 6  shows the general case of the property generated from property schemata&#39;s reset (q=n), jump_instruction (q=jmp m ), interrupt (q=int, if t irpt =t int , q=int−1, if t irpt &lt;t int ), or simple_instruction, followed by a property generated from the property schemata&#39;s simple_instruction or jump_instruction. It degenerates to  FIG. 5  for the case q=1.     FIG. 7  shows the general case of one of the properties generated from the property schemata&#39;s reset, simple_instruction, jump_instruction, or interrupt h  followed by a property generated from the property schemata interrupts, where q is assigned as indicated above.       

     The figures show instruction specific computations and a region of pairs (time, stage) between the instruction specific computations. For a given stage s, this region of pairs starts at T q +1=t 0 +1 for the stages s in [2, q], and at T s +1 for the stages s&gt;q. For a given one of the stages s, the region extends to the right until it terminates at the time points t s−1  inclusively that were introduced above. 
     It will be shown about this region that the stages s are empty at the time points t in that region, i.e. that full s  @ t=0 for all t in the interval [max(T q , T s )+1, t s−1 ]. This has two consequences: Firstly, it can be shown that the assume parts about the absence of cancels are satisfied; secondly it will be shown that the virtual register values after P j  become the virtual register values that are being required by P j+1 . 
     The proof about the empty region will be executed by an induction in two dimensions: The induction in the direction of increasing stages will be executed by a base and a step case which are proven themselves by inductions over time. 
     In the following, it is not differentiated between the property generated from an auxiliary one of the property schemata and the auxiliary property schemata itself. The property &lt;name&gt; will therefore be written as an abbreviation for “a property generated from an auxiliary property schemata &lt;name&gt;”. This is unambiguous, because there is always only one property generated from an auxiliary property schemata. 
     The base case for the induction over the stages s is s=2. 
     The base case for the induction over the time is t=max(T q , T 2 )+1 
     If 2&lt;=q, P j  is generated from one of the property schemata&#39;s jump_instruction, interrupt h , or reset. It cannot be generated from the property schemata simple_instruction, because this would be related to q=1. Consequently T 2 &lt;=T q , and full 2  @ T q +1=0 from the proof part of the main property P j . 
     If q=1, there is only something to prove if the interval is not empty, which requires T 2 &lt;t 1 . It is stall 2  @ T 2 =0. Additionally, it is stall 1  @ T 2 =1, because t 1  was defined to be the next time point after T 1  without a stall 1 . From the property stall_empty then follows full 2  @ T 2 +1=0. 
     Step case for the induction over the time: Let w be a time point in [T 2 +1, t 1 −1]. The induction hypothesis allows the assumption full 2  @ w=0. Then stall 1  @ w=1 (because t 1  is the first nostall of stage 1 after T 1 ) and from property stall_empty follows full 2  @ w+1=0. 
     This proves the base case for the induction over the stages. 
     Induction step from s to s+1: Let s be some stage in the interval [2, n−1]. From the induction hypothesis it follows that full s =0 for all time points in [max(T q , T s )+1, t s−1 ]. 
     The induction step over the stages is again proven by induction over time. 
     The base case t=max(T q , T s+1 )+1 requires case induction over the relation of q and s+1: 
     Firstly, s+1&lt;=q is examined. This means that property P j  is generated from property schemata reset, jump_instruction or interrupts. It proves directly full s+1  @ T q +1=0. 
     If q&lt;s+1, the interval [max(T q , T s+1 )+1, t s ] only contains elements, if T s+1 &lt;t s . Out of the definition of q it is T s &lt;T s+1 , hence stall s+1  @ T s+1 =0. A case split about the relation of t s−1  and T s+1  needs to be executed. 
     If t s−1 &lt;T s+1 , then it is T s+1  in the interval [t s−1 +1, t s −1] and therefore stall s  @ T s+1 =1. Then property stall_empty allows to conclude full s+1 +1=0. 
     If T s+1 &lt;=t s−1 , then the time point T s+1  lies in the interval [t s +1, t s−1 ]. Thus the hypothesis for the induction over the stages is applicable and shows full s  @ T s+1 =0. If there is no interrupt accepted at T s+1 , or if s/=int, then the property stall_empty is applicable and shows full s+1  @ T s+1 +1=0. 
     If s=int and an interrupt is accepted at T s+1 , then T s+1 =t irpt . t int  is defined to be the first time point with a nostall that is greater or equal t irpt . As t int  is expected to be &gt;T int+1 , it follows stall s  @ T int+1 =1. Thus, property stall_empty again shows full int+1  @ T int+1 +1=0. 
     Step: Let full s+1  @ w=0 be proven for some time point w in the interval [max(T q , T s+1 )+1, t s −1]. 
     To determine full s+1  @ w+1, an interrupt accepted at time w=t irpt  can only become relevant, if t irpt &lt;t s . Thus, s=int. Moreover, stall int  @ t irpt =1. This allows the application of property stall_empty, which gives full s+1  @ t irpt +1=0. 
     For the remaining cases, an interrupt accepted at time w can therefore be excluded, or is irrelevant for the application of property stall_empty. 
     If w&lt;=t s−1 , the induction hypothesis about the stage s is applicable, giving full s  @ w=0. Therefore, property stall_empty is applicable, and this shows full s+1  @ w+1=0. 
     If t s−1 &lt;w, there is w in [t s−1 +1, t s −1]. In this interval, there is stall s  @ w=1, thus the application of property stall_empty delivers full s+1  @ w+1=0. 
     This proves the induction step. 
     This proves the whole claim. 
     Cancels 
     Let t be a time point between (and including) t 0 +1=T q +1 and t n . Let U(t) be the stage function related to the T 1 , T 2 , . . . T n . Let L(t) be the stage function related to the t 1 , t 2 , . . . t n . 
     Obviously, it is at least L(t)&lt;=U(t). It will be shown later, that this can be strengthened to L(t)&lt;U(t). 
     It will be proven that cancel L(t)  @ t=0. This is done by proving that cancel s  @ t=0 for all s in the interval [L(t), max(U(t), n)]. 
     This can be seen by induction over s.
         Base: If t&lt;=T n , then the assume part of main property P j  delivers cancel U(t)  @ t=0 and the prove part primary_cancel U(t)-1  @ t=0. As P j  was shown to be applicable, the assume part describes the situation. This shows cancel U(t)-1  @ t=0. If t&gt;T n , then U(t)=n+1 and it follows from the property empty_cancel that cancel n  @ t=0. This proves the base case.   Step: Let there be cancel s  @ t=0 for some stage s in the interval [L(t)+1, U(t)−1]. If int&lt;s, the induction hypothesis follows directly from the property empty_cancel: It is cancel s−1  @ t=0. If s&lt;=int, it is cancel s−1  @ t=cancel s  @ t or primary_cancel s−1  @ t, because this is how primary_cancel is defined. From the induction hypothesis, it is cancel s  @ t=0, from the property empty_cancel, it is primary_cancel s−1  @ t=0 and thus cancel s−1 =0. This proves the step case and thus the whole claim.       

     A consequence of this proof is that it shows that the condition 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 during [t 0 +1, t 1 ]: cancel 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 ]: cancel 2  = 0; 
               
               
                   
                 during [t 2 +1, t 3 ]: cancel 3  = 0; 
               
               
                   
                 ... 
               
               
                   
                 during [t n−1 +1, t n ]: cancel n  = 0; 
               
               
                   
                   
               
             
          
         
       
     
     of the candidate property P j+1  is satisfied. 
     Disjoint Slots 
     A slot from time point t and stage s is defined to be a sequence of time points (t, t s+1 , t s+2 , . . . t n , t n +1) with 
     
       
         
               
               
               
               
             
               
               
               
             
               
               
               
               
             
               
               
               
             
               
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 at 
                 t: 
                   stall s  = 0; 
               
             
          
           
               
                   
                 during [t s +1, t s+1 −1]: 
                   stall s+1  = 1; 
               
             
          
           
               
                   
                 at 
                 t s+1 : 
                   stall s+1  = 0; 
               
               
                   
                 ... 
               
             
          
           
               
                   
                 during [t n−1 +1, t n ]: 
                   stall n  = 1; 
               
             
          
           
               
                   
                 at 
                 t n : 
                   stall n  = 0; 
               
               
                   
                   
               
             
          
         
       
     
     Instructions and interrupts are executed in slots. The instruction slots start at time t 1  in stage 1 and are proven to be marked by full s  @ t for all t&gt;=T q  if the property P j  was generated from the property schemata&#39;s simple_instruction or jump_instruction, the interrupt slots start at time t int  in stage int and are proven to be marked by full s  @ t if the property P j  was generated from property schemata interrupt h . For the instruction slots defined by the t 1 , t 2 , . . . t n  in case of instruction execution and for the interrupt slots defined by t int , t int+1 , . . . t n  in case of interrupts, the property full_slot also shows that the full s =1 @ t shows that stage s executes an instruction or an interrupt at time t. 
     This shows that the instruction slots or the interrupt slots of two instruction or interrupt executions will never merge: Let there be two slots that start at the same stage s at different time points t and t′, where full s  @ t=1 and full s  @ t′=1; then the slots are disjoint in the sense, that for all stages i the intervals [t i +1, t i+1 ] and [t′ i +1, t′ i+1 ] are disjoint. 
     This can be seen as follows: Assume that t&lt;t′ and that there is some time point and some stage where the slots overlap, then there is some first stage s′ for which the interval [t s′-1 +1, t s′ ] and [t′ s′-1 +1, t′ s′ ] intersect. As stall s′ =1 for all but the last time point in both intervals, it can be concluded that t s′ =t′ s′ . Therefore, [t′ s′-1 +1, t′ s′ ] is a subset of [t s′-1 +1, t s′ ]. As a result of property full_slot it is full s′ =1 for all time points in [t s′-1 +1, t s′ ]. It is t s′-1 &lt;t′ s′-1 , because otherwise the intervals would also intersect in stage s′−1, and it was assumed that s′ is the smallest such stage. Therefore, full s′  @ t′ s′-1 =1 and full s′-1  @ t′ s′-1 =1. From the definition of the slot, it is also stall s′-1  @ t′ s′-1 =1 and this forms a contradiction to property stall_full. 
     This shows that the execution of two instructions will never merge. Consequently, L(t)&lt;U(t). 
     Register Values 
     For every architecture register R[k] it is proven that for two time points v&lt;=w, both in interval [t dec-1 +1, t writebackR ] that 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 valid R,L(v)  @ v -&gt; valid R, L(w)  @ w and 
               
               
                   
                 valid R,L(v)  @ v -&gt; data R,L(v) (k) @ v = R[k] @ j + 1 
               
               
                   
                   
               
             
          
         
       
     
     The last equality is a consequence from the main induction hypothesis. Additionally for all registers R[k] on which TRIGGER 0  depends and for all v in the interval [T int +1, t int ] it will be proven
 
valid R,int ( k ) @  v  and (data R,int ( k ) @  v=R[k] @ j+ 1)
 
     To this end, one of the registers R[k] and one time point t from the interval [t 0 +1, t n ] is examined. As valid R,s  and data R,s  are only defined for pipeline stages s in the interval [dec, writeback R ], functions must be derived from the stage functions U and L that account for this limitation. Let l(t) be max(dec, L(t)) and u(t) be min(U(t), writeback R +1). Then it is proven by induction that for all stages s in [l(t), u(t)−1] it is
 
valid R,s ( k ) @  t =valid R,u(t)-1 ( k ) @  t  
 
     Proof: There is nothing to be shown in the base case s=u(t)−1. 
     Step from s to s−1: Let above claim hold for some s in [l(t)+1, u(t)−1]. Then it is from the definition 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 valid R,s−1 (k) @ t = (if (result_write R,s  and result_dest R,s  = k) 
               
               
                   
                   then result_valid R,s   
               
               
                   
                  else valid R,s (k)) @ t 
               
               
                   
                   
               
             
          
         
       
     
     Property empty_write is applicable, taking into account that full s  @ t=0, therefore result_write R,s =0, and hence valid R,s−1 (k) @ t=valid R,s (k) @ t. This proves the step and the claim. 
     Moreover, it will be proven that
 
valid R,s ( k ) @  t −&gt;data R,s ( k ) @  t=R[k] @ j+ 1
 
     Base case: To this end the claim will first be proven for s=u(t)−1. There is nothing to prove as long as t&lt;=T n +1, because this is an immediate consequence from the induction hypothesis. If t is from the interval [T n +1, t n-1 ] it is full writebackR  @ t=0, hence the property empty_write R  delivers the result result_write R,writebackR  @ t=0 and the property write_back R  allows the conclusion that data R,writebackR (k) @ t+1=data R,writebackR (k) @ t=R[k] @ j+1. If t is from the interval [t n-1 +1, t n −1] the same equation follows from stall n =1 and the property write_back R . Thus above claim holds for s=u(t). 
     Step from s to s−1: The reasoning for the step from s to s−1 follows the reasoning about valid R,s (k). It is by definition 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 data R,s−1 (k) @ t = 
               
               
                   
                 (if result_write R,s  and result_dest R,s  = k 
               
               
                   
                 then result_data R,s   
               
               
                   
                 else data R,s (k)) @ t 
               
               
                   
                   
               
             
          
         
       
     
     Since result_write R,s  @ t=0 (from property empty_write) it is data R,s−1 (k) @ t=data R,s (k) @ t=R[k] @ j+1. 
     The claim about valid R,int (k) and data R,int (k) is a consequence from the last proof, because property interrupt_regs_valid R,k  guarantees the validity. The first claim from this section is a consequence from the reasoning about valid R,s (k), data R,s (k), the fact that valid R,writebackR =1 by definition and the induction hypothesis. 
     Application of a Property Generated from Property Schemata interrupt h    
     The following will show that the property P j+1  generated from one of the three property schemata&#39;s simple_instruction, jump_instruction, or interrupt h  is always applicable. It will now be shown that if the candidate for the property P j+1  is generated from property schemata interrupt h , the property is indeed applicable: 
     If time variables from the property are instantiated with the time points t 0 , t 1 , . . . t n  and t irpt  as defined above, the conditions about the stalls and triggers (line 25 to 46 in property schemata interrupt h  are all satisfied. Moreover, the section about cancels shows that the assume part about the cancels (line 48 to 56) is satisfied, and the section about the empty region proves the assumptions about the values full h+1 , full h+2 , . . . full int  (line 62 to 65). 
     The assumption about process_new_instruction @ t 0  on line 59 is discharged by the proof of process_new_instruction @ T q  in main property P j . 
     This shows that one of the property schemata&#39;s interrupt h  is applicable. 
     The interrupt mapping and the reasoning about the architecture registers and the virtual registers show that TRIGGER 0  @ j+1 will evaluate the same values in the same way as trigger 0  @ t irpt . Thus, the architecture will execute an interrupt in its j+1 st  cycle. 
     It must now be shown that the main induction hypothesis is valid for j+1. 
     Conjecture 1 requires a look at all possible main properties. Therefore, for the current state of the proof it can only be noted, that a P j+1  exists whenever there should be an interrupt. 
     Conjecture 2 requires a proof of the consistency expressions for the virtual register after P j+1 . 
     Let R[k] be an architecture register. Let v&lt;=w be two time points from the interval [t int +1, t writebackR +1], and S be the stage function related to the time point t 1 , t 2 , t 3 , . . . t n   
     
       
         
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                   
                 valid R,S(v)−1 (k) @ v = 
               
               
                   
                   
                 (if (result_write R,S(v)  and result_dest R , S(v)  = k) 
               
               
                   
                   
                 then result_valid R , S(v)   
               
               
                   
                   
                 else valid R,S(v) (k)) @ v 
               
               
                   
                 and 
               
               
                   
                   
                 valid R,S(w)−1 (k) @ w = 
               
               
                   
                   
                 (if (result_write R,S(w)  and result_dest R , S(w)  = k) 
               
               
                   
                   
                 then result_valid R , S(w)   
               
               
                   
                   
                 else valid R,S(w) (k)) @ w 
               
               
                   
                   
               
             
          
         
       
     
     Main property P j  determines that result_write R,s(v)  @ v=result_write R,S(w)  @ w. If both are 1, then result_dest R,S(v)  @ v=result_dest R,S(w)  @ w, because both are equal to index 0,R , which is derived from INDEX 0,R  by replacing the architecture objects by expressions that evaluate a signal at one dedicated point of time. 
     Therefore, either valid R,s(v)-1 (k) @ v=result_valid R,S(v)  @ v and valid R,s(w)-1 (k) @ w=result_valid R,S(w)  @ v, or valid R,s(v)-1 (k) @ v=valid R,s(v) (k) @ v and valid R,s(w)-1 (k) @ w=valid R,s(w) (k) @ w. In both cases, the implication
 
valid R,L(v)-1 ( k ) @  v −&gt;valid R,L(w)-1 ( k ) @  w  
 
holds. The first is a consequence from the proof part of P j+1 , the second is a consequence from the reasoning about registers.
 
     Similar considerations show the equality of the values data R,S(v)-1 (k) @ v and data R,S(w)-1  @ w. If valid R,L(v)-1 (k) @ v=1, then result_write R,S(v)  @ v=result_write R,S(w)  @ w and result_dest R,S(v)  @ v=result_dest R,S(w)  @ w, which is a direct consequence of the proof part of main property P j+1 . Therefore, either valid R,L(v)-1 (k) @ v=result_valid R,L(v)  @ v=1, hence result_valid R,L(w)  @ w=1 and therefore data R,S(v)-1  @ v=update 0,R  @ v and data R,S(w)-1  @ w=update 0,R  @ w. In this case both expressions are equal, because update 0,R  is derived from UPDATE 0,R  by replacing all architecture objects by expressions that reference the implementation signals at one dedicated point of time. 
     In the case of data R,S(v)  @ v=data R,S(v)-1  @ v and data R,S(w)  @ w=data R,s(w)-1  @ w the equality follows from the considerations about the register file values. This proves conjecture 2 of the main induction hypothesis. 
     Therefore, it is possible to speak about a value of R[k] after the main property. P j+1 . This value is computed as follows. Let t be a time point from the interval [t irpt +1, t writebackR +1], such that valid R,L(t)-1 (k) @ t=1. Then 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 data R,L(t)−1 (k) @ t = 
               
               
                   
                  (if result_write R,L(t)  and result_dest R,L(t)  = k 
               
               
                   
                  then result_data R,L(t)   
               
               
                   
                  else data R,L(t) (k)) @ t 
               
               
                   
                   
               
             
          
         
       
     
     If result_write R,L(t)  and result_dest R,L(t) =k @ t is satisfied, it is valid R,L(t)-1 (k) @ t=result_valid R,L(t)  @ t and data R,L(t)-1 (k) @ t=result_data R,L(t) , the proof part of P j+1  then assures result_data R,L(t)  @ t=update 0,R  @ t irpt  where update 0,R  evaluates signals at dedicated time points defined by the way update 0,R  is derived from UPDATE 0,R  such that it is independent of the point of time where update 0,R  itself is evaluated. Also k=index 0,R  @ t irpt , which is again independent of the time point of evaluation. A proof part entry assures that all virtual register values being read in update 0,R  are valid, thus the main induction hypothesis shows that they are equal to the related values of R[k] @ j+1. Therefore update 0,R  @ t=UPDATE 0,R  and index 0,R  @ t=INDEX 0,R  @ j+1, such that R[k] @ j+2=data R,L(t)-1 (k) @ t. 
     If result_write R,L(t)  and result_dest R,L(t) =k is not satisfied, similar considerations show that R[k] @ j+1=R[k] @ j+2 and therefore again R[k] @ j+2=data R,L(t)-1 (k) @ t. This proves conjecture 3 of the main induction hypothesis. 
     Similarly, the equality of the PCs after instruction P j+1  and the j+1 st  architecture cycle are shown to prove conjecture 4. 
     Likewise, it can be shown that implementation and architecture perform equal memory transactions, thus proving conjecture 5. 
     The requirement that there is no interrupt accepted between [right_hook+1, t int ] of P j+1  follows from the respective proof part, and this proves conjecture 6. 
     Application of Properties Generated from Property Schemata simple_instruction or jump_instruction 
     Now the case in which no interrupt is accepted in the interval [T int +1, t int ] is considered. In this case there are also time points t 0 , t 1 , t 2 , . . . defined above, and if the time variables of a property generated from the property schemata simple_instruction or jump_instruction schemata are instantiated accordingly, the assumption about the stall behaviour (lines 13 to 21 in the property schemata&#39;s simple_instruction and jump_instruction) is again satisfied. 
     The reasoning about the cancel behaviour shows that the related assumptions (lines 24 to 28) are satisfied. 
     The assumption about process_new_instruction @ to (line 31) is discharged by the proof of process_new_instruction @ T q  in main property P j . 
     This shows that the assume part of the partial property simple_instruction.fetch or jump_instruction.fetch is satisfied. Therefore it is proven that a read access to the instruction memory is executed with the address pc @ t 1 , which equals PC @ j+1 due to the induction hypothesis. Therefore, the instruction memory returns the same instruction word iw @ t iv  for the implementation and IW @ j+1 for the architecture. 
     It is mentioned above that as a prerequisite for this examination the instruction memory only returns valid instructions. Therefore, there is at least one, and possibly even multiple architecture description entries with TRIGGER_IW m =1. For all these architecture description entries, the assumptions trigger_iw m  of the partial properties simple_instruction.validate_regs or jump_instruction.validate_regs are now satisfied. This shows that all trigger_state m  are evaluated on the base of valid virtual register values. Similar to the reasoning for interrupts above it can be seen that trigger_state m  @ t dec =TRIGGER_STATE m  @ j+1. It belongs to the requirements of this examination, that the possibly multiple TRIGGER_STATE m  for the same TRIGGER_IW m  form a full case split. Thus, there is one specification entry m where TRIGGER_STATE m  and TRIGGER_IW m  are both satisfied. The generated property for this entry will become P j+1 . Its applicability has already been shown. 
     This shows that for all execution traces that have initial parts that are already matched by a chain, P 0 , P 1 , P 2 , . . . P j  of main properties always a main property P j+1  can be found that makes the chain P 0 , P 1 , P 2 , . . . P j+1  of main properties match a longer initial part of the execution trace. 
     This proves conjecture 1 of the main induction hypothesis. 
     The conjecture 2, 3, 4, and 5 of the main induction hypothesis are shown as above for the property generated from property schemata interrupt h . 
     Then, given any execution trace that is matched by the chain P 0 , P 1 , P 2 , . . . P j , of main properties there is an instantiation of the time variables of P j  and according to this instantiation, conjecture 6 of the induction hypothesis allows to assume trigger 0 =0 for all time points in the interval [T q +1, T int ] (the T relate to the time points of P j ). For the time variable to of P j+1 , there is t 0 &lt;=T int . Therefore, trigger 0 =0 for all time points in [t 0 +1, T int ]. An interrupt accepted in the interval [T int +1, t int ] is handled by the section about the application of a property generated from property schemata interrupt h , if P j+1  is generated from the property schemata&#39;s simple_instruction or jump_instruction, there is no interrupt accepted in [T int +1, t int ]. This proves conjecture 6 of the main induction hypothesis. 
     This concludes the proof. One important consequence of the proof is that if the correspondence information is provided such that all generated properties can be proven to hold on the implementation, the exact shape of the correspondence information is irrelevant. Therefore, the correspondence information cannot make the verification process falsely output equivalence for a non equivalent pair of the architecture description and the implementation description. 
     Application Example 
     The user inputs were demonstrated using a small example processor with the following features:
         It has one register file REG with 8 registers.   It has a program counter PC   It is implemented by a 4 stage pipeline.   It supports forwarding.   It supports stalls initiated by the data memory.   It supports some exemplary instructions. These instructions will be listed next, and the operands of the instructions are described. The full instruction consists of an opcode to select what has to be done and the operands need to be interpreted according to the opcode. All this is to be decoded from the instruction word. The list of instructions is:   NOT: A register is selected by the command, its contents bitwise negated and the result is stored at a destination register the address of which is also given in the instruction.   ADD/SUB: Two source operand registers are selected by the command and the result is written into a destination address the address of which is given by the instruction.   LD: A register is selected by the instruction to provide some base address. An offset provided by the instruction will be added to the base address. This gives an address from which data is loaded from the data memory.   ST: A register is selected by the instruction to provide a base address. An offset provided by the instruction will be added to the base address. This gives the address of a write request for the data memory. The instruction also provides the address of the register the data of which is to be stored.   BEQZ: A register is selected by the instruction. If this register is 0, a jump will be executed. Execution of the jump means that an offset provided by the instruction is added to the address where the instruction is found in the instruction memory; this gives the address of the next instruction. If the register is not 0, the jump will not be executed and the program counter will be incremented by the size of the instruction.   In case of the instruction BEQZ, the processor speculates that the instruction is not taken. The condition that the source register file is 0 is checked in the 2 nd  stage, which can lead to cancel instructions in stage 1.   Interrupts arrive at the processor via the signal int_valid_i. The interrupts are accepted if the register REG[0] is 0. The address to which the processor should return after an interrupt service routine will be stored in the register REG[0]. In case of the interrupt the start address of the interrupt service routine is provided via the input int_addr_i, which belongs to the interrupt inputs.
 
Architecture
       

     Architecture Inputs 
     Besides the standardized memory inputs (see the description above) the architecture has the input INT_VALID_I on which the interrupt may arrive, an input INT_ADDR_I to define the first address of the interrupt service routine and an input RESET_N to reset the processor. 
     Architecture States 
     The architecture states are the register file REG and the program counter PC. 
     Architecture description Entries 
     Initialization 
     The processor is initialized by activation of the reset. This initialisation is captured by the following expression:
 
TRIGGER init :=RESET —   N= 0;
 
     After the initialization is completed, the processor is in a state in which all architecture states yield 0. The corresponding activity block ACT init  is therefore: 
     
       
         
               
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 PC := 
                 0; 
                   
               
               
                   
                 REG[0] := 
                 0; 
               
               
                   
                 REG[1] := 
                 0; 
               
               
                   
                 REG[2] := 
                 0; 
               
               
                   
                 REG[3] := 
                 0; 
               
               
                   
                 REG[4] := 
                 0; 
               
               
                   
                 REG[5] := 
                 0; 
               
               
                   
                 REG[6] := 
                 0; 
               
               
                   
                 REG[7] := 
                 0; 
               
               
                   
                   
               
             
          
         
       
     
     Interrupt 
     The condition under which an interrupt is accepted is given by
 
TRIGGER 0 :=INT_VALID —   I  and REG[0]=0;
 
     The following activity block ACT 0  describes the execution of the interrupt according to what was said above. 
     
       
         
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 UPDATE 0,PC  := 
                 INT_ADDR_I; 
               
               
                   
                 UPDATE 0,REG  := 
                 PC; 
               
               
                   
                 INDEX 0,REG  :=0; 
               
               
                   
                 DMEM_IDLE 0   
               
               
                   
                   
               
             
          
         
       
     
     The last entry of the activity block refers to the fact that no access to the data memory is executed. 
     Arithmetic/Logical Instructions 
     It is assumed that constants add, sub, not, etc. are defined that contain the opcode for the related instruction. 
     The way arithmetic/logical instructions are executed does not depend on the processor state but solely on the instruction word. This is reflected by the triggers. For instruction ADD the trigger is: 
     
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER_IW 1  := IW[15:11] = add; 
               
               
                   
                 TRIGGER_STATE 1  :=  true; 
               
               
                   
                   
               
             
          
         
       
     
     The activity block specifies the PC increment and the update of register file REG according to the instruction. 
     
       
         
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 UPDATE 1,PC  := 
                   (PC + 2)[7 :0]; 
               
               
                   
                 UPDATE 1,REG  := 
                   (REG[IW[10:8]] + REG[IW[7:5]])[15:0] 
               
               
                   
                 INDEX 1,REG  := 
                 IW[4:2]; 
               
               
                   
                 VINDEX 1,1  := 
                   IW[7:5]; 
               
               
                   
                 VINDEX 1,2  := 
                   IW[10:8]; 
               
               
                   
                 DMEM_IDLE 1   
               
               
                   
                   
               
             
          
         
       
     
     Similar for instruction SUB: 
     
       
         
               
               
             
               
               
             
               
               
             
               
             
               
               
             
           
               
                   
               
             
             
               
                 TRIGGER_IW 2  := 
                 IW[15:11] = sub; 
               
             
          
           
               
                 TRIGGER_STATE 2  := 
                  true; 
               
             
          
           
               
                 UPDATE 2,PC  := 
                 (PC + 2)[7 :0]; 
               
               
                 UPDATE 2,REG  := 
                 unsigned((REG[IW[10:8]] − REG[IW[7:5]])[15:0]) 
               
             
          
           
               
                 INDEX 2,REG  :=IW[4:2]; 
               
             
          
           
               
                 VINDEX 2,1  := 
                 IW[7:5]; 
               
               
                 VINDEX 2,2  := 
                 IW[10:8]; 
               
               
                 DMEM_IDLE 2   
               
               
                   
               
             
          
         
       
     
     Instruction NOT 
     
       
         
               
               
               
             
               
               
               
             
               
               
               
             
               
               
             
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER_IW 3  := 
                 IW[15:11] = not; 
               
             
          
           
               
                   
                 TRIGGER_STATE 3  := 
                  true; 
               
             
          
           
               
                   
                 UPDATE 3,PC  := 
                 (PC + 2)[7 :0]; 
               
               
                   
                 UPDATE 3,REG  := 
                 ~ REG[IW[10:8]] 
               
             
          
           
               
                   
                 INDEX 3,REG  :=IW[4:2]; 
               
             
          
           
               
                   
                 VINDEX 3,1  := 
                 IW[10:8]; 
               
               
                   
                 DMEM_IDLE 3   
               
               
                   
                   
               
             
          
         
       
     
     Memory Instructions 
     The interesting part of the memory instructions is that the activity block contains the entry DMEM_READ or DMEM_WRITE, and that the activity blocks of read instructions use the macro DMEM_RDATA for the read data. 
     Instruction LD 
     
       
         
               
               
               
             
               
               
               
             
               
               
               
             
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER_IW 4  := 
                 IW[15:11] = ld; 
               
             
          
           
               
                   
                 TRIGGER_STATE 4  := 
                 true; 
               
               
                   
                 UPDATE 4,PC  := 
                 (PC + 2)[7 :0]; 
               
             
          
           
               
                   
                 UPDATE 4,REG  := 
                 DMEM_RDATA; 
               
               
                   
                 INDEX 4,REG  := 
                 IW[10:8]; 
               
               
                   
                 VINDEX 4,1  := 
                 IW[7:5]; 
               
             
          
           
               
                   
                 DMEM_READ 4 ((IW[4:0] + REG[IW[7:5]]) [7:0]) 
               
               
                   
                   
               
             
          
         
       
     
     Instruction ST 
     
       
         
               
               
               
             
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER_IW 5  := 
                 IW[15:11] = st; 
               
             
          
           
               
                   
                 TRIGGGER_STATE 5  := 
                 true; 
               
               
                   
                 UPDATE 5,PC  := 
                 (PC + 2)[7 :0]; 
               
               
                   
                   
               
             
          
         
       
     
     No assignment to REG 
     
       
         
               
               
             
               
             
           
               
                   
               
             
             
               
                 VINDEX 5,1  := 
                 IW[10:8]; 
               
               
                 VINDEX 5,2  := 
                 IW[7:5] 
               
             
          
           
               
                 DMEM_WRITE 5 ((IW[4:0] + REG[IW[7:5]]) [7:0], REG[IW[10:8]]) 
               
               
                   
               
             
          
         
       
     
     Conditional Jump 
     The conditional jump has two essentially different behaviours, depending on whether or not the jump is taken. This is reflected by two architecture description entries with nontrivial trigger_state macros. The example instruction is BEQZ 
     Jump not taken 
     
       
         
               
               
               
             
               
               
               
             
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER_IW 6  := 
                 IW[15:11] = beqz; 
               
             
          
           
               
                   
                 TRIGGER_STATE 6  := 
                 REG[IW[10:8]] /= 0; 
               
               
                   
                 UPDATE 6,PC  := 
                 (PC + 2)[7 :0]; 
               
             
          
           
               
                   
                 VINDEX 6,1  := 
                 IW[10:8]; 
               
               
                   
                 No update for REG. 
               
               
                   
                 DMEM_IDLE 6   
               
               
                   
                   
               
             
          
         
       
     
     Jump taken 
     
       
         
               
               
               
             
               
               
               
             
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 TRIGGER_IW 7  := 
                 IW[15:11] = beqz; 
               
             
          
           
               
                   
                 TRIGGER_STATE 7  := 
                 REG[IW[10:8]] = 0; 
               
               
                   
                 UPDATE 7,PC  := 
                 (PC + IW[7:0])[7 :0]; 
               
             
          
           
               
                   
                 INDEX 7,1  := 
                 IW[10:8]; 
               
               
                   
                 NO update for REG. 
               
               
                   
                 DMEM_IDLE 7   
               
               
                   
                   
               
             
          
         
       
     
     Correspondence Information 
     Classification of the Pipeline Stages 
     The total number of pipeline stages is
 
 n= 4
 
     Also, decoding is done in the second stage:
 
dec=2
 
     Most of the architecture description entries do not refer to a jump. Only the last one of the architecture description entries is about a jump taken, and this jump is decided in the 2 nd  stage, such that the only stage to be cancelled is the stage 1. 
     
       
         
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 jmp 1   
                 = 1 
               
               
                   
                 jmp 2   
                 = 1 
               
               
                   
                 jmp 3   
                 = 1 
               
               
                   
                 jmp 4   
                 = 1 
               
               
                   
                 jmp 5   
                 = 1 
               
               
                   
                 jmp 6   
                 = 1 
               
               
                   
                 jmp 7   
                 = 2 
               
               
                   
                   
               
             
          
         
       
     
     An interrupt is accepted in stage 3. This means that an instruction in stage 4 will not be cancelled by the interrupt, whereas all of the other instructions will be cancelled by the interrupt.
 
int=3
 
     There is only one architecture register file REG, and the data will be written back from stage 4.
 
writeback REG =4
 
     All of the data in the processor is forwarded to the decode stage which is stage 2. Therefore, all of the data that is needed by the instruction must be valid when this instruction is in stage 2 and when stage 2 does not stall. 
     
       
         
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 vstage 1,1   
                 = 2; 
               
               
                   
                 vstage 1,2   
                 = 2; 
               
               
                   
                 vstage 2,1   
                 = 2; 
               
               
                   
                 vstage 2,2   
                 = 2; 
               
               
                   
                 vstage 3,1   
                 = 2; 
               
               
                   
                 vstage 4,2   
                 = 2; 
               
               
                   
                 vstage 5,2   
                 = 2; 
               
               
                   
                 vstage 6,1   
                 = 2; 
               
               
                   
                 vstage 7,1   
                 = 2; 
               
               
                   
                   
               
             
          
         
       
     
     Stall Conditions 
     The example processor does not have one dedicated stall signal per each stage. Instead, the stall conditions are composed of several signals. This is captured by the correspondence information about the stalls. This correspondence information was obtained by the designer who explained the conditions under which the related stages do not move the instruction forward. 
     
       
         
               
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 stall 1   
                 := 
                 id_stall &amp;&amp; id_full; 
               
               
                   
                 stall 2   
                 := 
                 id_stall; 
               
               
                   
                 stall 3   
                 := 
                 mem_stall || stall_i; 
               
               
                   
                 stall 4   
                 := 
                 mem_stall; 
               
               
                   
                   
               
             
          
         
       
     
     Cancel Conditions 
     The processor does not have dedicated cancel signals. Again, the cancel conditions are expressed by expressions rather than single signals. 
     
       
         
               
               
             
           
               
                   
               
             
             
               
                 cancel 1 := 
                 (!id_stall &amp;&amp; opcode == beqz &amp;&amp; full 2 ) || int_valid_i; 
               
               
                 cancel 2 := 
                 int_valid_i; 
               
               
                 cancel 3 := 
                 0; 
               
               
                 cancel 4 := 
                 0; 
               
               
                   
               
             
          
         
       
     
     Full Conditions 
     
       
         
               
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 full 2   
                 := 
                 id_full &amp;&amp; !id_squash; 
               
               
                   
                 full 3   
                 := 
                 ex_full; 
               
               
                   
                 full 4   
                 := 
                 ma_full; 
               
               
                   
                   
               
             
          
         
       
     
     Start State
 
process_new_instruction_state:=true;
 
     Program Counter
 
pc:=if_Pc;
 
     Registers 
     The processor has only the register file REG. 
                                           result_write_REG 3     := ex_full &amp;&amp; ex_write_reg &amp;&amp; !int_valid_i;       result_write_REG 4     := ma_full &amp;&amp; ma_write_reg;       result_valid_REG 3     := ex_full &amp;&amp; !ex_read_from_mem;       result_valid_REG 4     := ma_full &amp;&amp; !mem_stall;       result_dest_REG 3     := ex_dest_reg;       result_dest_REG 4     := ma_dest_reg;       result_data_REG 3     := ex_result;       result_data_REG 4     := real_ma_result;            current_REG(unsigned reg_no) := register[reg_no];                    
Access Protocol Description
 
     The instruction memory address is passed in the first stage:
 
 ia= 1
 
     The instruction itself arrives when the execution is in the second stage:
 
 iv= 2
 
     The communication with the data memory is split into the stage 3 (to pass the address) and stage 4, to receive read data.
 
 da= 3
 
 dv= 4
 
     These macros describe how the processor signals read to the instruction memory and reads or writes to the data memory. 
                                                                                                   ibus_read(net[ ] pc) := imem_addr_o == pc;                iw :=   instruction_word;                dbus_idle := !ex_dmem_enable_o || int_valid_i;           dbus_read(net[ ] addr) := ex_dmem_enable_o                &amp;&amp; ! ex_dmem_write_o           &amp;&amp; ex_result[7:0] == addr;                dbus_rdata := dmem_data_i;           dbus_write(net[ ] addr, wdata) := ex_dmem_enable_o                &amp;&amp; ex_dmem_write_o           &amp;&amp; ex_result[7:0] == addr           &amp;&amp; ex_dmem_data_o == wdata;                        
Property Generation
 
     The generation of the property for the add instruction is sketched in this section. 
     The correspondence information about the register file REG is combined according to the section “Virtual Register File” to build the macros data_REG s (k) and valid_REG s (k) for all applicable stages s, i.e. for the stages 2, 3, or 4. 
     Next, the appropriate property schemata is to be selected. In the case of the ADD instruction which is described in the architecture description entry 1, the user specified with the correspondence information jmp 1 =1 that the architecture description block does not specify a jump instruction. Thus, property schemata simple_instruction is to be applied. 
     Then the architectural state needs to be replaced by implementation signals. In this step, the macros TRJGGER 0 , TRIGGER_IW 1 , TRIGGER_STATE 1 , INDEX 1,R , UPDATE 1,R , UPDATE 1,PC , VINDEX 1,i , ADDR 1  and WDATA 1  have to be replaced by trigger 0 , trigger_iw 1 , trigger_state 1 , index 1,R , update 1,R , update 1,PC , vindex 1,i , addr 1 , and wdata 1 . According to the rules described for this transformation the replacement for TRIGGER 0  is
 
trigger 0 =int_valid_i and data_REG 3 (0)
 
     Taking note of the correspondence information, the related replacements will be given below. Wherever useful, the result of the direct replacement is presented together with a more readable form. 
     
       
         
               
               
             
               
             
               
               
             
           
               
                   
               
             
             
               
                 ibus_read(iaddr) 
                 = imem_addr_o = iaddr; 
               
               
                 trigger_iw 1   
                 = ((iw @ t 2 )[15:11] = add) 
               
             
          
           
               
                 = (iw[15:11] @ t2 = add) 
               
             
          
           
               
                 trigger_state 1   
                 = true; 
               
               
                 update 1,PC   
                 = ((pc @ t 1 ) + 2)[7:0]; 
               
               
                 update 1,REG   
                 = ((data_REG 2  @ t 2 )((iw @ t 2 )[10:8])) + 
               
               
                   
                    ((data_REG 2  @ t 2 )((iw @ t 2 )[7:5])) 
               
               
                   
                 = (data_REG 2 (iw[10:8]) + data_REG 2 (iw[7:5])) @ 
               
               
                 index 1,REG   
                 = (iw @ t 2 )[4:2] 
               
               
                   
                 = iw[4:2] @ t 2 ; 
               
               
                 vindex 1,1   
                 = (iw @ t 2 )[10:8]; 
               
               
                 vindex 1,2   
                 = (iw @ t 2 )[7:5]; 
               
               
                   
               
             
          
         
       
     
     As the activity block ACT 1  specifies DMEM_IDLE (which means that no memory access is made), replacements for DATA 1  and WADDR 1  are not needed. 
     Now all placeholders of the property schemata are provided in the form of macros. What remains to be done is to expand the property schemata for the instruction and the implementation. This expansion already provides the required property into which the macros are expanded during the proof of the property against the implementation. 
     
       
         
               
             
               
               
             
               
             
               
               
             
               
               
               
               
             
               
               
               
             
               
               
               
               
             
               
               
               
             
               
               
               
               
             
               
               
               
             
               
               
               
               
             
               
               
               
             
               
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
               
             
               
               
             
               
               
               
               
             
               
             
               
               
               
               
             
               
               
             
               
               
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
               
               
               
               
             
               
               
               
             
               
               
             
               
               
               
             
               
               
             
           
               
                   
               
             
             
               
                 property add_instruction; 
               
               
                 dependencies: no_reset; 
               
               
                 for time_points: 
               
             
          
           
               
                   
                 t 0  = t, 
               
               
                   
                 t 1  &gt; t 0 , 
               
               
                   
                 t 2  &gt; t 1 , 
               
               
                   
                 t 3  &gt; t 2 , 
               
               
                   
                 t 4  &gt; t 3 ; 
               
             
          
           
               
                 assume: 
               
             
          
           
               
                   
                 //Describe the slot that is occupied by the instruction 
               
             
          
           
               
                   
                 at 
                 t 0 : 
                 stall 1  = 0 || cancel 1  = 1; 
               
             
          
           
               
                   
                 during [t 0 +1, t 1 −1]: 
                 stall 1  = 1; 
               
             
          
           
               
                   
                 at 
                 t 1 : 
                 stall 1  = 0; 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 −1]: 
                 stall 2  = 1; 
               
             
          
           
               
                   
                 at 
                 t 2 : 
                 stall 2  = 0; 
               
             
          
           
               
                   
                 during [t 2 +1, t 3 −1]: 
                 stall 3  = 1; 
               
             
          
           
               
                   
                 at 
                 t 3 : 
                 stall 3  = 0; 
               
             
          
           
               
                   
                 during [t 3 +1, t 4 −1]: 
                 stall 4  = 1; 
               
             
          
           
               
                   
                 at 
                 t 4 : 
                 stall 4  = 0; 
               
             
          
           
               
                   
                 // assume that no preceding property cancelled this one 
               
             
          
           
               
                   
                 during [t 0 +1, t 1 ]: 
                 cancel 1  = 0; 
               
               
                   
                 during [t 1 +1, t 2 ]: 
                 cancel 2  = 0; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 cancel 3  = 0; 
               
               
                   
                 during [t 3 +1, t 4 ]: 
                 cancel 4  = 0; 
               
             
          
           
               
                   
                 //assume that the processor is ready to execute next instruction 
               
             
          
           
               
                   
                 at 
                 t 0 : 
                 process_new_instruction_state; 
               
             
          
           
               
                   
                 //assume that instruction execution is not interrupted. 
               
             
          
           
               
                   
                 during [t 0 +1, t 3 ]: 
                 not trigger 0 ; 
               
             
          
           
               
                   
                 &lt;fetch&gt; // This is a cut point, see ITL section 
               
               
                   
                 //assume that iw contains the instruction 
               
               
                   
                 //that should be handled in this property. 
               
             
          
           
               
                   
                 at 
                 t 2 : 
                 trigger_iw 1 ; 
               
             
          
           
               
                   
                 &lt;validate_regs&gt; 
               
             
          
           
               
                   
                 at 
                 t 2 : 
                 trigger_state 1 ; 
               
             
          
           
               
                 prove: 
               
             
          
           
               
                   
                 at 
                 t 1 : 
                 ibus_read(pc @ t 0 +1); 
               
             
          
           
               
                   
                 &lt;fetch&gt; 
               
               
                   
                 //Prove that the virtual register file values are valid 
               
               
                   
                 //whenever they are to decide upon trigger_state. 
               
               
                   
                 //... trigger_state does not reference them here. 
               
               
                   
                 &lt;validate_regs&gt; 
               
               
                   
                 //Prove that the virtual register file values are valid 
               
               
                   
                 //whenever they are required. 
               
             
          
           
               
                   
                 at 
                 t 2 : 
                 valid REG,2 (vindex 1,1 ); 
               
               
                   
                 at 
                 t 2 : 
                 valid REG,2 (vindex 1,2 ); 
               
             
          
           
               
                   
                 at t 1 : 
                 process_new_instruction_state; 
               
               
                   
                 at t 1 +1: 
                 pc = update 1,PC ; 
               
             
          
           
               
                   
                 //Prove that the full signals are correctly created. 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 ]: 
                 full 2  = 1; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 full 3  = 1; 
               
               
                   
                 during [t 3 +1, t 4 ]: 
                 full 4  = 1; 
               
             
          
           
               
                   
                 //Prove that this instruction will not initiate cancels. 
               
             
          
           
               
                   
                 during [t 1 +1, t 2 ]: 
                 primary_cancel 1  = 0; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 primary_cancel 2  = 0; 
               
               
                   
                 during [t 3 +1, t 4 ]: 
                 primary_cancel 3  = 0; 
               
             
          
           
               
                   
                 //For all registers that get updated, prove their correct 
               
               
                   
                 //handling in the pipeline. 
               
             
          
           
               
                   
                 at 
                 t 3 : 
                 if result_valid R,3  = 1 
               
               
                   
                   
                   
                 then next(result_valid R,4 ) = 1 
               
               
                   
                   
                   
                 end if; 
               
             
          
           
               
                   
                 during [t 2 +1, t 3 ]: 
                 result_write R,3  = 1; 
               
               
                   
                 during [t 3 +1, t 4 ]: 
                 result_write R,4  = 1; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 result_dest R,3  = index 1,R ; 
               
               
                   
                 during [t 3 +1, t 4 ]: 
                 result_dest R,4  = index 1,R ; 
               
               
                   
                 during [t 2 +1, t 3 −1]: 
                 if (result_valid R,3  = 1) 
               
               
                   
                   
                 then next(result_valid R,3 ) = 1 
               
               
                   
                   
                 end if; 
               
               
                   
                 during [t 3 +1, t 4 −1]: 
                 if (result_valid R,4  = 1) 
               
               
                   
                   
                 then next(result_valid R,4 ) = 1 
               
               
                   
                   
                 end if; 
               
               
                   
                 during [t 2 +1, t 3 ]: 
                 if (result_valid R,3 ) 
               
               
                   
                   
                 then result_data R,3  = update 1,R ; 
               
               
                   
                   
                 end if; 
               
               
                   
                 during [t 3 +1, t 4 ]: 
                 if (result_valid R,4 ) 
               
               
                   
                   
                 then result_data R,4  = update 1,R ; 
               
               
                   
                   
                 end if; 
               
               
                   
                 at t 4 +1: 
                 current R (index R ) = update 1,R   
               
             
          
           
               
                   
                 //there is no register in this example that does not get updated. 
               
               
                   
                 //the architecture description contains DMEM_IDLE 
               
             
          
           
               
                   
                 at t da : 
                 dbus_idle; 
               
             
          
           
               
                 left_hook: 
                 t0; 
               
               
                 right_hook: 
                 t1; 
               
               
                 end property; 
               
               
                   
               
             
          
         
       
     
     The instantiation of this property makes the proof part of the partial property add_instruction.fetch and add_instruction.validate_regs equal, which mean that the proof of the partial property add_instruction.validate_regs is skipped. 
     The foregoing description of the preferred embodiment of the invention has been presented for purposes of illustration and description. It is not intended to be exhaustive or to limit the invention to the precise form disclosed, and modifications and variations are possible in light of the above teachings or may be acquired from practice of the invention. The embodiment was chosen and described in order to explain the principles of the invention and its practical application to enable one skilled in the art to utilize the invention in various embodiments as are suited to the particular use contemplated. It is intended that the scope of the invention be defined by the claims appended hereto, and their equivalents. The entirety of each of the aforementioned documents is incorporated by reference herein.