SOURCE ARCHIVE
EXTRACTED CONTENT
81,112 chars Verification of Pipelined Microprocessors by Correspondence Checking
in Symbolic Ternary Simulation¹
Miroslav N. Velev* Randal E. Bryant‡, *
mvelev@ece.cmu.edu randy.bryant@cs.cmu.edu
*Department of Electrical and Computer Engineering‡
School of Computer Science
Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A.
Abstract employing X’s reduces the number of simulation patterns,
often dramatically. However, ternary simulators will some-
This paper makes the idea of memory shadowing [5] times produce a value X, when an exhaustive analysis applicable to symbolic ternary simulation. Memory shad- would determine the value to be binary (i.e., 0 or 1). This owing, an extension of Burch and Dill’s pipeline verifica- has been resolved by combining ternary modeling with tion method [6] to the bit level, is a technique for symbolic simulation [1], such that the signals can accept providing on-the-fly identical initial memory state to two symbolic ternary values, instead of the scalar values 0, 1, different memory execution sequences. We also present an and X. Each symbolic ternary value is represented by a algorithm which compares the final states of two memories pair of symbolic Boolean expressions, defined over a set of for ternary correspondence, as well as an approach for symbolic Boolean variables, that encode the cases when generating efficiently the initial state of memories. These the signal would evaluate to 0, 1, or X. The advantage of techniques allow us to verify that a pipelined circuit has symbolic ternary simulation is that it efficiently covers a behavior corresponding to that of its unpipelined specifi- wide range of circuit operating conditions with a single cation by simulating two symbolic ternary execution symbolic simulation pattern that involves far fewer vari- sequences and comparing their final memory states. ables than would be required for a complete binary sym- Experimental results show the potential of the new ideas. bolic simulation. One of the hurdles in simulation has been the repre- sentation of memory arrays. These have been traditionally
Introduction modeled by explicitly representing every memory bit. While this is not a problem for conventional simulation, This paper makes memory shadowing [5] applicable symbolic simulation would require a symbolic variable to
to symbolic ternary simulation. Memory shadowing is a denote the initial state of every memory bit. Therefore, the technique for providing on-the-fly identical initial memory number of variables would be proportional to the size of state to two different memory execution sequences. Com- the memory, and would be prohibitive for large memory bined with an algorithm which compares the final states of arrays. two memories, memory shadowing allows us to verify that This limitation is overcome in [18] by replacing each a pipelined circuit has behavior corresponding to that of its memory array with an Efficient Memory Model (EMM), unpipelined specification. This is done by simulating two assuming that the memory address and control inputs can symbolic execution sequences and comparing their final accept only symbolic binary values. The EMM is a behav- memory states. However, the method presented in [5] ioral model, which allows the number of symbolic vari- assumes simulation over symbolic binary values. ables used to be proportional to the number of distinct Ternary simulation, where the “unknown” value X is symbolic memory locations accessed rather than to the used to indicate that a signal can be either 0 or 1, has size of the memory. It is based on the observation that a proven to be more powerful than binary simulation for typical verification execution sequence usually accesses both validation and formal verification of digital circuits only a limited number of distinct symbolic locations. [17]. Given that the simulation algorithm satisfies a mono- Memory state is represented in the EMM by a list of tonicity property, any binary values resulting when simu- entries encoding the relative history of memory opera- lating patterns with X’s would also result when the X’s are tions. The list interacts with the rest of the circuit by replaced by any combination of 0’s and 1’s. Hence, means of a software interface developed as part of the symbolic simulator. 1. This research was supported in part by the SRC under A ternary version of the EMM is presented in [19], contract 97-DC-068. where the memory address and control inputs are allowed
Copyright 1998 IEEE. Published in the Proceedings of CSD’98, March 1998 Fukushima, Japan. Personal use of this material
is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works, must be obtained from the IEEE. Contact: Manager, Copyrights and Permissions / IEEE Service Center / 445 Hoes Lane / P.O. Box 1331 / Piscataway, NJ 08855-1331, USA. Telephone: + Intl. 908-562-3966.
to accept symbolic ternary values, while the EMM will F behave as a conservative approximation to the replaced memory array. Conservative approximation means that QSpec Spec Q′Spec false positive verification results are guaranteed not to occur, although false negative verification results are pos- Abs Abs sible. Since symbolic ternary values are a superset of sym- bolic binary values, the ternary EMM is a superset of the F binary EMM from [18], while also exploiting the compu- QImpl Impl Q′Impl tational power of symbolic ternary simulation. Burch and Dill also use a symbolic representation of Figure 1. Commutative diagram for the correctness crite- memory arrays [6]. They apply uninterpreted functions rion with equality, which allows them to introduce only a sin- The Burch and Dill approach is conceptually elegant gle symbolic variable to denote the initial state of the in the way it uses a symbolic simulation of the hardware entire memory. Each Write or Read operation results in design to automatically compute an abstraction function building a formula over the current state of the memory, so from the pipeline state to the user-visible state. Namely, that the latest memory state reflects the sequence of mem- starting from a general symbolic initial state QImpl they ory writes. However, we need bit-level data for various simulate a flush of the pipeline by stalling it for a sufficient memory locations in order to verify the data path. This number of cycles that will allow all partially executed requires our algorithms to introduce symbolic variables instructions to complete. Then, they consider the resulting proportional to both the number of distinct symbolic mem- state of the user-visible memory elements (e.g., the regis- ory locations accessed and to the number of data bits per ter file and the program counter) to be the matching state location. Furthermore, we need the flexibility to include QSpec. new symbolic memory locations as part of the initial mem- Burch and Dill’s implementation [6][7] of their ory state at any point in the verification process. Hence, method requires a high level abstract model of the imple- the memory state in our case reflects the relative history of mentation that still exposes relevant design issues, such as memory operations, rather than the sequence of writes. pipelining. They work on models that completely repre- This difference will become clear as we present our algo- sent the control path of the processor, but hide the func- rithms.The memory shadowing technique [5] is an extension tional details of the data path by means of uninterpreted of Burch and Dill’s pipeline verification method [6] to a functions. Our implementation of Burch and Dill’s bit-level circuit verification. The correctness criterion of method, presented in this paper, allows verification at the Burch and Dill’s method is expressed with a commutative bit level. By verifying at the bit level, we avoid the need to diagram and an underlying abstraction function - see Fig- construct an abstracted model of the circuit. We can verify ure 1. This correctness criterion is not new to verification. the actual hardware design, given a logic gate-level or reg- It has been introduced by Hoare [8] for verifying computa- ister-transfer-level description. tions on abstract data types in software, and has been used An extensive body of research has been spawned by by Bose and Fisher [2] to verify pipelined circuits. All Burch and Dill’s method. Sawada and Hunt [16] have these verification methods are based on comparing an combined it with theorem proving, assuming the availabil- implementation transformation FImpl against a specifica- ity of a set of invariants that completely specifies the prop- tion transformation FSpec. The assumption is that the two erties of the pipelined processor in correct operation. transformations start from a pair of matching initial states Burch [7] has extended it to superscalar processor verifica-
- QImpl and QSpec, respectively - where the match is deter- tion by proposing a new flushing mechanism (notice that mined according to some abstraction function Abs. The the method requires an arbitrary abstraction function that correctness criterion is that the two transformations should makes the correctness criterion diagram commute) and by yield a pair of matching final states - Q′Impl and Q′Spec, decomposing the commutative diagram from [6] into three respectively - where the match is determined by the same more easily verifiable commutative diagrams. The correct- abstraction function. In other words, the abstraction func- ness of this decomposition is proven by Windley and tion should make the diagram commute. Note that there Burch [21]. Jones, Seger, and Dill [12] propose the use of are two paths from QImpl to Q′Spec. We will refer to the the pipeline as a specification for the correctness of its for- one that involves FImpl as the implementation side of the warding logic. They apply two specially designed instruc- commutative diagram, while the one that involves FSpec tion sequences that should yield identical behaviors and will be called the specification side. compare their effects on the register file. One of the sequences completely fills the pipeline with instructions and then flushes it with a sequence of NOPs, while the
2
other consists of the same instructions but separated with data intensive systems. Both methods avoid building a as many NOPs as to avoid the exercising of the forwarding transition function for the system by constructing it on- logic. the-fly during symbolic simulation. This allows them to The contributions of this paper are: 1) combining the employ the EMM for representing the state of the system memory shadowing technique [5] with the ternary EMM in a very efficient way. [19] in order to support the efficient symbolic ternary sim- In the remainder of the paper, Section 2 summarizes ulation when extending Burch and Dill’s pipeline verifica- Burch and Dill’s pipeline verification method. Section 3 tion method [6] to completely model the functionality of describes the symbolic domain used in our algorithms. the data path at the bit level; 2) a modified correctness cri- Section 4 presents the assumptions, data structures, and terion in the form of a commutative diagram targeted to algorithms of the ternary EMM. The memory shadowing symbolic ternary simulation; 3) a variable-group indexing technique for providing on-the-fly identical initial memory technique for generating the initial state of EMMs; and state to two different ternary execution sequences is 4) experimental results with a shortened MIPS pipeline explained in Section 5, which also presents an algorithm showing the potential of the new ideas. that compares for correspondence the states of two mem- We consider two forms of verification, supported by ory arrays. The variable-group indexing technique for gen- our tool: 1) Symbolic Trajectory Evaluation (STE) [17], erating the initial state of EMMs is presented in Section 6. where one proves that a circuit satisfies a specification The verification methodology for ternary correspondence given as a temporal logic formula; and 2) Correspondence checking by applying memory shadowing is described in Checking, where one proves a correspondence between Section 7. Experimental results are summarized in Section two circuits by evaluating two execution sequences start- 8. Finally, conclusions are drawn and future work is out- ing from a common initial state and showing that they lined in Section 9. yield identical final user-visible states, based on the com- mutative diagram of Figure 1. We propose using both 2. Burch and Dill’s Pipeline Verification forms as part of a four step approach for the verification of Method pipelined processors. The first step is to use STE to verify the transistor-level memory elements (both memory arrays When verifying a pipelined processor, Burch and Dill and latches), independently from the rest of the circuit. [6] assume the availability of a specification non-pipelined Pandey and Bryant [13][14] have combined symmetry circuit, which has user-visible state U = {0, 1}n and input reductions and STE to enable the verification of very large state I = {0, 1}m. The implementation (possibly pipelined) memory arrays at the transistor level. The second step is to circuit is assumed to have the same user-visible and input replace the memory arrays with EMMs for both the imple- state, although it can also have pipeline state P = {0, 1}k. mentation and the specification circuits. The third step is The combined user-visible and pipeline state of the imple- to use STE to verify the non-pipelined specification cir- mentation is then U × P and will be written in the cuit, which is assumed to support the same instruction set form 〈Õ u , Õp 〉. Each of the circuits is characterized with its architecture and to have the same user-visible state as the transition function δI : I × (U × P) → (U × P) for the pipelined processor. One of our previous papers describes implementation, and δS : I × U → U for the specifica- the use of the EMM in this context [18]. The fourth and tion. last step is to perform correspondence checking between Burch and Dill further assume that if the implementa- the pipelined processor and its specification. This step is tion is pipelined, it has or can be modified to include a stall the focus of the present work. input. When asserted, this input will prevent new instruc- Another form of verification is symbolic model tions from entering the pipeline, while letting partially checking [11]. It uses the transition relation of a system executed instructions advance and allowing the pipeline and an initial set of states in order to find the set of reach- state to be flushed. The notation Stall will be used for the able states and to verify whether they satisfy certain prop- implementation’s transition function when the stall input erties. The temporal logic supported by symbolic model is asserted. It is also assumed that the two circuits support checking is very rich. However, the method requires two the same instruction set architecture and start from the symbolic Boolean variables per bit of state in order to same arbitrary initial user-visible state. build the transition relation. This precludes it from being The method uses a projection function, used for verification of systems with very large state Proj : (U × P) → U, which removes all but the user-vis- spaces, and makes it most applicable for verification of ible state from the implementation, and an abstraction control intensive systems, such as communication and function, cache coherence protocols. On the other hand, STE and Abs(〈Õ u , Õp 〉) =˙ Proj(Stalll(〈Õ Correspondence Checking are suitable for verification of u , Õp 〉)),
3
which maps the combined user-visible and pipeline notation 〈a1, ... , an〉 to explicitly represent the address set state 〈Õ u , Õp 〉 of the implementation to its user-visible expression a, where ai is the control expression for the state. This is done by stalling the pipeline for a sufficient corresponding bit position of a. Data set expressions will number of cycles l, that would allow all partially executed have a similar explicit representation, but with w bits. instructions to complete (so that the pipeline is flushed), Symbolic variables will be introduced in each of the and then stripping off all but the user-visible state. The domains and will be used in expression generation. correctness criterion expressed by Figure 1 is The symbol UD will designate the universal data set. ∀ Õx , Õ u , Õp .Abs(δI(Õx , 〈Õ u , Õp 〉)) = It will represent the most general information about a set δS(Õx , Abs(〈Õ of data. In ternary logic, UD can be represented by a vector u , Õp 〉)) , (1) of control expressions consisting entirely of X’s. where Õx is an input combination that allows the imple- We will use the term context to refer to an assignment mentation and the specification to execute one cycle with- of values to the symbolic variables. A Boolean expression out stalling, i.e., to start executing one instruction (and to can be viewed as defining a set of contexts, namely those complete it in the case of the specification). for which the expression evaluates to true. A symbolic predicate is a function which takes sym- 3. Symbolic Domain bolic arguments and returns a symbolic Boolean expres- sion. The following symbolic predicates will be used in We will consider three different domains - control, our algorithms, where c is of type CExpr, and a is of type address, and data - corresponding to the three different ASExpr: types of information that can be applied at the inputs of a Hard(c) =˙ c.h ∧ ¬c.l , (2) memory array. A control expression c will represent the value of a node in ternary symbolic simulation and will Soft(c) =˙ c.h ∧ c.l , (3) have a high encoding c.h and a low encoding c.l, each of Unique(a) =˙ n ¬ Soft(a which is a Boolean expression. The ternary values that can i = 1 i) . (4) be represented by a control expression c are shown in The predicates Hard and Soft define the conditions for Table 1. We would write [c.h, c.l] to denote c. It will be their arguments to be the ternary 1 and X, respectively. assumed that c.h and c.l cannot be simultaneously false. The predicate Unique defines the condition for the address The types BExpr, CExpr will denote respectively Bool- set expression a to represent a unique or single address. ean and control expressions in the algorithms to be pre- The selection operator ITE (for “If-Then-Else”), sented. when applied on three Boolean expressions, is defined as: Ternary value c.h c.l ITE(b, t, e) =˙ (b ∧ t) ∨ (¬b ∧ e) . (5) 0 false true Address set comparison with another address set is imple- 1 true false mented as:a1 = a2 =˙ ¬ n [(a1.hi ⊕ a2.hi) ∨ (a1.li ⊕ a2.li)] , (6) X true true where a1.hi and ia= 11.li represent the high and low encodings Table 1. 2-bit encoding of ternary logic aof the control expression for bit1 i of address set expression . Address set selection a1 ← ITE(b, a2, a3) is imple- The memory address and data inputs, since connected mented by selecting the corresponding bits: with circuit nodes, will receive ternary values represented a1.hi ← ITE(b, a2.hi, a3.hi) , as control expressions. Hence, addresses and data will be a represented by vectors of control expressions having width 1.li ← ITE(b, a2.li, a3.li) , i = 1, ... , n . (7) n and w, respectively, for a memory with N = 2n locations, Checking whether address set a1 is a subset of address set each holding a word consisting of w bits. Observe that an a2 is done by: n X at a given bit position represents the “unknown” value, a i.e., the bit can be either 0 or 1, so that many distinct 1 ⊆ a2 ˙= ¬ i = 1 (a1.hi ∧ ¬a2.hi ∨ a1.li ∧ ¬a2.li) , (8) addresses or data will be represented. To capture this prop- and checking address sets a1 and a2 for overlap is imple- erty of ternary simulation, we introduce the type ASExpr mented by: n (address set expression) to denote a set of addresses. Simi- Overlap(a1, a2) =˙ (a1.li ∧ a2.li ∨ a1.hi ∧ a2.hi). (9) larly, the type DSExpr (data set expression) will denote a i = 1 set of data. Note that in both cases, a set will be repre- The definition of symbolic predicates over data set expres- sented by a single vector of ternary values. We will use the sions is similar, but over vectors of width w.
4
wn WriteAddr0 MEMORY ReadAddr0 n LATCH
WriteData0 ARRAY ReadData0 w
WriteEnable0 ReadEnable0 1 WriteAddr ReadAddr 1
w WriteData ReadData w
wn WriteAddrP ReadAddrQ n
WriteDataP ReadDataQ w
WriteEnableP ReadEnableQ
(a) (b)
Figure 2. (a) A memory array that can be modeled by an EMM; (b) A latch modeled by an EMM
Note that all of the above predicates are symbolic, system can be represented with such EMMs and possibly
i.e., they return a symbolic Boolean expression and will be some extra logic. For example, a latch can be viewed as a true in some contexts and false in others. Therefore, a memory array with a single address, so that it can be repre- symbolic predicate cannot be used as a control decision in sented as an EMM with one write and one read port, both algorithms. The function Valid(), when applied to a sym- of which have the same number of data bits and only one bolic Boolean expression, will return true if the expres- address input, which is identically connected to the same sion is valid or equal to true (i.e., true for all contexts), constant logic value (e.g., true) - see Figure 2.b. and will return false otherwise. We can make control deci- The interaction of the memory array with the rest of sions based on whether or not an expression is valid. the circuit is assumed to take place when a port Enable We will also need to form a data set expression which signal is not 0 (i.e., false). In case of multiple port is the union of two data set expressions, d1 and d2. If these Enables not being 0 simultaneously, the resulting differ in exactly one bit position, i.e., one of them has a 0 accesses to the memory array will be ordered according to and the other a 1, then the ternary result will have an X in the priority of the ports. It will be assumed that the memo- that bit position and will be an exact computation. How- ries respond instantaneously to any requests. ever, if d1 and d2 differ in many bit positions, these will be During symbolic simulation, the memory state is rep- represented as X’s in the ternary result and that will not resented by a list containing entries of the form 〈h, s, a, d〉, always yield an exact computation. For example, if where h and s are Boolean expressions denoting the set of d1 = 〈0, 1〉 and d2 = 〈1, 0〉, the result will be 〈X, X〉 and will contexts for which the entry is defined, a is an address set not be exact, as it will also contain the data set expressions expression denoting a memory location, and d is a data set 〈0, 0〉 and 〈1, 1〉, which are not subsets of d∼1 or d2. We expression representing the contents of this location. The define the operation approximate union d1 ∪ d2 of two context information is included for modeling memory sys- data set expressions as: tems where the Write and Read operations may be per- [d1 ∪∼ d2 ]i =˙ [d1.hi ∨ d2.hi, d1.li ∨ d2.li] , formed conditionally on the value of a control signal c. i = 1, ... , w . (10) The Boolean expression h represents the contexts Hard(c) ∧ Unique(a), when the control signal was 1, and We have used Ordered Binary Decision Diagrams the address a was unique. Under contexts h the location a (OBDDs) [4] to represent the Boolean expressions in our is definitely overwritten with data d. The Boolean expres- implementation. However, any representation of Boolean sion s represents the contexts expressions can be substituted, as long as function Valid() Soft(c) ∨ Hard(c) ∧ ¬Unique(a), when the control signal can be defined for it. was an X, or it was a 1 and the address was not unique. Under contexts s the location a is uncertainly overwritten 4. Efficient Modeling of Memory Arrays in with data d. Initially the list is empty. The type List will be Symbolic Ternary Simulation used to denote such memory lists. The list interacts with the rest of the circuit by means 4.1 Overview of a software interface developed as part of the symbolic simulation engine. The interface monitors the memory The EMM models memory arrays with write and/or input lines. Should a memory input value change, given read ports, all of which have the same numbers of address that its corresponding port Enable value c is not 0, a and data bits - n and w, respectively - as shown in Figure Write or a Read operation will result, as determined by the 2.a. An inward/outward triangle indicates an enable input type of the port. The Address and Data lines of the port of a write/read port. The assumption is that every memory will be scanned in order to form the address set expression
5
. . .
. . .
. . .
. . .
a and the data set expression d, respectively. A Write oper- procedure Write(List mem, CExpr c, ASExpr a, DSExpr d) ation takes as arguments both a and d, while a Read opera- /* Write data d to location a under control c / tion takes only a. These operations will be presented h ← Hard(c) ∧ Unique(a) shortly. s ← Soft(c) ∨ Hard(c) ∧ ¬Unique(a) A Read operation retrieves from the list a data set InsertTail(mem, 〈h, s, a, d〉) expression rd that represents the data contents of address a. The software interface completes the read by scheduling Figure 3. Implementation of the Write operation the Data lines of the port to be updated with the data set expression ITE(Hard(c), rd, ITE(Soft(c), (rd ∼ function Read(List mem, ASExpr a) : DSExpr ∪ d), d)). / Attempt to read from location a */ Again, this guarantees that the EMM provides a conserva- tive approximation of the replaced memory array. The rou- rd ← UD tines needed by the software interface for accessing the list if ¬Valid(¬Unique(a)) then are presented next. for each 〈eh, es, ea, ed〉 in mem from head to tail do After completing a Write operation, the software hard_match ← eh ∧ (ea = a) interface checks every read port of the same memory for a soft_match ← [es ∨ eh ∧ ¬(ea = a)] ∧ Overlap(ea, a) possible on-going read (as determined by the read port rd ← ITE(hard_match, ed, Enable value being different from 0) from an address ITE(soft_match, (ed ∪∼ rd), rd)) that overlaps the one of the recent write. For any such port, return rd a Read operation is invoked immediately and the∼ Data Figure 4. Implementation of the Read operation lines of the read port are updated with rd ∪ d where rd is the data set expression returned by the Read, and d is the For each list entry, function Read() builds the Bool- data set expression that would otherwise appear on the ean expression hard_match that indicates the contexts Data lines at that time. This guarantees that the EMM under which the entry is hard (definite) and its (unique) would behave as a conservative approximation of the address equals the read address a. Under these contexts, replaced memory array. that element’s data ed is selected. Else, under the contexts expressed by the Boolean expression soft_match, the 4.2 Memory Support Operations approximate union of the element’s data and the previ- The list entries are kept in order from head (low pri- ously formed data is selected. Finally, under the contexts ority) to tail (high priority). Intuitively, the entries towards when both hard_match and soft_match are false, the previ- the low priority end correspond to the initial state of the ously formed data is kept. memory, while the ones at the high priority end represent UD is used as the default data set expression. The recent memory updates, with the tail entry being the result contexts for which Read() does not find a matching of the latest Write operation. Entries may be inserted at address in the list are those for which the addressed mem- either end, using procedures InsertHead() and InsertTail(). ory location has never been accessed by a write. The data set expression UD is then returned to indicate that the loca- 4.3 Implementation of Memory Write and Read tion may contain arbitrary data. Operations The Read operation is designed to be precise only in the contexts when the argument address is unique, and to The Write operation, shown as a procedure in Figure return UD otherwise. The expression soft_match is defined 3, takes as arguments a memory list, a control expression so that for any list entry, whose address intersects the read denoting the contexts for which the write should be per- address a, the approximate union of the entry’s data set formed, and address set and data set expressions denoting expression and the previously formed data set expression the memory location and its desired contents, respectively. is selected. Note that in the contexts when the currently As the code shows, the write is implemented by simply examined list element is hard, as determined by eh, we inserting an element into the tail (high priority) end of the require that the element’s address does not equal the read list, indicating that this entry should overwrite any other address (so that it is a proper subset of it). This ensures entries for this address. that the Boolean expressions for hard_match and The Read operation is shown in Figure 4 as a function soft_match will not be true simultaneously. For an imple- which, given a memory list and an address set expression, mentation of the Read operation that yields more precise returns a data set expression indicating the contents of this results, and for a way to optimize the Write operation, the location. It does so by scanning through the list from low- reader is referred to [19]. est to highest priority.
6
Comparing Symbolic Ternary Memory set expression g has already been overwritten in both the Execution Sequences primary and the shadow memory lists, it can be deleted In Correspondence Checking, we wish to test from both lists and reused.
whether two sequences of memory operations, which we When executing the sequence A, we would use mem- will refer to as “A” and “B,” yield identical behaviors. ory B as the shadow, and conversely when executing the That is, we assume the two sequences start with identical sequence B, we would use memory A as the shadow. Note initial memory states. For each Read operation in that the Write operations proceed as before. With this sequence A, its counterpart in sequence B must encounter shadowing, any time a symbolic variable is assigned to the same initial value. Furthermore, the final states result- represent the initial state of a memory location, the same ing from the two sequences must match. To implement symbol will be assigned to the same location and under the this, we require some mechanism for guaranteeing that same contexts in both memories, thus enforcing the consistent values are used for the initial contents of the assumption that the two memories have matching initial two memories. In addition, we require an algorithm for states. comparing the contents of two memories. 5.2 Comparing Final States in Symbolic Ternary 5.1 Maintaining Consistent Initial States Simulation If we were to execute the operations for the two When adopting the correctness criterion (1) of Burch sequences independently, we would generate different and Dill’s method to symbolic ternary simulation, we can symbols to represent the initial memory contents, and treat the final state Q′Spec, reached along the specification hence we would not yield matching results. Even if we side of the commutative diagram, as an overspecification could “reset” our symbol generator, so that the execution of the final state Q′′Spec, reached along the implementation sequence B used the same series of generated symbols as side of the diagram. In other words, the implementation sequence A, there would be a mismatch if the two will be correct if each of the state bits in Q′′Spec will be sequences access memory locations in a different order. equal to or not more general than its counterpart bit in Instead, we modify the Read operation to maintain a con- Q′Spec, i.e., the two bits must be related according to the sistent initial state between the memory being operated on, bit-level definition of the “⊆“-relation from (8). Hence, the and a “shadow” memory, as shown in Figure 5. correctness criterion when combining Burch and Dill’s method with ternary simulation can be expressed as: function ShadowRead(List mem, List shadow, ∀ Õx , Õ u , Õp . Abs(δI(Õx , 〈Õ ⊆ ASExpr a) : DSExpr δS(Õx , u , Õp 〉)) Abs(〈Õ /* Read from location a of memory mem / u , Õp 〉)) , (11) / Maintain consistency with shadow memory */ which is equivalently represented in Figure 6. ifg ← GenDataExpr(mem) F ¬Valid(¬Unique(a)) then QSpec Spec Q′Spec ⊇ Q′′Spec InsertHead(mem, 〈Unique(a), false, a, g〉) InsertHead(shadow, 〈Unique(a), false, a, g〉) return Read(mem, a) Abs Abs Figure 5. Implementation of the ShadowRead operation Function GenDataExpr() is used to produce a data set QImpl FImpl Q′ expression consisting of a fresh Boolean variable for every Impl bit position. This data set expression will be used as “ini- Figure 6. Commutative diagram for the correctness crite- tial” data for the contents of the given address under the rion when using symbolic ternary simulation contexts when the address is unique and it has not been In comparing the contents of two memories, we can initialized or written to before. In this way, we dynami- exploit the fact that only a small number of locations actu- cally introduce state for symbolic memory locations, as ally have defined values for any given context. Figure 7 needed by the circuit for a given simulation sequence. shows how a Boolean expression can be constructed indi- headInserting the element 〈Unique(a), false, a, g〉 into the cating the contexts for which two memories have corre- quent (low priority) end of both lists ensures that subse- sponding contents. This algorithm only checks the Read operations will encounter the same data set locations denoted by the address set expressions occurring expression for the “initial” state of location a as the one in the two lists, since all other addresses have not been used by the present Read. As an optimization, when data accessed and their initial contents, assumed to be identical,
7
have not been modified. A further optimization, that is not sequence B never reads or writes this address. Then the list shown, is to maintain a table of the address set expressions for A will contain an entry with address a, while the list that have been processed, so as to ensure that only one for B will not. Executing ShadowRead(memB, memA, a) comparison is performed for each distinct address set will return an expression involving a new data set expres- expression. sion generated by GenDataExpr(), which will not equal function CompareForContainment(List SpecMem, the expression returned by ShadowRead(memA, memB, a), List ImplMem) : BExpr and hence the mismatch will be detected. Notice that this /* Compare implementation memory for / situation will not result in an error when sequence A is / correspondence to specification memory */ produced by the specification circuit and the data that A correspondence ← true writes to address a is UD. for each 〈eh, es, ea, ed〉 in SpecMem do 6. Generating Memory State Spec_d ← ShadowRead(SpecMem, ImplMem, ea) Impl_d ← ShadowRead(ImplMem, SpecMem, ea) One drawback of OBDDs [4], used as a representa- correspondence ← correspondence ∧ tion of Boolean expressions in our implementation of the (Impl_d ⊆ Spec_d) presented algorithms, is that they require a global ordering for each 〈eh, es, ea, ed〉 in ImplMem do of the variables. This translates into a problem when gen- Spec_d ← ShadowRead(SpecMem, ImplMem, ea) erating the initial state of EMMs, due to the widely vary- Impl_d ← ShadowRead(ImplMem, SpecMem, ea) ing classes of instructions supported by modern correspondence ← correspondence ∧ instruction set architectures. (Impl_d ⊆ Spec_d) The problem stems from an implicit rule that the return correspondence address variables that will be used in an address set Figure 7. Comparing states of two memories in symbolic expression for accessing an EMM, need to be placed ternary simulation before the data variables that will represent the contents of that location. This requirement reduces the OBDD sizes, 5.3 Observation since the address variables will be used to select a set of data variables for the contents of the corresponding mem- One final subtlety about our comparison technique is ory location, when function Read() is invoked. The selec- worth noting. Normally two execution sequences will tion will be based on the comparison with other address yield matching final memory states only if they perform set expressions in the list for the EMM. If the address vari- identical Write operations, at least for the final writes to ables were intermixed with the data variables, or were situ- each memory location. Thus, if sequence A performs a ated after them in the global ordering of the variables, we write to some address a, one would expect sequence B to would expect an exponential complexity of the Boolean do likewise. Consider the case, however, where sequence expressions returned by function Read(), as opposed to a A first reads from the unique address a and then writes the linear complexity. This would be due to the need for the read value back to address a. Then location a is still in its data variables to be replicated in these expressions for initial state, and there is no need for sequence B to either every possible outcome of comparing the given address set read or write this location. Observe that our method will expression to the address set expressions in the list. correctly handle this case. In executing sequence A, we A similar rule is that control variables (e.g., opera- will add entries 〈Unique(a), false, a, g〉 to both lists. The tion-code, and functional-code variables) need to be Write operation in A may cause this entry to be replaced, placed before the data variables that they will affect. but since it preserves the initial state of this location, the Again, the control variables will select one out of many two memories will compare successfully. operations to be performed on the data variables, so that The condition described above is also the reason why the above argument still applies. the list for memory A must be used as a shadow argument In order to account for the above two rules, we intro- for the Read operations performed on memory B. Even duce the notion of ordered variable groups. Each variable though we have already evaluated the effect of all Read group contains interleaved vectors of symbolic Boolean and Write operations by sequence A, sequence B may variables that are used for the same purpose (e.g., access memory locations never accessed by A. This is addresses, control, data). Additional vectors from the same allowed as long as the accesses do not alter the values at group can be generated dynamically, as required by the these or any other memory locations. circuit for a given symbolic simulation sequence. The vari- On the other hand, suppose sequence A writes to able groups are ordered based on their relation, according address a without ever reading the initial state, while to the above two rules.
8
Op Rs Rt Rd 00000 Fn register-register instruction format
31 26 25 21 20 16 15 11 10 6 5 0
Op Rs Rt Imm register-immediate instruction format
31 26 25 21 20 16 15 0
00000000000000000000000000000000 NOP instruction format
31 0
Figure 8. The MIPS formats for register-register, register-immediate, and NOP instructions. The instructions are encoded with 32 bits, numbered 0 through 31 - see the digits below the rectagles. Op stands for the operation-code field of 6 bits, Fn represents the functional-code field of 6 bits, and Imm is the immediate field of 16 bits. Rs, Rt and Rd are 5-bit register identi- fiers. Rs and Rt are the source registers, while Rd is the destination register, for register-register instructions. Rs is a source register providing the second operand, and Rt is the destination register for register-immediate instructions
Therefore, the ideal global ordering of the variable ple data set expressions, each composed of variables from
groups, needed to verify the MIPS pipeline [15] for its reg- many variable groups and/or constants, which are indexed ister-register and register-immediate instructions [10] (see (selected) by the type of the instruction. The resulting data Figure 8), will be: instruction-addresses, operation-codes, set expression is generated according to a pattern, defined functional-codes, register-identifiers, high-data, and low- by the user, for the given EMM. Figure 9 illustrates how data (when listed from first to last in the global ordering of this pattern can be defined for the IMem of the MIPS, the variables). The need to split the data variables into two when the set of verified instructions consists of ori, or, groups is dictated by the format of the MIPS register- and nop. immediate instructions. Notice that the instruction-address gendataexpr IMem ( variables represent the contents of the program counter Op : OpCode (PC) and identify locations of the instruction memory Fn : FnCode (IMem), so that they need to be placed before the instruc- Rs, Rt, Rd : RegId tions (that will represent the contents of the IMem), i.e., Imm : LoData before all other variable groups. The justification for the switch <Op, Fn> ( ordering of the other variable groups is similar. case <0,0,1,1,0,1,-,-,-,-,-,->: /* ori / As Figure 8 shows, the lowest 6 bits of the MIPS return <0,0,1,1,0,1, Rs, Rt, Imm> instructions can represent the functional code in register- case <0,0,0,0,0,0,1,0,0,1,0,1>: / or / register instructions, or part of the immediate data in regis- return <0,0,0,0,0,0, Rs, Rt, Rd, ter-immediate instructions. Ideally, these 6 bits would be 0,0,0,0,0,1,0,0,1,0,1> encoded with functional-code variables for the register- default: / nop / register instructions, and data variables for the register- return <0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, immediate instructions. Furthermore, the functional-code ) 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0> variables need to be placed before the data variables (as condition <Op, Fn> = the functional code determines what operations are to be <0,0,1,1,0,1,-,-,-,-,-,-> || / ori / performed on the data by the ALU). Supplying a single <0,0,0,0,0,0,1,0,0,1,0,1> || / or / vector of symbolic Boolean variables for the initial state of <0,0,0,0,0,0,0,0,0,0,0,0> / nop */ the instruction memory at a particular address location ) (the way that function GenDataExpr() was defined to Figure 9. Definition of the variable-group indexing pattern work so far) will mean that a dynamic-variable-reordering for the MIPS instruction memory (IMem), when verifying OBDD package will need to find a different global vari- the pipeline for the instructions ori, or, and nop. “-” indicates able order, conditional on the type of the instruction, a don’t-care, so that the corresponding variable does not which will be impossible for a symbolic instruction repre- participate in the Boolean expression senting many instruction formats simultaneously. OpCode, FnCode, RegId, and LoData are the 6.1 Variable-Group Indexing declaration names for the operation-code, functional-code, Our solution is to introduce a state-encoding tech- register-identifier, and low-data variable groups, respec- nique that we call “variable-group indexing”. It allows the tively. Op, Fn, Rs, Rt, Rd, and Imm are vectors of fresh EMM to return a data set expression that consists of multi- Boolean variables generated within the corresponding
9
variable group by being interleaved with other such vec- procedure Write(List mem, CExpr c, ASExpr a, DSExpr d, tors in the same variable group. The switch statement BExpr global_care_set, Boolean verify_generality) uses the concatenation of the Op and Fn vectors of Bool- /* Write data d to location a under control c / ean variables in order to index one out of three possible h ← Hard(c) ∧ Unique(a) patterns for the initial state of the IMem, according to the s ← Soft(c) ∨ Hard(c) ∧ ¬Unique(a) case and default directives. The condition state- if (verify_generality) then ment defines a Boolean expression in terms of the fresh VerifyGenerality(mem, h, s, d, global_care_set) variables in Op and Fn, which is used to update a Boolean InsertTail(mem, 〈h, s, a, d〉) expression global_care_set (whose application will be Figure 10. illustrated shortly) by being conjuncted with the current Modified implementation of the Write opera- value of global_care_set every time when a new data set tion expression is generated for that memory. In this way, the Procedure VerifyGenerality(), shown in Figure 11, switch and condition statements allow the state of verifies its data set expression argument for being a subset the EMMs to be restricted to a subset of the system state (according to the “⊆“-relation from (8)) of the initial state space. This makes possible the verification of micropro- for the corresponding memory, as represented by a fresh cessors for a subset of their instruction set architectures. data set expression g, generated according to the variable- Hence, function GenDataExpr() is modified in order group indexing pattern for the memory. Function GetVari- to reflect the variable-group indexing pattern for an EMM, ableSupport() extracts the symbolic Boolean variables i.e., to return a Boolean expression instead of just a single used in its argument data set expression. For the new data Boolean variable for every bit position in the generated set expression d to be a subset of the initial state of the data set expression. memory, we require that for every binary pattern of the As Figure 9 shows, we might be imposing restrictions variables in the support of d, there exist a binary pattern of on the initial state that is generated on-the-fly by GenDa- the variables in the support of the newly generated default taExpr(), therefore considering a subset of the system state data set expression g that makes g be a superset of d, given space as a possible initial state. However, the correctness the implication by the Boolean expression criterion expressed by the commutative diagram from Fig- global_care_set, conjuncted with (h ∨ s). Notice that the ure 1 is a proof by induction. It proves that if the imple- universal quantification with respect to the variables in the mentation starts from an arbitrary initial state QImpl, and is support of d is done implicitly. Given that the result of the exercised with an arbitrary instruction, then the reachable existential quantification with respect to the variables of g state Q′Impl will be correct, when compared (by means of is not true, then a further universal quantification would an abstraction function) to the specification’s behavior for never make it true. The verification is aborted by calling an arbitrary instruction. Since the initial state QImpl is arbi- procedure Exit(), when the Boolean expression correct is trary, then it is a superset of the reachable state Q′Impl, so not true, i.e., when the data set expression d is not a subset that, by induction, the implementation will function cor- of the initial state for the memory. As an optimization, the rectly for an arbitrary instruction applied to Q′Impl. How- data set expression g, generated in the procedure, can be ever, if the initial state QImpl is restricted to a subset of the reused. system state space, and Q′Impl is not a subset of QImpl, procedure VerifyGenerality(List mem, BExpr h, BExpr s, then the inductive argument for the correctness criterion DSExpr d, BExpr global_care_set) would not hold. Hence, we need to check that Q′Impl is a / Compare new memory state d for satisfying the memory’s subset of QImpl. This is equivalent to proving an invariant variable-group indexing pattern */ of the implementation. Õg ← GenDataExpr(mem) 6.2 Verifying Memory State for Consistency with l ← GetVariableSupport(g) Its Variable-Group Indexing Pattern ifcorrect ← ∃ Õl . [global_care_set ∧ (h ∨ s) ⇒ (d ⊆ g)] ¬Valid(correct) then We therefore modify the Write operation in order to Exit() check, conditional on a new argument Boolean expression Figure 11. verify_generality, the set of reachable states for being a Verifying new state of a memory for being a subset of the initial state, as expressed by the variable- subset of the initial state of that memory, as represented by group indexing pattern for the corresponding memory - the memory’s variable-group indexing pattern see Figure 10. The type Boolean is used for flags that can Observe that procedure VerifyGenerality() need only be either true or false. be called for EMMs that get written to by the circuit and whose variable-group indexing patterns exclude some
10
IFD EX WB
IFD_EX EX_WB
Control
4
MUX
PC IMem RegFile Sign-Extend ReadReg1 MU Instr MU ReadData1 M X U X A Addr Nop ReadReg2 X L ReadData2 M U WriteReg UX WriteData Forwarding Control
Flush
Figure 12. The shortened pipelined MIPS (SPMIPS)
combinations. Hence, these are only the pipeline latches in This would be provided automatically by function the MIPS. ShadowRead(). 8. Compare the original, memi, and the shadow, shadowi, 7. Ternary Correspondence Checking by memory lists for every user-visible memory element i Applying Memory Shadowing and let containmenti ← When applying memory shadowing, the EMM soft- i = 1, ..., CompareForContainment(memi, shadowi) , u, where u is the number of user-visible ware interface uses function ShadowRead() for performing memory elements. reads, and procedure Write() for performing writes. Shad- 9. Form the Boolean expression for our correctness crite- owRead() provides the two execution sequences with iden- rion: u tical initial memory state by constructing it on-the-fly. We global_care_set ⇒ containmenti , (12) check the correctness criterion (11) by applying function where global_care_set i = 1 CompareForContainment() on all the user-visible memory taExpr() according to theis updated by function GenDa- elements. The universal quantification is done implicitly condition statements in by using the same symbolic initial memory state and the the declaration of variable-group indexing patterns for same symbolic instruction for both execution sequences. EMMs. The steps of our methodology are: It is also possible to traverse the commutative dia-
Load the implementation (possibly pipelined) circuit gram with another sequence of circuit and memory swaps, and associate every memory element in it with empty i.e., to exercise first the specification side of the diagram. original and shadow memory lists. global_care_set ← true. 8. Experimental Results
verify_generality ← true. Simulate the implementa- We implemented all the correspondence checking tion circuit for one clock cycle with a (legal) symbolic routines, presented in this paper, within a tool [9] that sup-
instruction. verify_generality ← false. ports the STE technique. Although correspondence check-
Simulate a flush of the implementation circuit. ing and STE are two different forms of verification, as Swap the original and shadow memory lists for every noted in Section 1, they have in common the use of a sym-
memory element. bolic simulator and the EMM. This allows them to be
Simulate a flush of the implementation circuit. applied on the same circuit descriptions, which can be in Swap the implementation and the specification (non- either gate-level or register-transfer-level form. Further- pipelined) circuits by keeping the contents of the more, gate-level circuits can be automatically generated
memory lists for every user-visible memory element. from transistor-level circuits [3]. Simulate the specification circuit for one clock cycle We examined the shortened pipelined MIPS with the same symbolic instruction as used in Step 2. (SPMIPS), shown in Figure 12. It was compared to its
11 CPU Time (s) Memory (MB) Instructions Verified Data Path Width Data Path Width o an ad sl su or an ad sl no 4 8 16 r d d t b i di di ti p 32 64 4 8 16 32 64 4 3 4 7 12 23 1.4 1.4 1.4 1.5 1.6 4 4 6 11 20 42 91 2.1 2.8 4.4 7.4 13.5 4 4 12 23 48 102 224 4.3 7.3 13.3 25.4 49.4 4 4 4 21 45 98 213 509 7.3 13.3 25.3 49.4 97.4 4 4 4 4 37 80 171 456 1 079 9.3 21.4 49.3 97.3 193.2 4 4 4 4 4 45 92 203 480 1 256 13.3 25.3 49.3 97.3 193.4 4 4 4 4 4 4 68 148 320 829 --- 17.1 34.0 57.3 145.6 --- 4 4 4 4 4 4 4 79 186 403 1 056 --- 13.3 40.3 87.8 150.1 --- 4 4 4 4 4 4 4 4 113 268 659 --- --- 25.3 49.3 113.2 --- --- 4 4 4 4 4 4 4 4 4 141 299 789 --- --- 29.3 49.3 133.8 --- --- 4 4 4 4 4 4 4 4 4 4 164 419 1 141 --- --- 41.3 97.1 193.2 --- ---Table 2. Experimental results from the correspondence checking between the SPMIPS and its non-pipelined version when verifying the instructions marked with “4“. In the cases indicated with “---”, the experiments did not finish because of limited/insufficient memory
non-pipelined version. The shaded boxes represent mem- implicitly shown as connecting the complement of Flush ory arrays and latches modeled by EMMs. The SPMIPS to the corresponding port enables). In this way, we did not
consists of three stages: a combined instruction fetch and read/write the PC and did not read the IMem and the Reg- decode stage (IFD), an execution stage (EX), and a write- File during flushing. This is allowed, since the method back stage (WB). The original MIPS is described in [15]. requires an arbitrary abstraction function that makes the Experiments for correspondence checking of the diagram for the correctness criterion commute. However, SPMIPS to its non-pipelined version were performed for the above flushing function reduces the CPU time and data path widths (i.e., the data width of the register file and memory requirements for the verification. Observe that the the ALU) between 4 and 64 bits. The instruction size was PC should be read and written during flushing if jump or always 32 bits, as in the original MIPS. Two MIPS instruc- brunch instructions are also being verified. tion formats were supported by the SPMIPS and its non- The experiments were performed on an IBM RS/ pipelined version - register-register and register-immedi- 6000 43P-140 with a 233MHz PowerPC 604e micropro- ate. Particularly, ten instructions were implemented in the cessor, having 512 MB of physical memory, and running control of both microprocessors: five register-register AIX 4.1.5. Table 2 shows the results from the correspon- instructions - or, and, add, slt, and sub; four register- dence checking between the SPMIPS and its non-pipe- immediate instructions - ori, andi, addi, and slti; lined version. Some of the experiments did not finish and the nop. The immediate operand in register-immedi- because of a system limitation that the C function mal- ate instructions was formed from the 16-bit immediate loc() cannot allocate more than 256 MB of memory for field of the instruction by taking as many bits as half the a single process, although the computer that we used had data path width, but not exceeding 16 (in the case of a 64- 512 MB of physical memory. bit wide data path), and sign-extending them by replicat- ing the most significant bit until filling the data width. 9. Conclusions and Future Work The multiplexor controlled by signal Flush is assumed to have been added to the circuit by the user in Based on our experiments, we can draw the following con- order to implement the flushing function. Furthermore, we clusions: modified the circuit by conjuncting the complement of sig- • Register-immediate instructions take less CPU time nal Flush with some EMM port enable signals (this is and memory to be verified than do register-register
12
instructions. We explain that with their simpler vari- Microprocessors by Comparing Memory Execution
able-group indexing patterns. Sequences in Symbolic Simulation,”2 Asian Computer Sci-
• The CPU time and memory approximately double as ence Conference (ASIAN ’97), R.K. Shyamasundar and K. Ueda, eds., LNCS 1345, Springer-Verlag, December 1997, the data path width doubles. pp. 18-31. • The CPU time and memory flatten as the set of veri- [6] J.R. Burch, and D.L. Dill, “Automated Verification of fied instructions is expanded. The reason is the simpli- Pipelined Microprocessor Control,” CAV ‘94, D.L. Dill, ed., LNCS 818, Springer-Verlag, June 1994, pp. 68-80. fication of the Boolean expressions when generating [7] J.R. Burch, “Techniques for Verifying Superscalar Micro- the initial state of the EMMs because of the availabil- processors,” DAC ‘96, June 1996, pp. 552-557. ity of more instructions with the same format, but [8] C.A.R. Hoare, “Proof of Correctness of Data Representa- slightly different operation-codes and/or functional- [9] tions,” Acta Informatica, 1972, Vol.1, pp. 271-281. codes. A. Jain, “Formal Hardware Verification by Symbolic Tra- jectory Evaluation,” Ph.D. thesis, Department of Electrical • An extra level of forwarding logic, due to a dummy and Computer Engineering, Carnegie Mellon University, pipeline stage between the EX and WB stages of the [10] August 1997. SPMIPS, increased the CPU time and memory from G. Kane, and J. Heinrich, MIPS RISC Architecture, Pren- tice Hall, Englewood Cliffs, NJ, 1992. two to more than ten times for the experiments that [11] K.L. McMillan, Symbolic Model Checking, Kluwer Aca- could finish (not shown). This can be attributed to the demic Publishers, 1993. greater complexity of the Boolean expressions for the [12] R.B. Jones, C.-J.H. Seger, and D.L. Dill, “Self-Consis- resulting ALU operands. tency Checking,” FMCAD ‘96, M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November 1996, pp. In the future, we will work on automating the process 159-171. of defining the variable-group indexing patterns for pipe- [13] M. Pandey, “Formal Verification of Memory Arrays,” line latches, in order to reduce the chance for an error on Ph.D. thesis, School of Computer Science, Carnegie Mel- the side of the user. We will also study the efficiency of [14] lon University, May 1997. M. Pandey, and R.E. Bryant, “Exploiting Symmetry When functions that simplify OBDDs based on a care-set Verifying Transistor-Level Circuits by Symbolic Trajec- OBDD. Furthermore, we will explore ways to deal with tory Evaluation,” CAV ‘97, O. Grumberg, ed., LNCS 1254, the verification complexity introduced by multiple levels [15] Springer-Verlag, June 1997, pp. 244-255. of forwarding logic. Finally, we will work on techniques to D.A. Patterson, and J.L. Hennessy, Computer Organiza- enable the verification of load, store, jump, and branch tion and Design: The Hardware/Software Interface, 2nd Edition, Morgan Kaufmann Publishers, San Francisco, instructions. Notice that the variable-group indexing pat- CA, 1998. terns of these instructions cannot satisfy the rule for plac- [16] J. Sawada, and W.A. Hunt, Jr., “Trace Table Based ing address variables before data variables in the global Approach for Pipelined Microprocessor Verification,” CAV variable ordering. The reason is that variables which will ‘97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June represent the data of a memory array in the variable-group [17] 1997, pp. 364-375. C.-J.H. Seger, and R.E. Bryant, “Formal Verification by indexing patterns of these instructions, will also be used as Symbolic Evaluation of Partially-Ordered Trajectories,” an address to that same memory array. For example, in the Formal Methods in System Design, Vol. 6, No. 2 (March case of the store instruction, the contents of a register will [18] 1995), pp. 147-190. serve both as data to be stored in the data memory and as a M.N. Velev, R.E. Bryant, and A. Jain, “Efficient Modeling destination address in the same memory. of Memory Arrays in Symbolic Simulation,”2 CAV ‘97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, References [19] pp. 388-399. M.N. Velev, and R.E. Bryant, “Efficient Modeling of [1] D.L. Beatty, R.E. Bryant, and C.-J.H. Seger, “Synchronous Memory Arrays in Symbolic Ternary Simulation,”2 First Circuit Verification by Symbolic Simulation: An Illustra- International Conference on Tools and Algorithms for the tion,” Sixth MIT Conference on Advanced Research in Construction and Analysis of Systems (TACAS ’98), Portu- VLSI, 1990, pp. 98-112. [20] gal, March-April 1998. [2] S. Bose, and A.L. Fisher, “Verifying Pipelined Hardware M.N. Velev, and R.E. Bryant, “Efficient Modeling of Using Symbolic Logic Simulation,” International Confer- Memory Arrays with Timing Requirements in Symbolic ence on Computer Design, October 1989, pp. 217-221. Ternary Simulation,”2 International Workshop on Timing [3] R.E. Bryant, “Extraction of Gate Level Models from Tran- Issues in the Specification and Synthesis of Digital Systems sistor Circuits by Four-Valued Symbolic Analysis,” Inter- [21] (TAU ‘97), Austin, TX, December 1997, pp. 28-38. national Conference on Computer Aided Design, P.J. Windley, and J.R. Burch, “Mechanically Checking a November 1991, pp. 350-353. Lemma Used in an Automatic Verification Tool,” FMCAD [4] R.E. Bryant, “Symbolic Boolean Manipulation with ‘96, M. Srivas and A. Camilleri, eds., LNCS 1166, Ordered Binary-Decision Diagrams,” ACM Computing Springer-Verlag, November 1996, pp. 362-376. Serveys, Vol. 24, No. 3 (September 1992), pp. 293-318. 2. Available from: http://www.ece.cmu.edu/afs/ [5] R.E. Bryant, and M.N. Velev, “Verification of Pipelined ece/usr/mvelev/.home-page.html
13