Abstract:
A system for representing a physical environment comprises a first store for holding a set of state bits, a second store for holding a set of input bits, an input device for inputting a set of initial states of said state bits into said first store, means for implementing a set of state transition functions for manipulating said input bits and said state bits, and means for generating input bits satisfying a set of constrains representing restrictions on the physical environment.

Description:
FIELD OF THE INVENTION 
     The present invention relates to a system for representing or simulating operation of a physical environment, and is applicable to a technique for proving properties of a system, and more especially but not exclusively to a technique for proving properties of a hardware system. 
     BACKGROUND OF THE INVENTION 
     Although a hardware system may itself be deterministic such that its behaviour may be determined completely by inputs to the system, the same may not be true of the environment in which the hardware system exists. Typically, the behaviour of the environment is dependent upon such a large number of inputs that it is not possible to provide a deterministic model of the behaviour of the environment which therefore appears to be a non-deterministic system. It is also possible that the environment is mathematically non-deterministic, in the sense that even if all of the inputs could be assessed, the outputs are still not known. 
     The present invention finds particular application in synthesising the behaviour of hardware systems within their environment for example for the development-testing of a hardware system. It is also possible to apply the invention to modelling the behaviour of software systems for testing purposes. 
     SUMMARY OF THE INVENTION 
     According to a first aspect of the present invention there is provided a system for representing a physical environment comprising a first store for holding a set of state bits; a second store for holding a set of input bits; an input device for inputting a set of initial states of said state bits into said first store; means for implementing a set of state transition functions for manipulating said input bits and said state bits; 
     and means for generating input bits satisfying a set of constrains representing restrictions on the physical environment. 
     According to a second aspect of the present invention there is provided a method of operating a computer system to generate results simulating operation of a hardware system in a predetermined physical environment, the method comprising generating input bits satisfying a set of constraints representing restrictions on the physical environment; manipulating said input bits with a set of state bits according to a set of state transition functions to produce a set of outputs; and using said outputs to generate said results. 
     According to a third aspect of the present invention there is provided a method for proving the properties of a system comprising: 
     providing at least one constraint upon at least a subset of the inputs to the system; 
     deriving from the or each constraint a respective set of input relationships; 
     processing the input relationships to provide correction conditions for at least a first input; 
     providing a set of unconstrained inputs; and 
     applying the correction conditions to said first inputs. 
     A standard representation for a deterministic system is as a Mealy machine. A Mealy machine is a sequential logic system in which the outputs are determined by both the inputs and a previously-stored state or states. Mealy machines may be formed by hardware arrangements of sequential logic circuitry and such arrangements can be represented by a state graph consisting of plural sets of state bits, each set of state bits being connected to a respective next sequential state by a transition function. 
     Although it would be possible to provide a physical Mealy machine having physical sequential logic circuitry, the preferred embodiment of the present invention provides a software model of a Mealy machine in which numbers are assigned to each of the state bits and to each input bit, transition functions, observation functions and initial states being set as binary decision diagrams over these variable numbers. 
    
    
     BRIEF DESCRIPTION OF THE FIGURES 
     An embodiment of the invention will now be described with reference to the accompanying drawings in which: 
    
    
     DESCRIPTION OF THE PREFERRED EMBODIMENT 
     FIG. 1 is a diagram illustrating the application of the invention, 
     FIG. 2 is a diagram showing an environment and a circuit subject to the environment; 
     FIG. 3 shows a block diagram of the invention. 
     FIG. 1 shows a diagrammatic example for illustrating the application of the invention. FIG. 1 shows an arrangement of three circuit blocks (10, 11, 12), the arrangement having three inputs (I1, I2, I3) and an output (0). Circuit block (10) has four inputs (A, B, C, D) and an output (E). For the sake of example, the inputs A and B of circuit block (10) are provided by outputs of circuit block (11), itself having inputs (I2, I3). Input (C) of circuit block (10) is provided by a circuit input (I1) and input (D) of circuit block (10) is provided by an output (F) of circuit block (12), which circuit block receives an input from the output (E) of circuit block (10). 
     It would be possible to model the behaviour of the circuit block (10) entirely in isolation, but such a model may include conditions which do not occur in practical operation, due to the environment within which circuit block (10) resides. For example, the inputs A and C may be constrained by circuit block (11) to be always complementary, in which case operating the model for non-complementary A and C would not be useful. 
     Referring now to FIG. 2, the invention provides a model (21) of the environment of circuit block (10). The environment shown in FIG. 2 has two parts, the first part being the input environment (21A) and the second being the output environment (21B). In general, there will be an environment associated with the totality with the circuit block (10), but for simplicity only the input environment (21A) will be considered at present. The effect of the input environment (21A) is to impart such constraints upon a non-constrained set of inputs (P, Q, R, S) as would be necessary to simulate the inputs (A, B, C, D). For example, if the circuit block (11) were a flip flop, then the previously-discussed constraint upon the inputs (A, B) would exist, namely that these would be mutually complementary. If input (C) were a reset input then a constraint upon input (C) could be C═0 for normal operation to occur. 
     In FIG. 2, the environment model (21A) effects logical operation on the input (P) to provide the environment output (A) as input (10) and likewise effects logical operations on each of inputs (Q, R, S) to provide respective environment outputs (C, D, B) as inputs (C, D, B) to 10, such that no matter how or when the logic states of inputs P-S vary, the inputs to circuit block (10) are only those which could exist if the circuit block (10) were located as shown in FIG. 1. 
     The invention proposes that if a constraint (T) is given by 
     
         NOT I &amp; T0+I &amp; T1 
    
     where I is an input and neither T0 nor T1 depend on I, then I can be generated from a new input J which satisfies the relation 
     
         I=NOT J &amp; NOT T0+J &amp; T1. 
    
     In the example given above for the reset signal, there are two possible states of the input. The first state is C=RESET=1 and the second state is C=RESET=0. To satisfy the specified constraint that C=0 the first state does not exist and the second state always exists, thus (RESET=1)=0 and (RESET=0)=1. Thus, using the above relationship between I and J, for the case where C, represents the input to be constrained by &#34;RESET =0&#34; and Q is an unconstrained input described as J then the relationship between C and Q is given by: 
     
         C=Q &amp; 0 +(NOT Q) &amp; (NOT 1) 
    
     Turning to the other example above, the constraint is given by: 
     
         A=NOT B 
    
     In this case, assuming that the input B is directly provided by the input S so that B=S then it is necessary to constrain the signals applied to the input A regardless of the values of inputs P and S to satisfy the constraint above. 
     If A=1 then according to the constraint this can only occur when B (=S)=0. If A=0, this can only occur when B (=S)=1. 
     Thus the relationship may be reflected by the states (A=1, NOT B), (A=0, B). 
     Thus using the method of the invention: 
     
         A=P &amp; (NOT S)+(NOT P) &amp; (NOT S) 
    
     The method is to synthesise an environment from a Mealy machine with constraints and prove properties about the Mealy machine in that environment. The basic idea is to generate a set of inputs to the Mealy machine which are guaranteed to satisfy the constraints. If the constraint is A and it is equal to &#34;!i &amp; AO+AO+i &amp; A1&#34;, where i is an input and neither AO nor A1 depend on i (the Shannon decomposition), then i is generated from a new input, j, by the equation &#34;i=!j &amp; !AO+j &amp; A1&#34;. This equation for i does in fact satisfy the constraint (insofar as is possible) because: 
     
         A=!i &amp; AO+i &amp; A1 
    
     
         A=!(!j &amp; !AO+j &amp; A1) &amp; AO+(!j &amp; !AO+j &amp; A1) &amp; A1 
    
     
         A=(!j &amp; AO+j &amp; !A1) &amp; AO+(!j &amp; !AO+j &amp; A1) &amp; A1 
    
     
         A=!j &amp; (AO+!AO &amp; A1)+j &amp; (AO &amp; !A1+A1) 
    
     
         A=!j &amp; (AO+A1)+j &amp; (AO+A1) 
    
     
         A=AO+A1 
    
     This means that so long as there is a possible assignment to i which satisfies the constraint, then the equation for i is such an assignment. Equations for all the other inputs can be generated using the constraint &#34;AO+A1&#34;. 
     As well as understanding that the equation for i satisfies the constraint, it must be ensured that all possible values of i are generated. Therefore, suppose that &#34;r&#34; is an assignment to all of the inputs which satisfies &#34;A&#34;. If &#34;r(i)=0&#34;, then we must have &#34;r(AO)=1&#34; (ie, &#34;AO&#34; evaluates to &#34;1&#34; under the assignments defined by &#34;r&#34;) since &#34;r(A)=1&#34;; now, setting &#34;r(j)=0&#34;, it is clear that the equation for i evaluates to 0. Similarly, if &#34;r(i)=1&#34; then &#34;r(A1)=1&#34; and if we set &#34;r(j)=1&#34; then the equation for i evaluates to 1. 
     Note that if the constraint complete determines i, ie &#34;A1=!AO&#34;, then the equation for i reduces to &#34;A1&#34; and the input i will be completely eliminated from the description. 
     Referring to FIG. 3, constraints 50 are processed to provide correction functions 51 and these are applied to unconstrained input bits 52 to provide constrained input bits 53. Initial states 60 are used to set state bits 61 and these together with the constrained input bits are used as inputs to provide state transition functions 63 and observation functions 64. 
     One application is to modelling system invariants. 
     When a state diagram has one or more states which are residual in that the state or states are not accessible via normal state transitions, such invariant states can only be accessed by initialising the system into the residual state. If the environment obeys the constraints, the system must guarantee to maintain the residue. This however must be proved by using standard model--checking techniques. However once proved the state may be encoded using the above-mentioned environment synthesis technique using a new set of state bits to generate a set of signals which guarantee the state invariant. To prove that the new Mealy machine is sequentially equivalent to the original, the original state bits are added back to the observation function and under the assumption that the input and state observations of the two machines are equal, then the outputs and the next state observations are equal. 
     Thus there has been described a system for representing a physical environment and a method of operating a computer system to generate results simulating operation of a hardware system.