MicroTESK: An Extendable Framework for
                                                                                        Test Program Generation

                                                             Alexander Kamkin∗, Tatiana Sergeeva∗, Andrei Tatarnikov∗† and Artemiy Utekhin‡
 ∗ Institute for System Programming of the Russian Academy of Sciences (ISPRAS)
                                                                  † National Research University Higher School of Economics (NRU HSE)
                                                                                    ‡ Moscow State University (MSU)
                                                                           Email: {kamkin,leonsia,andrewt,utekhin}@ispras.ru

Abstract— Creation of test programs and analysis of their menting and strengthening each other. It is a typical solution, execution is the main approach to system-level verification of for example, when general functionality of a microprocessor microprocessors. A lot of techniques have been proposed to is tested by randomly generated programs, while critical logic automate test program generation, ranging from completely random to well directed ones. However, no “silver bullet” has is verified by advanced model-based techniques. been found. In good industrial practices, various methods are Unfortunately, there is no framework that could accomodate combined complementing each other. Unfortunately, there is a variety of test program generation techniques. Engineers no solution that could integrate all (or at least most) of the have to use a number of tools with different input/output techniques in a single framework. Engineers are forced to usea number of tools, which leads to the following problems: formats, and it is a big problem how to integrate them and (1) it is required to maintain duplicating data (each tool uses keep their configurations in consistent states. It is not difficult its own representation of the target design); (2) to be used to use different tools for solving loosely connected tasks, together, tools need to be integrated (engineers have to deal with but settling tightly dependent problems by means of two or different formats and interfaces). This paper proposes a concept more tools might require deep knowledge of their internal of an extendable framework (MicroTESK) that follows a unified interfaces. The root of the problem is that different tools use methodology for defining test program generation techniques. The framework supports random and combinatorial generation different representation of the target design, and often one and (what is even more important) can be easily extended with representation is hidden from others. As a result, similar things new techniques being implemented as the framework’s plugins. are specified several times, duplicating data and complicating tests maintenance. I. INTRODUCTION We propose a concept of an extendable test program Being extremely complex, modern microprocessors require generation framework, named MicroTESK [6]. The idea is systematic activities for ensuring their correctness and reli- to represent knowledge about the microprocessor under test ability. Such activities are usually referred to as verification (a design/coverage model) in a general way and to provide and testing [1]. The first of them, verification, is applied in the easy access to that knowledge to a number of test generators development stage and focuses on discovering logical faults built as the framework’s plugins. Being shared among various in microprocessor designs (functional faults, interface faults, tools, a common model serves as a natural interface for etc.). The second one, testing, is related to the manufacturing their integration. Moreover, we have unified test generator stage and deals with diagnosing physical faults in integrated interfaces, making it possible to use different tools for solving circuits (stuck-at faults, bridging faults, etc.). The general a testing task and even to combine them for doing complex approach to both tasks is based on execution of verification/test jobs. Interaction between the framework and engineers is done programs, which are assembly programs causing some situa- with the help of test templates that specify test scenarios tions in the design (internal events, component interactions, in a hierarchical manner (dividing testing tasks into smaller etc.) [2]. (Throughout the paper we will use the term testing subtasks and linking each of them with an appropriate test to denote both verification and testing.) generator). By the present time, a great number of techniques for The rest of the paper is organized as follows. Section 2 automated test program generation have been proposed. All overviews existing test generation techniques and tools. Sec- of them can be subdivided in the following categories: tion 3 analyses the approaches described in Section 2 and (1) random generation [3], (2) combinatorial generation [2], formulates a concept of an extendable test program generation (3) template-based generation [4] and (3) model-based gener- framework. Section 4 outlines the framework architecture ation [5]. The thing is that there is no a “silver bullet”, which and introduces two main components: a modeling framework can effectively “fight” against all kinds of testing tasks. In real- and a testing framework. Section 5 considers the modeling life practice, different approaches are used together comple- framework and its components: a translator and a modeling library. Section 6 pays attention to the testing framework This work was supported in part by the Ministry of Education and Science consisting of a test template processor, a testing library and a of the Russian Federation under grant #8232 (06/08/2012). constraint solver engine. Section 7 concludes the paper.

II. TEST PROGRAM GENERATION TECHNIQUES                           step, it selects an instruction to be put into a program and,
   There is a variety of techniques for test program construc-   then, formulates and solves a constraint system for the chosen
   tion. All of them can be divided into two types: (1) manual   instruction.
test program development and (2)        automated test program           As opposed to the previously described approaches, model-

generation. Nowadays, manually created tests are rarely used based generation uses microprocessor models to compose test for systematic verification of microprocessors, but the ap- programs (or test templates). It is worthwhile clarifying the proach is still in use for testing hardly formalizable and terminology. There are two main types of models used in highly unlikely “corner cases” in microprocessor behavior. As microprocessor design and test: (1) instruction-level models for automated techniques, they can be subdivided into the (behavioral models) and (2) microarchitectual models (struc- following classes: (1) random generation, (2) combinatorial tural models). Models of the first type specify micropro- generation, (3) template-based generation and (4) model- cessors as instruction sets (in other words, they describe a based generation. programmer’s view to microprocessors: ‘How to write pro- grams for a microprocessor?’). Models of the second type Random generation is the most common technique to define the internal structure of microprocessors (this is a produce complex (though unsystematic) test programs for computer engineer’s point of view: ‘How a microprocessor is microprocessor verification. Being easy to implement, the organized inside?’). All test program generation methods and method, however, can create a significant workload to the tools apparently use instruction-level models, but only few of microprocessor and is able to detect some high-quality bugs. them use microarchitectural models. The latter ones are called One of the most famous generators of that type is RAVEN model-based. Let us consider some examples. (Random Architecture Verification Engine) developed by Ob- In [5], a method for directed test program generation has sidian Software Inc (now acquired by ARM) [3]. To generate been proposed. It takes detailed microprocessor specifications test programs, the tool not only applies randomization, but written in the EXPRESSION language [9] and translates them takes into account information about common microprocessor into the SMV (Symbolic Model Verifier) description [10]. faults. RAVEN is built upon pre-developed and custom made Specifications define the structure of the design (components modules that can be included into the generator to expand its and their interconnections), its behavior (semantics of the functionality [3]. Unforfunately, due to the lack of publicly instructions) and mapping between the structure and the be- available information, technical details are unclear. havior. The key part of the work is a fault model describing Another approach to test program construction is combi- typical errors for registers, individual operations, pipeline natorial generation. A brief analysis of microprocessor errata paths and for interactions between several operations. For each shows that many bugs can be detected by small test cases of the fault types, the set of concrete properties is generated, (2-5 instructions). Thus, it may be useful to systematically each of which is covered by a test case constructed by SMV enumerate short sequences of instructions (including test situ- (as a counterexample for the negation of the property). The ations for individual instructions and dependencies between generated test cases are mapped into test programs. As the instructions) [2]. The technique has been implemented in authors say, the technique does not scale well on complex the first version of MicroTESK (ISPRAS). The tool supports microprocessor designs. Thus, they suggest using the template- hierarchical decomposition of a test program generator into based approach as an addition. Test templates are developed iterators (each being responsible for iterating its own part by hand and describe sequences of instructions that create of the test) and combinators (combining results of the inner certain situations in the design’s behavior (first of all, pipeline iterators into complex test sequences). MicroTESK can also hazards). Test program generation is performed with the help construct test programs with branch instructions (generation of the graph model extracted from the specifications. It should is done by enumeration of control flow graphs and bounded be noticed that both approaches are based on rather accurate depth-first exploration of the execution traces) [7]. specifications, and it is better to apply them in the late design The next method is called template-based generation. A stages when the microarchitecture is stable. test template is an abstract representation of a test program, In [11], a microprocessor is formally specified as an oper- where constraints are used to specify possible values of ation state machine (OSM). The OSM is a system of com- instruction operands (instead of concrete values used in usual municating extended finite state machines (EFSMs) modeling programs). When constructing a test program, a generator the microprocessor at two levels: (1) the operational level tries to find random solutions to the given constraint systems and (2) the hardware level. At the first level, movement of (such approach is usually referred to as constraint-based the instructions across the pipeline stages is described (each random generation [8]). Automating routine work, the method operation is specified by an EFSM). At the second level, hard- considerably increases productivity of engineers. The leading ware resources are modeled using so-called token managers. generator of that kind is Genesys-Pro (IBM Research) [4]. This An operation EFSM changes its state by capturing/releasing is an architecture-independent tool that uses two types of input tokens of the token managers. The pipeline model is defined as data: (1) a model (containing architecture-specific information) a concurrent composition of the operation EFSMs and resource and (2) test templates (describing test scenarios). Genesys-Pro EFSMs. Test programs are generated on-the-fly by traversing generates test programs in an instruction-wise manner: at each all reachable states and transitions of the joint OSM model.

           III. EXTENDABLE FRAMEWORK CONCEPT                          The testing framework is comprised of engines of two types:
         Let us analyze the test generation techniques and tools   (1) test sequence generators and (2) test data generators.
having been surveyed previously and formulate a concept                   The main test sequence generators are random and combi-

of an extendable test program generation framework. It is natorial generators [2], [3]. It is explained by the fact that worthwhile answering the questions: ‘What is extendability?’ the modeling framework is organized around instruction-level and ‘What is an extendable framework?’ In general terms, ex- models, which give no information on how to compose instruc- tendability is a framework characteristic that shows how much tions into sequences for achieving particular testing goals. A effort it takes to integrate a new or existing component (in useful feature is support for test program composition [12]. our case, a microprocessor model or a test generation engine) Given two test programs (or test templates) focusing on into the framework. Indeed, the less effort it is required, the different (and more or less independent) situations, it may be more extendable the framework is. The object of this study is interesting to shuffle them with the intention to cause situations to suggest a framework architecture that would minimize the to occur simultaneously or close to each other. More advanced effort for creating new models/engines and plugging them into model-based generators can be installed into the framework the framework. together with the corresponding models. Moreover, extension There is a number of basic requirements that all kinds of the modeling framework shoud be always accompanied of extendable frameworks are expected to comply with. A by the extension of the testing framework (if a new type of system should be architected in such a way that there is a models is added into the framework, one should describe how core (platform) and there are extensions (plugins) connected to generate tests on the base of such models). to the core via the extension points. Obviously, there should We think, it is a promising practice to use constraint solvers be well-defined interfaces between the core and its extensions for test data generation (as it is done in Genesys-Pro [4]). as well as clear mechanisms for installing extensions into It implies that test situations are expressed as constraints the framework and calling them for solving particular tasks. on the instruction operands and the microprocessor state. An An optional requirement, which, we think, is essential for important property of the approach is that situations can be true extendable frameworks, is open source. The open source easily combined by conjuncting the constraints. In contrast to paradigm significantly simplifies creation and distribution of Genesys-Pro, we suggest using general-purpose SMT solvers framework extensions. (like Yices [13] and Z3 [14]) supporting the unified SMT- LIB notation [15]. In addition, the generation core can be There are also specific requirements to test program gener- extended with custom generators (which are useful when ation frameworks. Analyzing the approaches presented in the situations are hardly expressible in terms of constraints). There previous section, we can see that all of them use instruction- is also a library of predefined generators including random level models (either explicitly or implicitly). Evidently, to cre- generators and directed generators (e.g., for the floating-point ate a valid test program, one should know instruction formats arithmetic [16]). and instruction preconditions. However, if more sophisticated programs need to be generated, more complicated models IV. MICROTESK FRAMEWORK ARCHITECTURE should be utilized (finite state machines, nets, etc.). In our The MicroTESK framework is divided into two main parts: opinion, the core should be formed around instruction-level (1) the modeling framework and (2) the testing framework. The models, while more specialized models/engines should be purpose of the modeling framework is to represent a model organized as framework extensions. Another suggestion is to of the microprocessor under test (a design model) as well divide the test program generation framework into two parts: as model-based testing knowledge (a coverage model). The (1) the modeling framework and (2) the testing framework, design/coverage model is extracted from formal specifications each having its own core and being extendable. written in an architecture description language (ADL). The The core of the modeling framework allows describing testing framework, for its turn, is responsible for generating registers (as variables storing fixed-size bit vectors), memory test programs for the target microprocessor on the base of (as an array of machine words) and instructions (as atomic information provided by the model. Testing goals are defined operations over registers and memory). More detailed speci- in test templates written in a template description language fication is provided by so-called model extensions. There is (TDL). a number of points that such extensions can be connected The MicroTESK modeling framework consists of (1) a to (e.g., the memory access handler and the instruction exe- translator (analyzing formal specifications in an ADL and cution handler). The framework supports standard extensions producing the microprocessor model) and (2) a modeling for specifying memory management (cache hierarchy, address library (containing interfaces to be implemented by a model translation mechanisms, etc.) and pipelining (interconnection and classes to be used as building blocks) (see Figure 1). between pipeline stages, control flow transfers, etc.). Note that The translator includes two back-ends: (1) a model generator the standard extensions, in turn, have extension points and can (constructing an executable design model) and (2) a coverage be easily customized by engineers (e.g., it is possible to define extractor (building a coverage model for the microprocessor a cache replacement strategy or describe behavior of a pipeline instructions). In a similar fashion, the modeling library is split stage). into design and coverage libraries.

                      Modeling Framework                                            The framework functionality is divided into the following
          Formal      Translator           Modeling Library           aspects:     (1)       instruction set, (2)   memory  management    and
  Specifications       Model Generator     Design Library             (3) pipelining. Forming the framework core, the first aspect
                      Coverage Extractor        Coverage Library      is responsible for modeling microprocessor instructions and
                                                                      generating test programs on the base of the instruction-level
                      Model                                           models (random, combinatorial and template-based generators
                        Design Model       Coverage Model             are in active use). Support for the next ones, memory manage-
                                                                      ment and pipelining, is implemented in the standard plugins.
                      Testing Framework                               For other design aspects, custom plugins can be created and
                       Test Template  Testing Library                 installed into the framework.
  Test Templates         Processor    Test Sequence Generators                                    V. MICROTESK MODELING FRAMEWORK
                         Constraint       Test Data Generators                          The purpose of the MicroTESK modeling framework is to
                       Solver Engine                                  represent knowledge about a microprocessor and share that
                      External Solvers     Test Programs              knowledge with the testing framework. An engineer provides
                                                                      formal specifications             of the microprocessor under test. The
                                                                      specifications are processed by the           translator (including the
    Figure 1.       General structure of the MicroTESK framework      front-end and two back-ends, the            model generator     and the
                                                                      coverage extractor). The translator produces the            model    by
    Framework Plugin      Design Aspect                               using the    modeling library (comprising the design         and   cov-
          Modeling            Core                                    erage libraries). Let us consider the modeling framework
                                                                      components in more detail.
             Translator                     Instruction Set           A. Translator
              Library      Extensions                                    The  translator  processes formal specifications          of the mi-
                                           Memory Management          croprocessor and builds the     design/coverage model           (apply-
          Testing                                                     ing the model generator/coverage extractor and using the
          Test Generators                      Pipelining             building blocks defined in the design/coverage library). Note
              Solvers                         User Defined            that microprocessor specifications are written in a mixture
                                                                      of languages, each being responsible its own design aspect.
                                                                      The central part of specifications is related to the instruction
  Figure 2. Design aspects and organization of a MicroTESK plugin     set architecture; other parts describe memory management,
                                                                      pipelining, etc. As specifications are heterogeneous, the trans-
                                                                      lator is actually represented as a set of tools processing their
               Components of the MicroTESK testing framework are as   parts of specifications.
follows: (1) a test template processor (handling test templates                             At the moment, Sim-nML [17], [18] is the only ADL

written in a TDL and generating test programs), (2) a testing supported by MicroTESK for specifying microprocessors at library (containing a wide range of test sequence generators the instruction level. Sim-nML code specifying the integer ad- and test data generators used by the test template processor) dition instruction (ADD) from the MIPS instruction set [19] is and (3) a constraint solver engine (providing the test gener- shown below. Several things need to be emphasized: (1) spec- ators of the testing library with a Java interface to external ifications can use the predefined function UNPREDICTABLE SMT solvers). to indicate the situations, where the design’s behavior is The framework components are not monolithic – they undefined; (2) by analyzing control and data flows in instruc- include some core functionality as well as extensions oriented tion specifications one can automatically extract the coverage to specific tasks. Such tasks are usually grouped according model; (3) instructions can be grouped together providing the to the design aspects they deal with. All extensions related framework with useful information to be used within test to the same aspect are united into a framework plugin (see templates; (4) basing on such specifications, the framework Figure 2). To extend the framework with features aimed at is able to predict the result of the test program execution [12]. modeling/testing a new design aspect, one should develop op ADD( r d : GPR , r s : GPR , r t : GPR) extensions for all of the framework components, including a c t i o n = { a modeling library (to provide building blocks for modeling i f ( NotWordValue ( r s ) NotWordValue ( r t ) ) the design aspect), a testing library (to let the framework the n know of how to test the design aspect) and a specification UNPREDICTABLE ( ) ; language coupled with a translator (to make it possible to e n d i f ; express properties on the design aspect in a human-readable tmp = r s < 3 1 . . 3 1 > : : r s <31..0 > + form). r t < 3 1 . . 3 1 > : : r t <31..0 >;

     i f  ( tmp <32..32 >      != tmp <31..31 >)                                  usable engine built-in into the framework uses the constraint-
     the n                                                                        based description of situations and constraint solving [20].
          S i g n a l E x c e p t i o n ( ” I n t e g e r O v e r f l o w ” ) ;
     e l s e                                                                          VI. MICROTESK TESTING FRAMEWORK
          r d   =    s i g n   e x t e n d ( tmp word < 3 1 . . 0 > ) ;                         The MicroTESK testing framework is responsible for gen-
     e n d i f  ;                                                                 erating test programs. An engineer provides a           test template
}                                                                                 describing a test scenario for the microprocessor under test.
                                                                                  The test template is handled by the test template processor
s y n t a x     =    f o r m a t ( ” add %s ,     %s , %s ” ,                     by using the engines of the testing library: (1) it applies the
     r d . s y n t a x ,     r s . s y n t a x ,  r t . s y n t a x )             test sequence generators to construct a symbolic test program
                                                                                  (i.e., sequence of instructions annotated with test situations);
op   ALU = ADD               | SUB | . . .                                        (2) it requests the  test data generators        to generate concrete
                                                                                  values of the instruction operands; (3) it instantiates the test
B. Design Library                                                                 program by inserting control code initializing the registers and
                   The design library is intended to represent a microprocessor   the memory with the generated test data. Let us consider the
model, which is used to simulate instruction execution and to                     testing framework components in more detail.
keep track of the design state during test program generation.                    A. Test Template Processor
State tracking is essential for generating                  self-checking tests
(i.e., programs with built-in checks of the microprocessor                                    The test template processor is a runtime environment that

state). In addition to the instruction simulator (which simulates handles a test template, chooses appropriate engines of the instructions and updates the model state) and the state observer testing library and produces a test program. The supported (which provides access to the model state), the design model TDL is organized as a Ruby [21] library. It allows describing provides meta-information describing the design elements instruction sequences in a way it is done in the assembly (registers, memory, instructions, etc.). The meta-information language (by using the meta-information provided by the de- is the main interface between the modeling framework and sign model) though supporting high-level scenario description the test template processor. constructs. The latter ones can be subdivided into two types: The design library has several extension points that allow (1) native Ruby constructs (conditional statements, loops, etc.) engineers to connect their components. The set of extension and (2) special MicroTESK constructs (test sequence blocks, points includes (1) the memory access handler and (2) the test situations, etc.). A simple test template example is given instruction execution handler. The handler of the first type is below. invoked every time a memory location is accessed for reading # Assembly −S t y l e Code or writing. It may encapsulate memory management logic such add r [ 1 ] , r [ 2 ] , r [ 3 ] as address translation and caching. The handler of the second s u b r [ 1 ] , r [ 1 ] , r [ 4 ] type is launched when an instruction is executed. It is usually used to model the microprocessor pipeline – decomposition of # Ruby C o n t r o l S t a t e m e n t s instructions into microoperations and their scheduling. ( 1 . . 3 ) . each do | i | C. Coverage Library add r [ i ] , r [ i + 1 ] , r [ i +2] The coverage library is used to describe situations that can end s ub r [ i ] , r [ i ] , r [ i +3] occur in a microprocessor (an overflow, a cache miss/hit, a pipeline bypass, etc.). Such a description (referred to as a # T e s t S e q u e n c e Block coverage model) serves as a basis for generating test programs b l o c k ( : e n g i n e => ” random ” , (especially, for creating test data for individual instructions of a : c o u n t => 2 0 1 3 ) program). Besides the test situations, the coverage model con- { tains grouping rules, classifying microprocessor instructions add r [ 1 ] , r [ 2 ] , r [ 3 ] according to some criteria (number of operands, resources s u b r [ 1 ] , r [ 2 ] , r [ 3 ] being accessed, control flow structure, etc.). Similar to the # T e s t S i t u a t i o n R e f e r e n c e design model, the coverage model provides meta-information do o v e r f l o w end on its elements, which is used by the test template processor. } Each test situation has a unique name that can be used in a test template to refer to the situation. There is a mapping of An important notion used in test templates is a test sequence situation names onto test generators. Thus, the test template block. In fact, a test template is a hierarchical structure processor knows which engine to use to create a particular of test sequence blocks, each holding a set of instructions test case. To make the engine comprehend how it can be (or nested blocks) and specifying a test sequence generator done, the situation include an engine-specific description of (and its parameters) to be used to produce a test sequence. the condition/action causing the situation to occur. The most The test template processor constructs test sequences for the

nested blocks by applying the corresponding engines and then                           #   N e s t e d   Block    B
combines/composes the built sequences with the root engine                             b l o c k ( : e n g i n e  => ” p e r m u t a t e ” ) {
(an example is given the section “Test Sequence Generators”).                                  l d     r [ k ] ,  r [ l ]
                 Another important feature of the test template processor                      s t     r [m] ,    r [ n ]
is support for generation of               self-checking tests. When con-              }
structing a test program, the test template processor can inject             }
special pieces of code that check whether the microprocessor                           In the example above, there is one top-level block contain-

state is valid in the corresponding execution point. Such code ing two nested blocks, A and B. Block A consists of four (called a test oracle) compares data stored in the previously instructions, ADD, SUB, MULT and DIV. Block B consists accessed registers and memory blocks with the reference data of LD and ST. The engine associated with A generates two (calculated by the instruction simulator) and terminates the sequences (:count => 2) of the length three (:length program if they do not match. => 3) composed of the instructions listed in the block. The B. Test Sequence Generators engine associated with B generates all permutations of the in- ner instructions (there are two permutations of two elements). A test sequence generator is organized as an iterator of test The top-level engine produces all possible combinations of the sequences. In the simplest case, a test sequence generator re- nested blocks’ sequences (:combine => "product") and turns a single test sequence for a single test sequence block. As randomly mixes them (:compose => "random"). The blocks can be nested, generators can be combined/composed in result may look as follows. a recursive manner. To do it, two strategies should be defined # C o m b i n a t i o n ( 1 , 1 ) for each non-terminal block: (1) a combinator (describing s u b r [ d ] , r [ e ] , r [ f ] # Block A how to combine the results of the inner iterators) and (2) a l d r [ k ] , r [ l ] # Block B compositor (defining the method for merging several pieces of d i v r [ i ] , r [ j ] # Block A code together). Thus, a combinator produces the combinations s t r [m] , r [ n ] # Block B of the inner test sequences, while a compositor merges those add r [ a ] , r [ b ] , r [ c ] # Block A sequences into the one. The testing library contains a variety of combinators and # C o m b i n a t i o n ( 1 , 2 ) compositors. The most usable combinators are: (1) a random s t r [m] , r [ n ] # Block B combinator (produces a number of random combinations s u b r [ d ] , r [ e ] , r [ f ] # Block A of the inner iterators’s results), (2) a product combinator l d r [ k ] , r [ l ] # Block B (creates all possible combinations of the inner blocks’ test d i v r [ i ] , r [ j ] # Block A sequences) and (3) a diagonal combinator (synchronously add r [ a ] , r [ b ] , r [ c ] # Block A requests the inner iterators and joins their results). The set of implemented compositors include: (1) a random compositor # C o m b i n a t i o n ( 2 , 1 ) (randomly mixes the inner test sequences), (2) a catenation m u l t r [ g ] , r [ h ] # Block A compositor (catenates the inner test sequences) and (2) a m u l t r [ g ] , r [ h ] # Block A nesting compositor (embeds the inner test sequences one into l d r [ k ] , r [ l ] # Block B another). Note that engineers are allowed to add their own add r [ a ] , r [ b ] , r [ c ] # Block A test sequence generators, combinators and compositors into s t r [m] , r [ n ] # Block B the testing library and invoke them from test templates. Let us consider a simple example. # C o m b i n a t i o n ( 2 , 2 ) # T e s t S e q u e n c e Block m u l t r [ g ] , r [ h ] # Block A b l o c k ( : combine => ” p r o d u c t ” , s t r [m] , r [ n ] # Block B : compose => ” random ” ) { m u l t r [ g ] , r [ h ] # Block A l d r [ k ] , r [ l ] # Block B # N e s t e d Block A add r [ a ] , r [ b ] , r [ c ] # Block A b l o c k ( : e n g i n e => ” random ” , : l e n g t h => 3 , C. Test Data Generators : c o u n t => 2 ) { A symbolic test program produced by test sequence gen- add r [ a ] , r [ b ] , r [ c ] erators does not necessarily define values of all of the in- s ub r [ d ] , r [ e ] , r [ f ] struction operands (leaving some of them either undefined m u l t r [ g ] , r [ h ] or deliberately ambiguous). The job of test data generators d i v r [ i ] , r [ j ] is to construct operand values on the base of the provided } test situations. Test data generation relies on the constraint solver engine that constructs operand values by solving the corresponding constraints. To achieve a given test situation,

the test template processor selects an appropriate test data types of models and test generation engines are supposed to generator and requests the design model for the state of the be added as the framework’s extensions. The goal of our work involved design elements. After that, it initializes the closed is not to create a “silver bullet” for microprocessor verification variables of the constraint (variables whose values are defined and testing (which, we believe, does not exist), but to organize by the previouly executed instructions) and calls the constraint a flexible, open-source environment being able to absorb solver engine to construct the free variables’ values. a variety of useful approaches. Let us emphasize that the As soon as the operand values are constructed, the test development having been launched at ISPRAS is based on the data generator returns control code, which is a sequence many-years experience of verifying industrial microprocessors. of instructions that accesses the microprocessor resources The work has not been finished, and there are a lot of things associated with the instruction operands and brings them into need to be done. In the nearest future, we are planning to the required states. For example, if an instruction operand is implement the framework core and customize the generator for a register, control code writes the constructed value into that widely-spread microprocessor architectures, including ARM register. Following the concept of the constraint-based random and MIPS. We are also working on MicroTESK’s extensions generation, different calls of a test data generator may lead to for specifying/testing memory management mechanisms and different values of free variables. However, each generated set pipeline control logic. of values should cause the specified test situation. REFERENCES D. Constraint Solver Engine [1] M.S. Abadir, S. Dasgupta, Guest Editors’ Introduction: Microprocessor The constraint solver engine is a framework component Test and Verification. IEEE Design & Test of Computers, Volume 17, Issue 4, 2000, pp. 4–5. that helps test data generators to construct test data by [2] A. Kamkin. Test Program Generation for Microprocessors. Institute for solving constraints specified in test situations. The engine is System Programming of RAS, Volume 14, Part 2, 2008, pp. 23–63 (in implemented as a collection of solvers encapsulated behind a [3] Russian). http://www.arm.com/community/partners/display product/rw/ProductId/5171/. generic interface. Solvers are divided into two major families: [4] A. Adir, E. Almog, L. Fournier, E. Marcus, M. Rimon, M. Vinov (1) universal solvers (handling a wide range of constraint and A. Ziv. Genesys-Pro: Innovations in Test Program Generation for types) and (2) custom solvers (aimed at specific test data Functional Processor Verification. IEEE Design & Test of Computers, Volume 21, Issue 2, 2004, pp. 84–93. generation tasks). [5] P. Mishra and N. Dutt. Specification-Driven Directed Test Generation Universal solvers are built around external SMT solvers (like for Validation of Pipelined Processors. ACM Transactions on Design Yices [13] and Z3 [14])), which provide a rich constraint Automation of Electronic Systems (TODAES), Volume 13, Issue 3, 2008, pp. 1–36. description language (supporting Boolean algebra, arithmetic, [6] http://forge.ispras.ru/projects/microtesk. logic over fixed-size bit vectors and other theories) as well as [7] A. Kamkin. Some Issues of Automation of Test Program Generation for effective decision procedures for solving such constraints. The Branch Units of Microprocessors. Institute for System Programming of RAS, Volume 18, 2010, pp. 129–150 (in Russian). MicroTESK framework uses Java Constraint Solver API [20] [8] Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus and providing a generic interface to SMT-LIB-based constraint G. Shurek. Constraint-Based Random Stimuli Generation for Hardware solvers [15]. The library allows dynamically creating con- [9] Verification. AI Magazine, Volume 28, Number 3, 2007, pp. 13–30. P. Grun, A. Halambi, A. Khare, V. Ganesh, N. Dutt and A. Nicolau. straints in Java, mapping them to the SMT-LIB descriptions, EXPRESSION: An ADL for System Level Design Exploration. Technical launching a solver and transferring results back to Java. [10] Report 1998-29, University of California, Irvine, 1998. Some test situations are hardly expressible in terms of [11] http://www.cs.cmu.edu/˜modelcheck/smv.html. T.N. Dang, A. Roychoudhury, T. Mitra and P. Mishra. Generating Test SMT constraints (e.g., situations in floating-point arithmetic, Programs to Cover Pipeline Interactions. Design Automation Confer- memory management, etc.). For such situations engineers [12] ence (DAC), 2009, pp. 142–147. are able to provide special custom solvers/generators. Note A. Kamkin, E. Kornykhin and D. Vorobyev. s Reconfigurable Model- Based Test Program Generator for Microprocessors. Software Testing, that custom solvers can also use SMT solvers to construct Verification and Validation Workshops (ICSTW), 2011, pp. 47–54. test data; though they usually implement non-trivial logic on [13] B. Dutertre and L. Moura. The YICES SMT Solver. 2006 forming a constraint system and interpreting its solution. When [14] (http://yices.csl.sri.com/tool-paper.pdf). L. Moura and N. Bjørner. Z3: An Efficient SMT Solver. Conference on the design/coverage model is extended with a new type of Tools and Algorithms for the Construction and Analysis of Systems knowledge, it often means a need to provide a corresponding [15] (TACAS), 2008, pp. 337–340. custom solver. To facilitate extension of the constraint solver D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial. GrammaT- ech, Inc., Version 1.1, 2011. engine with new solvers, both universal and custom solvers [16] M. Aharoni, S. Asaf, L. Fournier, A. Koifman and R. Nagel. FPgen – A implement uniform interfaces. Test Generation Framework for Datapath Floating-Point Verification. High Level Design Validation and Test Workshop (HLDVT), 2003. VII. CONCLUSION [17] pp. 17–22. M. Freericks, The nML Machine Description Formalism. Techical Re- We have suggested the extendable achitecture for test pro- [18] port, TU Berlin, FB20, Bericht 1991/15. gram generation framework. The proposed solution, named R. Moona, Processor Models For Retargetable Tools. International Workshop on Rapid Systems Prototyping (RSP), 2000, pp. 34–39. MicroTESK, can combine a wide range of microprocessor [19] MIPS64T M Architecture For Programmers. Volume II: The modeling and testing techniques. The central part of the MIPS64T M Instruction Set, Document Number: MD00087, Revision framework is built around instruction-level models and ran- [20] 2.00, June 9, 2003. http://forge.ispras.ru/projects/solver-api. dom/combinatorial test program generators. More complicated [21] http://www.ruby-lang.org.