Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

Heon-Mo Koo     Prabhat Mishra                                            Jayanta Bhadra                Magdy Abadir

Computer and Information Science and Engineering Freescale Semiconductor Inc. University of Florida, Gainesville, FL 32611, USA. 7700 West Parmer Lane Austin, TX 78727, USA {hkoo, prabhat}@cise.ufl.edu {Jayanta.Bhadra, M.Abadir}@freescale.com

Abstract                                                                  generate an architectural test program for micro-architectural
    Simulation-based validation of the current industrial proces-         design bugs such as a pipeline interaction error (e.g., “decode

sors typically use huge number of test programs generated at stage is not stalled even if Completion Queue is full”), or a instruction set architecture (ISA) level. However, architectural performance error (e.g., “data dependency is not resolved by test generation techniques have limitations in terms of exer- forwarding path even if operand is available”). Therefore, it is cising intricate micro-architectural artifacts. Therefore, it is necessary to use micro-architectural details during test genera- necessary to use micro-architectural details during test gener- tion.Compared to the random or biased-random tests, the directed ation. Furthermore, there is a lack of automated techniques for tests can reduce overall validation effort since shorter tests can directed test generation targeting micro-architectural faults. To obtain the same coverage goal. However, there is a lack of au- address these challenges, we present a directed test generation tomated techniques for directed test generation targeting micro- technique at micro-architectural level for functional validation architectural faults. As a result, directed tests are hand-written of microprocessors. A processor model is described in a tem- by experts. Due to manual development this process can be poral specification language at micro-architecture level. The error prone. desired behaviors of micro-architecture mechanisms are ex- pressed as temporal logic properties. We use decompositional Architectural model checking for systematic test generation. Our experiments Architectural Specification using a processor based on the Power ArchitectureT M Technol- Specification ogy1 shows very promising results in terms of test generation Properties time as well as test program length. Processor Model Properties Processor Model Processor Model Properties

                                                                               Model                      Property

1 Introduction Model Property Decomposition Decomposition Decomposition Decomposition

           Performance improvement of modern processors is accom-

panied with high design complexity by adopting complicated Test Test Generation micro-architectural mechanisms such as deeply pipelined su- Generation perscalar, dynamic scheduling, and dynamic speculation. Since Test cases verification complexity is directly proportional to the design Test cases complexity, considerable amount of time and resources are Figure 1. Test Program Generation Methodology spent on design verification. In the current industrial practice [11], random and biased- To address these challenges, we present a directed test gen- random test generation techniques at architecture (ISA) level eration technique at micro-architectural level for functional are most widely used for simulation-based validation to un- validation of microprocessors. Figure 1 shows our directed cover errors early in the design cycle as well as to perform sim- test generation methodology. The input specification contains ulation for the entire processor design. However, as demon- both the structure (micro-architectural details) and the behav- strated in Section 4, architectural test generation techniques ior (instruction-set) of the processor. The micro-architectural have difficulty in activating micro-architectural target artifacts features in the processor model include pipelined and clock- and pipeline functionalities since it is not possible to gener- accurate behaviors that enable micro-architectural test genera- ate information regarding pipeline interactions or timing details tion. Properties can be automatically generated from the input using input ISA specification. For example, it is very hard to specification based on a functional fault model such as pipeline 1The Power Architecture and Power.org wordmarks and the Power and (graph) coverage [9]. Additional properties can be added based Power.org logos and related marks are trademarks and service marks licensed on interesting scenarios such as combined pipeline stage rules by Power.org and corner cases. These properties are described in temporal

Seventh International Workshop on Microprocessor Test and Verification (MTV'06) 0-7695-2839-2/06 $20.00 © 2006

logic. For automatic test generation, we use decompositional when applying to the industrial processors due to high com- model checking where the processor model as well as the prop- plexity of even single pipeline path. In addition, they mainly erties are decomposed and the model checking is applied on focus on the data path rather than the control path. While a smaller partitions of the design using decomposed properties. data (opcode and operands) is located in a single pipeline stage, We introduce the notion of time steps to enable decomposi- control signals (functional unit status and buffer status) may tion of the properties into smaller ones based on their clock spread across multiple pipeline stages and buffers which make cycles. We have developed an efficient algorithm to merge the model partitioning and counterexample merging more difficult. partial counterexamples generated by the decomposed proper- Therefore, it is necessary to improve the decomposition and ties to produce the global counterexample corresponding to the merging algorithms for application to the complex industrial original property. We applied this methodology on a processor processors. based on the Power Architecture Technology to demonstrate the usefulness of our approach. 3 The main contribution of this work is to establish a frame- Directed Micro-architectural Test Generation work for a directed and automated micro-architectural test gen- Today’s test generation techniques and verification methods eration technique for validation of modern industrial proces- are very efficient to find bugs at the unit level. Hard-to-find sors. Since the proposed method is generic, its framework can bugs arise often from the interactions among many pipeline be used for validation of any other real processors. The rest stages and buffers of a modern processor design. We primarily of the paper is organized as follows. Section 2 presents re- focus on such micro-architectural interface among functional lated work addressing test generation in the context of micro- units in a pipelined processor. architectural validation of pipelined processors. Section 3 de- scribes our test generation methodology. Section 4 presents a Algorithm 1: Test Generation case study and Section 5 concludes the paper. Inputs: i) Processor model M ii) Set of interactions S from fault model and corner cases 2 Related Work Outputs: Test programs Begin Several methodologies have been developed for validation TestPrograms = φ of pipelined processors using finite state machine (FSM) mod- for each interaction Si in the set S els [1, 5, 6, 10] where FSM coverage is used to generate test Pi = CreateProperty(Si) programs. In modern processor designs, complicated micro- Pi = Negate(Pi) architectural mechanisms include interactions among many testi = DecompositionalMC(M, Pi) pipeline stages and buffers that lead the FSM-based approaches endforTestPrograms = TestPrograms ∪ testi to the state-space explosion problem. To alleviate the state ex- return TestPrograms plosion, Utamaphethai et al. [12] have presented a FSM model End partitioning technique based on micro-architectural pipeline storage buffers whose entries store data and status. However, Algorithm 1 describes our test generation procedure. This al- it suffers from targeting complete micro-architectural features gorithm takes the processor model M and desired pipeline inter- because test programs are generated by design errors from each actions S as inputs and generates test programs. The processor buffer, not for combined buffers. model is described in a temporal specification language such as An alternative formal method, model checking [2], has been SMV [13]. For each interaction Si, the algorithm produces one successfully used in software and hardware validation as a test test program testi. Si is composed of a set of instruction and generation engine [3, 9]. The negated version of a desired prop- control functionalities at pipeline units and their relations and erty along with the processor model is applied to the model it is converted to a temporal logic property Pi. The negation of checker. The model checker automatically produce a coun- Pi is an interaction fault. The processor model M and the fault terexample that contains a sequence of instructions (a test pro- Pi are applied to decompositional model checking framework gram) from an initial state to a failure state. However, this naive to generate a test program. The algorithm iterates over all the approach is unsuitable for a real processor model due to the interaction faults in the fault model and corner cases. state explosion problem during model checking. Koo and Mishra [7, 8] have proposed a processor/property 3.1 Micro-architectural Modeling decomposition technique to reduce the search space during counterexample generation as well as an algorithm for merging Figure 2 shows a functional block diagram of the four-wide the partial counterexamples to generate architectural test pro- superscalar e500 processor that is based on the Power Architec- grams. Their test generation technique is built on a relatively ture Technology [14] with the seven pipeline stages. Pipeline simple MIPS processor [4] with no renaming buffer, reorder- buffers are highlighted in grey. We have developed a processor ing buffer, or reservation station. They use pipeline path-level model based on the micro-architectural structure, the instruc- model partitioning to generate a test program for data forward- tion behavior, and the rules in each pipeline stage that deter- ing, but it causes deprivation of memory during model checking mine when instructions can move to the next stage and when

Seventh International Workshop on Microprocessor Test and Verification (MTV’06) 0-7695-2839-2/06 $20.00 © 2006

      I-cache
      I-cache                                     7 pipeline stages
        Fetch stage 1                            7 pipeline stages   of the properties can be expressed as:
        Fetch stage 1                             Superscalar
                                                 Superscalar
    IQ                                            Dynamic scheduling
    IQ  Fetch stage 2
        Fetch stage 2                    Rename
                                         Rename   Dynamic scheduling
                                      Buffers
                                      Buffers     Dynamic speculation
   GIQ                                           Dynamic speculation         ¬X(p) = X(¬ p)   ¬G(p) = F(¬ p)
   GIQ   Decode stage
         Decode stage                                                        ¬F(p) = G(¬ p)   ¬ pRq = ¬ pU¬q
         Issue stage
         Issue stage

RS
RS            RS
              RS                             RS
                                             RS           RS
                                                          RS                               For example, the negation of the interaction property is
        Execute stage
        Execute stage                                                G(¬ p1 ∨ ¬p2 ∨ . . . ∨ ¬pn) that becomes true if any of p1, p2,
                                            SU1          SU2

LSU stage 1 SU2 . . . , or pn is not true over all time steps. In the remainder of LSU stage 1 MU stage 1 MU stage 1 SU1 LSU stage 2 LSU stage 2 MU stage 2 MU stage 2 Divide Divide this section, we describe how to decompose these properties LSU stage 3 LSU stage 3 MU stage 3 MU stage 3 Post-divide MU stage 4 Post-divide (already negated) for efficient model checking. There are var- MU stage 4 ious combinations of temporal operators and Boolean connec- Completion stage tives where decompositions are not possible e.g., F(p ∧ q) = Completion stage Completion Write-back stage Completion F(p) ∧ F(q) and G(p ∨ q) = G(p) ∨ G(q). In certain situations, Write-back stage Queue Queue such as pUq, F(p → F(q)), or F(p → G(q)), decompositions Figure 2. Instruction Pipeline Flow of e500 processor that is are not beneficial compared to traditional model checking. The based on the Power Architecture Technology following combinations allow simple property decompositions.

they cannot. The micro-architectural features in the processor G(p ∧ q) = G(p) ∧ G(q) F(p ∨ q) = F(p) ∨ F(q) model include pipelined and clock-accurate behaviors such as X(p ∨ q) = X(p) ∨ X(q) X(p ∧ q) = X(p) ∧ X(q) multiple issue for instruction parallelism, out-of-order execu- Introducing the notion of clock (time step) in the property tion and in-order-completion for dynamic scheduling, register allows more decompositions for counterexample generation as renaming for removing false data dependency, reservation sta- shown below2. Note that the left and right hand side of the de- tions for avoiding stalls at Fetch and Decode pipeline stages, composition are not logically equivalent but they produce func- and data forwarding for early resolution of RAW data depen- tionally equivalent counterexamples. dency. By representing them in a model checking language, we can achieve the automatic test generation goal. G((clk = ts) ∨ (p ∨ q)) ≈ G((clk = ts) ∨ p) ∨ G((clk = ts) ∨ q) In order to use model checking as a test generator, the proces- Although we only use a few decomposition scenarios, it is sor model needs to be verified beforehand. Since it is infeasible important to note that these scenarios are sufficient for gener- to verify the entire model as a single unit due to the state ex- ating the properties where interactions are considered. In ad- plosion during model checking, we have partitioned the entire dition to these interaction properties, we created many micro- processor model into multiple modules based on the functional architectural properties based on real experiences of industrial units shown as rectangles in Figure 2. Each partitioned module designers. has been verified using the requirements and rules described in the specification. For verification of module interface, we inte- grated neighboring modules and verified their interface. These 3.3 Test Generation using Model Checking modules are basic units in processor model decomposition for test generation. The basic idea of DecompositionalMC( ) in Algorithm 1 is to apply the decomposed properties (sub-properties) to appropri- 3.2 Property Generation and Decomposition ate modules and compose their responses to construct the final test program. Model checker is used to generate partial coun- We generate a property for each pipeline interaction from the terexamples for the partitioned modules. Integration of these specification. Since interactions at a given cycle are semanti- partial counterexamples is a challenge due to the fact that the cally explicit and our processor model is organized in structure- relationships among decomposed modules and sub-properties oriented modules, the interactions can be converted into prop- are not preserved at whole design level in general. We propose erties. The generated properties are expressed in LTL (Linear clock-based integration of partial counterexamples. Temporal Logic) [2]. Each property consists of temporal oper- For example, if two sub-properties are applied at the same ators (G, F, X, U) and Boolean connectives (∧, ∨, ¬, and →). clock cycle (clk = ts) to two modules sharing a parent module, Most pipeline interactions can be converted in the form of a then two counterexamples are generated and merged into the property F(p1 ∧ p2 ∧ . . . ∧ pn) that combines activities pi over output property of the parent module for generating the coun- n modules using logical AND operator. The atomic proposition terexamples at the previous clock cycle (clk = ts − 1). In Fig- pi is a functional activity at a module i such as operation exe- ure 2, four reservation station (RS) modules share the parent cution, stall, exception or NOP. The property is true if (p1 ∧ p2 module Issue. Counterexamples generated from multiple RS at ∧ . . . ∧ pn) becomes true at any time step. the cycle k are merged for creating the output property of Is- Since we are interested in counterexample generation, we sue stage. The negated version of this property is applied to need to generate the negation of the property first. The negation 2The clk variable is used to count time steps, and ts is a specific time step.

Seventh International Workshop on Microprocessor Test and Verification (MTV'06) 0-7695-2839-2/06 $20.00 © 2006

                                    Table 1. Test Cases and Code Length
                          Test Cases                                             Test Code Length
                 1        Instruction dual issue                                        15
                 2        Renaming src1 operand                                         12
                 3        Read operand from forwarding path (RAW)                       9
                 4        Reservation station reads operand from forwarding path (RAW)  7
                 5        Read operand from renaming reg. (RAW)                         10
                 6        Read operand from GPR (RAW)                                   11

the model checker along with Issue module to generate a coun- the efficiency of our method by generating complicated micro- terexample at the cycle k − 1 that is used to produce the output architectural tests. Since the proposed technique is generic, properties of Decode, GIQ, and Rename buffer. Merging par- its framework can be used for validation of industrial-strength tial counterexamples continues until we obtain the primary in- processors. Our future work includes extension of the proces- put assignments for all the sub-properties. These assignments sor model for dynamic speculation and other features. Since contain fetched instruction data from I-cache and they are con- the number of interactions (directed tests) can be still extremely verted into assembly instruction sequences. large, we plan to develop a test compaction technique to reduce the number of test programs. 4 Experiments References We applied our methodology on a superscalar processor based on the Power Architecture Technology. We performed [1] D. Campenhout, T. Mudge, and J. Hayes. High-level test gener- various test generation experiments for validating the pipeline ation for design verification of pipelined microprocessors. DAC, interactions and corner cases. Table 1 shows a subset of the pages 185–188, 1999. directed test cases that we generated and their corresponding [2] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. length in terms of number of instruction sequences. For exam- MIT Press, Cambridge, MA, 1999. ple, test programs for case 3 through 6 exercise operand read [3] A. Gargantini and C. Heitmeyer. Using model checking to gen- from four different resources as shown in Figure 3, which can erate tests from requirements specifications. In ACM SIGSOFT be generated at micro-architecture level but very difficult at ISA Software Engineering Notes, volume 24, pages 146–162, 1999. level. In terms of efficiency, only several seconds were spent on [4] J. Hennessy and D. Patterson. Computer Architecture: A Quan- test generation. titative Approach. Morgan Kaufmann, 2002. [5] H. Iwashita, S. Kowatari, T. Nakata, and F. Hirose. Automatic test pattern generation for pipelined processors. ICCAD, pages Issue Issue Execute Execute Complete Complete Write-Back Write-Back 580–583, 1994. 33 55 66 [6] K. Kohno and N. Matsumoto. A new verification methodology for complex pipeline behavior. DAC, pages 816–821, 2001. [7] H.-M. Koo and P. Mishra. Functional test generation using Reservation Reservation 44 Instruction flow Station Instruction flow property decompositions for validation of pipelined processors. Station Forwarding data DATE, pages 1240–1245, 2006. Forwarding data [8] H.-M. Koo and P. Mishra. Test generation using SAT-based Figure 3. Four Different Data Forwarding Mechanisms bounded model checking for validation of pipelined processors. To validate these test cases, we converted the test programs GLSVLSI, 2006. into the input format of RTL simulation and monitored instruc- [9] P. Mishra and N. Dutt. Graph-based functional test program gen- tions in pipeline stages at every clock cycle during simulation eration for pipelined processors. DATE, pages 182–187, 2004. to ensure that the generated test program activates the actual [10] J. Shen and J. A. Abraham. An RTL abstraction technique for micro-architectural fault. processor microarchitecture validation and test generation. Jour- nal of Electronic Testing: Theory and Applications, 16(1-2):67– 81, 2000. 5 Conclusions [11] K. Shimizu, S. Gupta, T. Koyama, T. Omizo, J. Abdulhafiz, L. McConville, and T. Swanson. Verification of the cell broad- Architectural test generation techniques have limitations to band engine processor. DAC, pages 338–343, 2006. achieve micro-architectural coverage goal. This paper pre- [12] N. Utamaphethai, R. D. S. Blanton, and J. P. Shen. Effectiveness sented a directed test generation technique based on decom- of microarchitecture test program generation. IEEE Design & position of both processor model and properties for validation Test, 17(4):38–49, 2000. of performance as well as functionality of the modern micro- [13] www-cad.eecs.berkeley.edu/ kenmcmil/smv. Cadence SMV. processors. Our experimental results using e500 processor that [14] www.freescale.com/files/32bit/doc/refmanual/e500CORERMAD.pdf. is based on the Power Architecture Technology demonstrate Freescale PowerPc e500 core family reference manual.

Seventh International Workshop on Microprocessor Test and Verification (MTV'06) 0-7695-2839-2/06 $20.00 © 2006