A Methodology for Validation of Microprocessors using
                                                               Equivalence Checking

                 Prabhat Mishra                                     Nikil Dutt
                 pmishra@cecs.uci.edu                           dutt@cecs.uci.edu

                 Architectures and Compilers for Embedded Systems (ACES) Laboratory
                            Center for Embedded Computer Systems, University of California, Irvine, CA 92697, USA
                                                          http://www.cecs.uci.edu/˜aces

                 Abstract                                     validation technique is complementary to these bottom-

As embedded systems continue to face increasingly up approaches. Our approach leverages the system archi- higher performance requirements, deeply pipelined proces- tect’s knowledge about the behavior of the pipelined archi- sor architectures are being employed to meet desired system tecture, through Architecture Description Language (ADL) performance. Validation of such processor architectures is constructs, and thus allows a powerful top-down approach one of the most complex and expensive tasks in the current to architecture validation. Systems-on-Chip design process. A significant bottleneck in Figure 1 shows a traditional language-driven design the validation of such systems is the lack of a golden refer- space exploration flow. Given a set of application programs, ence model. This paper presents an Architecture Descrip- the goal is to find out the best possible architecture in a tion Language (ADL) driven methodology for generating reasonable amount of time. The programmable embedded golden reference model. We use EXPRESSION ADL to cap- system (processor, coprocessor, and memory subsystem) is ture the structure and behavior of the processor. The synthe- captured using an ADL. The ADL specification of the ar- sizable Register Transfer Language (RTL) description of the chitecture is used to generate a software toolkit (including architecture is generated from the ADL specification. The compiler, simulator, and assembler), and provide feedback generated RTL description is used as a golden reference to the designer on the quality of the architecture. model for verifying the correctness of the implementation using equivalence checking. We applied our methodology Architecture Specification ( English Document ) on a RISC DLX architecture to demonstrate the usefulness T i of our approach. Automatic Manual ADL Description Feedback 1 Introduction Validation Validation of programmable embedded systems is one Compiler Simulator of the most complex and expensive tasks in the current Application Generator Generator | Programs Systems-on-Chip design process. Traditionally, architects ASM BIN prepare an informal specification of the microprocessor in Compiler Assembler Simulator the form of an English document. The logic designers Figure 1. Language driven Design Space Exploration implement the processor using Hardware Description Lan- guage (HDL). The validation engineers verifies the im- An extensive body of recent work addresses ADL driven plementation using combination of simulation techniques software toolkit generation and design space exploration and formal methods. A significant bottleneck in the val- for processor-based embedded systems, in both academia: idation of such systems is the lack of a golden reference ISDL [11], Valen-C [1], MIMOLA [19], LISA [39], EX- model. Thus, many existing techniques ([14], [24]) em- PRESSION [12], nML [10], and industry: ARC [4], Axys ploy a bottom-up approach to processor validation, where [5], RADL [31], Target [36], Tensilica [37], MDES [38]. the functionality of an existing pipelined architecture is, in This paper presents an ADL driven methodology for ver- essence, reverse-engineered from its implementation. Our ifying the correctness of the implementation using equiva-

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions (MTV’03) COMPUTER 0-7695-2045-6/03 $ 17.00 © 2003 IEEE SOCIETY

                                                                             Feedback (Performance, Code Size)

lence checking. The architecture is captured in EXPRES- based techniques. This becomes impractical for design with SION ADL [12]. The synthesizable HDL is generated from many unmatched points. the ADL specification. The generated HDL description is used as a golden reference model during equivalence check- IN1 | ing. We applied our methodology on a RISC DLX architec- IN2 Cone1 OUT1 Automatically ture to demonstrate the usefulness of our approach. IN3 .

    matched cones

    . 2

The rest of the paper is organized as follows. Sec- IN4 . Cone2 . OUT IN5 . . tion 2 briefly describes the equivalence checking technique. . matched cones Section 3 presents related work addressing validation of . Conen OUTn [>> User specified pipelined processors. Section 4 presents our ADL-driven INm | [>> Unmatched cones equivalence checking framework followed by a case study a) Logic Cones in a Design Block in Section 5. Finally, Section 6 concludes the paper. Reference Design Implementation Design

2 Equivalence Checking

   >

Equivalence Checking is a branch of static verification =>

   > >

that employs formal techniques to prove that two versions

of a design either are, or are not, functionally equivalent.

This technique is primarily used to verify that a hardware

implementation modified due to design transformations is b) Compare Point Matching functionally equivalent to the original implementation. The Figure 2. Matching of Compare Points between Designs original design is assumed to be correct and known as the reference (golden) design. The modified design that needs During the verification stage, each matched compare to be verified against the reference design, is known as the point is proven either functionally equivalent or non- implementation. The equivalence checking flow consists of equivalent ([9], [21]). Design transformations can impact four stages: read, match, verification and debug. The match the structure of a logic cone within the implementation de- and verification stages are those most impacted by design sign. When logic cones are very dissimilar, performance transformations [40]. suffers. In some cases, such as during retiming, the logic During the read stage, both versions of the design are cones can change so significantly that additional setup is re- read by the equivalence checking tool and segmented into quired to successfully verify the designs. manageable sections called logic cones. Logic cones are The debug phase begins when the tool has returned a non- groups of logic bordered by registers, ports, or black boxes. equivalent result. Design transformations that have not been Figure 2(a) shows the cones for a typical design block. The accounted for can lead to a false negative result, and valu- output border of a logic cone is referred to as the compare able time could be spent debugging designs that are, in real- point. For example, OUT1 is the compare point in Cone1 of ity, equivalent. The solution would be to perform additional Figure 2(a). setup so that the tool is guided for the given designs. In match phase, the tool attempts to match, or map, com- pare points from the reference (golden) design to their cor- 3 Related Work responding compare point within the implementation de- sign [3]. Two types of matching techniques are used: non- function (name-based) and function-based (signature anal- Several approaches for formal or semi-formal verifica- ysis). Figure 2(b) shows compare point matching for a typi- tion of processors have been developed in the past. The- cal reference design and implementation. For better perfor- orem proving techniques, for example, have been success- mance, the majority of the matching should be completed fully adapted to verify pipelined processors ([8], [29], [30], by more efficient name-based methods. Design transfor- [33]). However, these approaches require a great deal of mations can result in fewer cones being matched by the user intervention, especially for verifying control intensive name-based techniques, slowing match performance. Creat- designs. Hosabettu [15] proposed an approach to decom- ing compare rules assist name-based techniques, but deter- pose and incrementally build the proof of correctness of mination and creation of the rules themselves can be time pipelined microprocessors by constructing the abstraction consuming. If the implementation is drastically different function using completion functions. than the reference design, design rules cannot be written Burch and Dill presented a technique for formally veri- and compare points will have to be manually matched for fying pipelined processor control circuitry [6]. Their tech- better performance or matched using more costly function- nique verifies the correctness of the implementation model

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions (MTV’03) COMPUTER 0-7695-2045-6/03 $ 17.00 © 2003 IEEE SOCIETY

of a pipelined processor against its Instruction-Set Architec- the architecture is generated from the ADL specification. ture (ISA) model based on quantifier-free logic of equality The hardware model is used as a golden reference model to with uninterpreted functions. The technique has been ex- verify the hand-written RTL Design. We use Formality [34] tended to handle more complex pipelined architectures by to check the equivalence between the hand-written RTL De- several researchers [32, 41, 42]. The approach of Velev and sign and the generated hardware model. Bryant [41] focuses on efficiently checking the commuta- tive condition for complex microarchitectures by reducing Architecture Specification the problem to checking equivalence of two terms in a logic ( English Document ) ....._ ! with equality, and uninterpreted function symbols. ! HERE i Huggins and Campenhout verified the ARM2 pipelined i ADL Specification ! processor using Abstract State Machine [16]. In [20], Levitt ! and Olukotun presented a verification technique, called un- i h pipelining, which repeatedly merges last two pipeline stages ! & Success Verify into one single stage, resulting in a sequential version of the processor. A framework for microprocessor correctness i! K Generic statements about safety that is independent of implementa- ! i Models tion representation and verification approach is presented in i J) [2]. Ho et al. [24] extract controlled token nets from a |i / HDL Generator logic design to perform efficient model checking. Jacobi ! I [17] used a methodology to verify out-of-order pipelines i y by combining model checking for the verification of the i RTL Hardware pipeline control, and theorem proving for the verification of i Design Model the pipeline functionality. Compositional model checking ! is used to verify a processor microarchitecture containing i Automatic most of the features of a modern microprocessor [18]. __ Different Equivalence Manual The existing techniques attempt to formally verify the im- Checker Feedback plementation of processors by comparing the pipelined im- Equivalent plementation with its sequential (ISA) specification model, or by deriving the sequential model from the implementa- Figure 3. ADL driven Validation Framework tion. Our validation technique is complementary to these First, we briefly describe the EXPRESSION ADL fol- approaches. We generate synthesizable RTL from the ADL lowed by a description of the ADL-driven synthesizable specification and use it as a golden reference model for ver- HDL generation technique. Finally, we present a case study ifying the correctness of the implementation using equiva- to validate DLX architecture using the generated reference lence checking. model. The industrial strength equivalence checkers (Formality [34], FormalPro [22], eCheck [28], Affirma [7], Conformal 4.1 The EXPRESSION ADL [43]) are traditionally used to check equivalence between RTL and gate level designs. It assumes that the original The EXPRESSION ADL allows automatic software RTL design is golden and verifies the modified design (e.g., toolkit generation and design space exploration of a wide modified RTL or gate level design). Our technique is com- range (DSP, VLIW, EPIC, Superscalar) of processors and plementary to this methodology. Our technique ensures that memory subsystems. We briefly describe the key aspects the original RTL design is golden. of the ADL in this section. The complete reference of the 4 ADL-driven Validation Framework language is provided in [12]. The EXPRESSION ADL captures the structure, behav- ior, and mapping (between structure and behavior) of the Figure 3 shows our ADL driven validation framework. programmable architecture as shown in Figure 4. System architects develop the architecture specification The structure of a processor can be viewed as a graph document. Logic designers implement the modules to gen- with the components as nodes and the connectivity as the erate RTL Design. The first step is to specify the architec- edges of the graph. It considers four types of compo- ture in EXPRESSION ADL [12]. It is necessary to validate nents: units (e.g., ALUs), storages (e.g., register files), the ADL specification to ensure that the architecture is well- ports, and connections (e.g., buses). There are two types of formed ([23], [26]). The synthesizable hardware model of edges: pipeline edges and data transfer edges. The pipeline

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions (MTV’03) COMPUTER 0-7695-2045-6/03 $ 17.00 © 2003 IEEE SOCIETY

Failed

edges specify instruction transfer between units via pipeline ADL. The decoder extracts information regarding opcode, latches, whereas the data transfer edges specify data trans- operands etc. from input instruction using the instruction fer between components, typically between units and stor- format. The mapping section of the ADL captures the infor- ages or between two storages. Each component has a list of mation regarding the mapping of opcodes to the functional attributes. For example, a functional unit has information units. The decoder uses this information to perform/initiate regarding latches, ports, connections, opcodes, timing and necessary functions (e.g., operand read) and decide where capacity. (pipeline latch) to send the instruction.

          EXPRESSION                                          Data Path
 Behavior Specification      Structure Specification                    The implementation of datapath consists of two parts.
                                                              First, compose each component in the structure.         Second,
 Operations Specification     Architecture Components         instantiate components (e.g., fetch, decode, ALU, LdSt,
                                                              writeback, branch, caches, register files, memories etc.) and
 Instruction Specification  Pipeline/Data-transfer Paths      establish connectivity using appropriate number of pipeline
     Operation Mappings           Memory Subsystem            latches, ports, and connections using the structural informa-
                                                              tion available in the ADL. To compose each component in
 Figure 4. The EXPRESSION ADL                                 the structure we use the information available in the ADL
                                                              regarding the functionality of the component and its pa-
 The behavior is organized into operation groups, with        rameters. For example, to compose an execution unit, it is

each group containing a set of operations having some com- necessary to instantiate all the opcode functionalities (e.g, mon characteristics. Each operation is then described in ADD, SUB etc. for an ALU) supported by that execution terms of it’s opcode, operands, behavior, and instruction for- unit. Also, if the execution unit is supposed to read the mat. operands then appropriate number of operand read function- The mapping functions map components in the structure alities need to be instantiated unless the same read function- to operations in the behavior. It defines, for each functional ality can be shared using multiplexors. Similarly, if this ex- unit, the set of operations supported by that unit (and vice ecution unit is supposed to write the data back to register versa). For example, the operation add is mapped to ALU file, the functionality for writing the result needs to be in- unit. stantiated. The actual implementation of an execution unit might contain many more functionalities e.g., read latch, 4.2 Synthesizable HDL Generation write latch, and insert/delete/modify reservation station (if applicable). The functional abstraction technique was first introduced by Mishra et al. [25] for generating simulation models for a Control Logic wide variety of architectures. In this paper we have used the functional abstraction technique to automatically generate The controller is implemented in two parts. First, it synthesizable VHDL models from the ADL specification. generates a centralized controller (using generic controller In fact, there is a direct relationship between generating a function with appropriate parameters) that maintains the simulator and a hardware model: the synthesizable VHDL information regarding each functional unit, such as busy, model is itself a simulator. stalled etc. It also computes hazard information based on The generated HDL description consists of three ma- the list of instructions currently in the pipeline. Based jor parts: instruction decoder, data-path, and control logic. on these bits and the information available in the ADL it We have implemented all the generic functions and sub- stalls/flushes necessary units in the pipeline. Second, a lo- functions using VHDL. In this section we briefly describe cal controller is maintained at each functional unit in the how to generate three major components using the generic pipeline. This local controller generates certain control sig- VHDL models. The detailed description is available in [27]. nals and sets necessary bits based on input instruction. For example, the local controller in an execution unit will acti- Instruction Decoder vate the add operation if the opcode is add, or it will set the busy bit in case of a multi-cycle operation. We have implemented a generic instruction decoder that 5 A Case Study uses information regarding individual instruction format and opcode mapping for each functional unit to decode a given instruction. The instruction format information In a case study we successfully applied the proposed is available in operations section of the EXPRESSION methodology on the DLX [13] processor. We have chosen

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions (MTV’03) COMPUTER 0-7695-2045-6/03 $ 17.00 © 2003 IEEE SOCIETY

DLX processor since it has been well studied in academia, Our future work will focus on improving this methodology and there are HDL implementations available that can be for verifying designs without prior knowledge of the imple- used in our validation framework. We have used the synthe- mentation style. sizable 32-bit RISC DLX implementation from University of Stuttgart [35]. 7 The EXPRESSION ADL captures the structure and be- Acknowledgments havior of the DLX architecture. The ADL specification is validated to ensure that the architecture is well-formed This work was partially supported by NSF grants CCR- ([23], [26]). Synthesizable HDL models are generated from 0203813 and CCR-0205712. We would like to acknowl- this specification. The generated HDL description is used edge the members of the ACES laboratory for their inputs. as a reference model. The RISC DLX from University of Stuttgart [35] is used as an implementation. We have used References Synopsys Formality equivalence checker [34] to verify the implementation against the generated golden RTL. [1] A. Inoue et al. A Programming Language for Processor Based The basic idea is simple. Irrespective of the implementa- Embedded Systems. In Proc. of Asia Pacific Conference on tion style, the equivalence checker will be able to verify the Hardware Description Languages (APCHDL), pages 89–94, design based on the correct behavior in the reference model. 1998. For example, our HDL generation framework generates 32- [2] M. Aagaard, B. Cook, N. Day, and R. Jones. A Framework for bit adder module that uses carry-look-ahead principle. The Microprocessor Correctness Statements. In T. Margaria and equivalence checker [34] will return success for the correct T. Melham, editor, Correct Hardware Design and Verification 32-bit adder implementation that uses ripple-carry adder Methods (CHARME), volume 2144 of LNCS, pages 433–448. principle. The equivalence checking process took four sec- Springer-Verlag, 2001. onds for this adder example on a 296 MHz Sun Ultra-250 [3] D. Anastasakis, R. Damiano, H. Ma, and T. Stanion. A Prac- with 1024M RAM. tical and Efficient Method for Compare-Point Matching. In Similarly, we generated structural model of a 32x32 Proc. of Design Automation Conference (DAC), pages 305– register-file and used it as a reference model to verify the 310, 2002. behavioral register-file implementation of the RISC DLX [4] ARC. http://www.arccores.com. ARC Cores. [35]. The equivalence checking process took 432 seconds [5] Axys. Axys Design Automation. http://www.axysdesign.com. for this example on a 296 MHz Sun Ultra-250 with 1024M RAM. The majority of this time (347 seconds) is spent in [6] J. Burch and D. Dill. Automatic verification of pipelined mi- the elaboration (linking) phase of the behavioral implemen- croprocessor control. In Computer Aided Verification (CAV), tation. 1994. Our framework generated synthesizable RTL for 32-bit [7] Cadence Affirma. http://www.cadence.com. RISC DLX that supports signed operations. We guided [8] D. Cyrluk. Microprocessor Verification in PVS: A Methodol- the RTL generation process to have similar structure as in ogy and Simple Example. Technical report, SRI-CSL-93-12, the implementation [35]. The equivalence checking process 1993. took 397 seconds on a 296 MHz Sun Ultra-250 with 1024M [9] C. Ejik. Sequential Equivalence Checking without State Space RAM. Traversal. In Proc. of Design Automation and Test in Europe (DATE), pages 618–623, 1998. 6 Summary [10] M. Freericks. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Dept., We have presented an architecture description language 1993. driven validation framework for microprocessors. The EX- [11] G. Hadjiyiannis et al. ISDL: An Instruction Set Description PRESSION ADL captures the structure and the behavior of Language for Retargetability. In Proc. of Design Automation the architecture. The synthesizable HDL description is gen- Conference (DAC), pages 299–302, 1997. erated from the ADL specification using the functional ab- [12] A. Halambi, P. Grun, V. Ganesh, A. Khare, N. Dutt, and straction technique. The generated HDL description is used A. Nicolau. EXPRESSION: A Language for Architecture as a golden reference model to verify the correctness of the Exploration through Compiler/Simulator Retargetability. In implementation using equivalence checking. We applied Proc. of Design Automation and Test in Europe (DATE), pages our methodology on a RISC DLX architecture to demon- 485–490, 1999. strate the usefulness of our approach. [13] J. Hennessy and D. Patterson. Computer Architecture: A Currently, we are able to verify designs where the ref- Quantitative Approach. Morgan Kaufmann Publishers Inc, erence model has similar structure as the implementation. San Mateo, CA, 1990.

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions (MTV’03) COMPUTER 0-7695-2045-6/03 $ 17.00 © 2003 IEEE SOCIETY

[14] R. Ho, C. Yang, M. A. Horowitz, and D. Dill. Architecture   [27] P. Mishra et al. Rapid Exploration of Pipelined Processors

Validation for Processors. In Proc. of International Sympo- through Automatic Generation of Synthesizable RTL Models. sium on Computer Architecture (ISCA), 1995. In Proc. of Rapid System Prototyping (RSP), pages 226–232, [15] R. M. Hosabettu. Systematic Verification Of Pipelined Mi- 2003. croprocessors. PhD thesis, PhD Thesis, Department of Com- [28] Prover eCheck. http://www.prover.com. puter Science, University of Utah, 2000. [29] J. Sawada and W. D. Hunt. Processor Verification with Pre- [16] J. Huggins and D. Campenhout. Specification and veri- cise Exceptions and Speculative Execution. In A. Hu and fication of pipelining in the ARM2 RISC microprocessor. M. Vardi, editor, Computer Aided Verification (CAV), volume 3(4):563–580, October 1998. 1427 of LNCS, pages 135–146. Springer-Verlag, 1998. [17] C. Jacobi. Formal Verification of Complex Out-of-Order [30] J. Sawada and J. W.A. Hunt. Trace Table based Approach Pipelines by Combining Model-Checking and Theorem- for Pipelined Microprocessor Verification. In O. Grumberg, Proving. In E. Brinksma and K. Larsen, editor, Computer editor, Computer Aided Verification (CAV), volume 1254 of Aided Verification (CAV), volume 2404 of LNCS, pages 309– LNCS, pages 364–375. Springer-Verlag, 1997. 323. Springer-Verlag, 2002. [31] C. Siska. A Processor Description Language Supporting Re- [18] R. Jhala and K. L. McMillan. Microarchitecture Verification targetable Multi-pipeline DSP Program Development Tools. by Compositional Model Checking. In G. Berry et al., editor, In Proc. of International Symposium on System Synthesis Computer Aided Verification (CAV), volume 2102 of LNCS, (ISSS), pages 31–36, 1998. pages 396–410. Springer-Verlag, 2001. [32] J. Skakkebaek, R. Jones, and D. Dill. Formal verification of [19] R. Leupers and P. Marwedel. Retargetable Code Generation out-of-order execution using incremental flushing. In Com- based on Structural Processor Descriptions. Design Automa- puter Aided Verification (CAV), 1998. tion for Embedded Systems, 3(1), 1998. [33] M. Srivas and M. Bickford. Formal Verification of a [20] J. Levitt and K. Olukotun. Verifying correct pipeline imple- Pipelined Microprocessor. In IEEE Software, volume 7(5), mentation for microprocessors. In Proc. of International Con- pages 52–64, 1990. ference on Computer-Aided Design (ICCAD), pages 162–169, [34] Synopsys Formality. http://www.synopsys.com. 1997. [35] Synthesizable DLX: Generic 32-bit RISC Processor. [21] J. Marques-Silva and T. Glass. Combinational Equivalence http://www.eda.org/rassp/vhdl/models/processor.html. Checking using Satisfiability and Recursive Learning. In Proc. of Design Automation and Test in Europe (DATE), pages 145– [36] Target. http://www.retarget.com. Target Compiler Technolo- 149, 1999. gies. [22] Mentor FormalPro. http://www.mentor.com. [37] Tensilica. http://www.tensilica.com. Tensilica Inc. [23] P. Mishra, H. Tomiyama, N. Dutt, and A. Nicolau. Auto- [38] Trimaran. The MDES User Manual. Trimaran Release: matic Verification of In-Order Execution in Microprocessors http://www.trimaran.org, 1997. with Fragmented Pipelines and Multicycle Functional Units. [39] V. Zivojnovic et al. LISA - Machine Description Language In Proc. of Design Automation and Test in Europe (DATE), and Generic Machine Model for HW/SW Co-Design. In IEEE 2002. Workshop on VLSI Signal Processing, 1996. [24] P. Ho et al. Formal Verification of Pipeline Control Using [40] R. Vallelunga and O. Eralp. Interoperable Tools Ease Equiv- Controlled Token Nets and Abstract Interpretation. In Proc. alence Checking. EE Times, Feb 3, 2003. of International Conference on Computer-Aided Design (IC- [41] M. Velev and R. Bryant. Formal verification of superscalar CAD), 1998. microprocessors with multicycle functional units, exceptions, [25] P. Mishra et al. Functional Abstraction driven Design Space and branch prediction. In Proc. of Design Automation Confer- Exploration of Heterogeneous Programmable Architectures. ence (DAC), pages 112–117, 2000. In Proc. of International Symposium on System Synthesis [42] M. N. Velev. Formal Verification of VLIW Microprocessors (ISSS), 2001. with Speculative Execution. In Computer Aided Verification [26] P. Mishra et al. Automatic Modeling and Validation of (CAV), 2000. Pipeline Specifications driven by an Architecture Description [43] Verplex Conformal. http://www.verplex.com. Language. In Proc. of Asia South Pacific Design Automation Conference (ASPDAC) / International Conference on VLSI Design, 2002.

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions (MTV’03) COMPUTER 0-7695-2045-6/03 $ 17.00 © 2003 IEEE SOCIETY