Prabhat Mishra
email: prabhat@cise.ufl.edu

Nikil Dutt
email: dutt@uci.edu

Functional Coverage Driven Test Generation for Validation of Pipelined Processors *

Functional verification of microprocessors is one of the most complex and expensive tasks in the current system-on-chip design process. A significant bottleneck in the validation of such systems is the lack of a suitable functional coverage metric. This paper presents a functional coverage based test generation technique for pipelined architectures. The proposed methodology makes three important contributions. First, a general graphtheoretic model is developed that can capture the structure and behavior (instruction-set) of a wide variety of pipelined processors. Second, we propose a functional fault model that is used to define the functional coverage for pipelined architectures. Finally, test generation procedures are presented that accept the graph model of the architecture as input and generate test programs to detect all the faults in the functional fault model. Our experimental results on two pipelined processor models demonstrate that the number of test programs generated by our approach to obtain a fault coverage is an order of magnitude less than those generated by traditional random or constrainedrandom test generation techniques.

Introduction

As embedded systems continue to face increasingly higher performance requirements, deeply pipelined processor architectures are being employed to meet desired system performance. Functional validation of such programmable processors is one of the most complex and expensive tasks in the current Systemson-Chip (SOC) design methodology. Simulation is the most widely used form of microprocessor verification: millions of cycles are spent during simulation using a combination of random and directed test cases in traditional validation flow. Several coverage measures are commonly used, such as code coverage, toggle coverage and fault coverage. Unfortunately, these measures do not have any direct relationship to the functionality of the device. For example, none of these determine if all possible interactions of hazards, stalls and exceptions are tested in a processor pipeline. Thus there is a need for a coverage metric based on the functionality of the design.

To define a useful functional coverage metric, we need to define a fault model of the design that is described at the functional level and independent of the implementation details. In this paper, we present a functional fault model for pipelined processors. The fault model should be applicable to the wide varieties of today's microprocessors from various architectural domains (such as RISC, DSP, VLIW and Superscalar) that differ widely in terms of their structure (organization) and behavior (instruction-set). We have developed a graph-theoretic model that can capture a wide spectrum of pipelined processors, coprocessors, and memory subsystems. We have defined functional coverage based on the effects of faults in the fault model applied at the level of the graph-theoretic model. This allows us to compute functional coverage of a pipelined processor for a given set of random or constrained-random test sequences.

We have developed test generation procedures that accept the graph model of the pipelined processor as input and generate test programs to detect all the faults in the functional fault model. We applied our methodology on two pipelined processors: a VLIW implementation of the DLX architecture [START_REF] Hennessy | Computer Architecture: A Quantitative Approach[END_REF], and a RISC implementation of the SPARC V8 architecture [19]. Our experimental results demonstrate two important aspects of our technique. First, it shows how our functional coverage can be used in an existing validation flow that uses random or directed-random test programs. Second, it demonstrates that the required number of test sequences generated by our algorithms to obtain a given fault (functional) coverage is an order of magnitude less than the random or constrained-random test programs.

The rest of the paper is organized as follows. Section 2 presents related work addressing validation of pipelined processors. Section 3 presents a graph-based modeling of pipelined architectures. The functional fault models are described in Section 4. Section 5 defines the functional coverage based on the fault model. Section 6 presents the test generation procedures followed by a case study in Section 7. Finally, Section 8 concludes the paper.

Related Work

Traditionally, validation of a microprocessor has been performed by applying a combination of random and directed test programs using simulation techniques. Many techniques have been proposed for generation of directed test programs [START_REF] Aharon | Test program generation for functional verification of PowerPC processors in IBM[END_REF][START_REF] Fine | Coverage directed test generation for functional verification using bayesian networks[END_REF][START_REF] Behm | Industrial experience with test generation languages for processor verification[END_REF][START_REF] Miyake | Automatic test generation for functional verification of microprocessors[END_REF][START_REF] Shen | Functional verification of the equator MAP1000 microprocessor[END_REF]. These techniques do not consider pipeline behavior for generating test programs.

Ur and Yadin [START_REF] Ur | Micro architecture coverage directed generation of test programs[END_REF] have presented a method for generation of assembler test programs that systematically probe the microarchitecture of a PowerPC processor. Iwashita et al. [START_REF] Iwashita | Automatic test pattern generation for pipelined processors[END_REF] use an FSM based processor modeling to automatically generate test programs. Campenhout et al. [START_REF] Campenhout | High-level test generation for design verification of pipelined microprocessors[END_REF] have proposed a test genera- tion algorithm that integrates high-level treatment of the datapath with low-level treatment of the controller. Kohno et al. [START_REF] Kohno | A new verification methodology for complex pipeline behavior[END_REF] have presented a tool that generates test programs for verifying pipeline behavior in the presence of hazards and exceptions. Ho et al. [START_REF] Ho | Architecture validation for processors[END_REF] have presented a technique for generating test vectors for verifying the corner cases of the design. Mishra et al. [START_REF] Mishra | Graph-based functional test program generation for pipelined processors[END_REF] have proposed a graph-based functional test program generation technique for pipelined processors using model checking. None of these techniques provides a comprehensive metric to measure the coverage of the pipeline interactions. An extensive survey on coverage metrics in simulation-based verification is presented by Tasiran et al. [START_REF] Tasiran | Coverage metrics for functional validation of hardware designs[END_REF]. Andrew Piziali [START_REF] Piziali | Functional Verification Coverage Measurement and Analysis[END_REF] has presented a comprehensive study on functional verification coverage measurement and analysis. Many researchers have proposed techniques for generation of functional test programs for manufacturing testing of microprocessors ( [START_REF] Chen | A scalable software-based self-test methodology for programmable processors[END_REF], [START_REF] Thatte | Test generation for microprocessors[END_REF]). These techniques use stuck-at fault coverage to demonstrate the quality of the generated tests. To the best of our knowledge, there are no previous approaches that describe functional fault models for pipelined architectures, use it to define functional coverage, and generate test programs to detect all the functional faults in the fault model.

Architecture Model of a Pipelined Processor

Modeling plays a central role in the generation of test programs for validation of pipelined processors. In this section, we briefly describe how the graph model captures the structure and behavior of the processor using the information available in the architecture manual.

Structure

The structure of an architecture pipeline is modeled as a graph with the components as nodes and the connectivity as the edges. We consider two types of components: units (e.g., ALUs) and storages (e.g., register files). There are two types of edges: pipeline edges and data transfer edges. A pipeline edge transfers instruction (operation) between two units. A data-transfer edge transfers data between units and storages.

For illustration, we use a simple multi-issue architecture consisting of a processor, a co-processor and a memory subsystem.

Figure 1 shows the graph-based model of this architecture that can issue up to three operations (an ALU operation, a memory access operation, and a coprocessor operation) per cycle. In the figure, oval boxes denote units, dotted ovals are storages, bold edges are pipeline edges, and dotted edges are data-transfer edges. A path from a root node (e.g., Fetch) to a leaf node (e.g, WriteBack) consisting of units and pipeline edges is called a pipeline path. For example, one of the pipeline path is {Fetch, Decode, ALU, WriteBack}. A path from a unit to main memory or register file consisting of storages and data-transfer edges is called a data-transfer path. For example, {MemCntrl, L1, L2, MainMemory} is a data-transfer path.

Behavior

The behavior of the architecture is typically captured by the instruction-set (ISA) description in the processor manual. It consists of a set of operations1 that can be executed on the architecture. Each operation in turn consists of a set of fields (e.g. opcode, arguments) that specify, at an abstract level, the execution semantics of the operation. We model the behavior as a graph, where the nodes represent the fields of each operation and the edges represent orderings between the fields. Figure 2 describes a portion of the behavior (consisting of two operation graphs) for the example processor shown in Figure 1.

Nodes are of two types: opcode and argument. The opcode nodes represent the opcode (i.e. mnemonic), and the argument nodes represent argument fields (i.e., source and destination arguments). In Figure 2, the ADD and STORE nodes are opcode nodes, while the others are argument nodes. Edges are also of two types: operation and execution. The operation edges link the fields of the operation and also specify the syntactical ordering between them. On the other hand, the execution edges specify the execution ordering between the fields. In Figure 2, the solid edges represent operation edges while the dotted edges represent execution edges. For the ADD operation, the operation edges specify that the syntactical ordering is opcode followed by DEST, SRC1 and SRC2 arguments (in that order), and the execution edges specify that the SRC1 and SRC2 arguments are executed (i.e., read) before the ADD operation is performed. Finally, the DEST argument is written.

Operation Edge Execution Edge

Argument Node

Opcode Node

SRC1 STORE SRC OFFSET SRC2 ADD DEST SRC1

Figure 2. A Fragment of the Behavior Graph

The architecture manual also provides information regarding the mapping between the structure and behavior. We define a set of mapping functions that map nodes in the structure to nodes in the behavior (and vice-versa). The unit-to-opcode (opcode-to-unit) mapping is a bi-directional function that maps unit nodes in the structure to opcode nodes in the behavior. The unit-to-opcode mappings for the architecture in Figure 1 include mappings from Fetch unit to opcodes {ADD, STORE}, ALU unit to opcode ADD, AddrCalc unit to opcode STORE etc. The argument-to-storage (storage-to-argument) mapping is a bi-directional function that maps argument nodes in the behavior to storage nodes in the structure. For example, the argumentto-storage mappings for the ADD operation are mappings from {DEST, SRC1, SRC2} to RegisterFile.

Functional Fault Models

In this section, we present fault models for various functions in a pipelined processor. We categorize various computations in a pipelined processor into register read/write, operation execution, execution path and pipeline execution. We outline the underlying fault mechanisms for each fault model, and describe the effects of these faults at the level of the architecture model presented in Section 3.

Fault Model for Register Read/Write

To ensure fault-free execution, all registers should be written and read correctly. In the presence of a fault, reading of a register will not return the previously written value. The fault could be due to an error in reading, register decoding, register storage, or prior writing. The outcome is an unexpected value. If V R i is written in register R i and read back, the output should be V R i in fault-free case. In the presence of a fault, output = V R i .

Fault Model for Operation Execution

All operations must execute correctly if there are no faults. In the presence of a fault, the output of the computation is different from the expected output. The fault could be due to an error in operation decoding, control generation or final computation. Erroneous operation decoding might return an incorrect opcode. This can happen if incorrect bits are decoded for the opcode. Selection of incorrect bits will also lead to erroneous decoding of source and destination operands. Even if the decoding is correct, due to an error in control generation an incorrect computation unit can be enabled. Finally, the computation unit can be faulty. The outcome is an unexpected result. Let val i , where val i = f opcode i (src 1 , src 2 , ...), denote the result of computing the operation "opcode i dest, src 1 , src 2 , ...". In the fault-free case, the destination will contain the value val i . Under a fault, the destination is not equal to val i .

Fault Model for Execution Path

During execution of an operation in the pipeline, one pipeline path and one or more data-transfer paths get activated. We define all these activated paths as the execution path for that operation. An execution path ep op i is faulty if it produces incorrect result during execution of operation op i in the pipeline. The fault could be due to an error in one of the paths (pipeline or data-transfer) in the execution path. A path is faulty if any one of its nodes or edges are faulty. A node is faulty if it accepts valid inputs and produces incorrect outputs. An edge is faulty if it does not transfer the data/instruction correctly.

Without loss of generality, let us assume that the processor has p pipeline paths (PP = ∪ p i=1 pp i ) and q data-transfer paths (DP = ∪ q j=1 d p j ). Furthermore, each pipeline path pp i is connected to a set of data-transfer paths DPgrp i (DPgrp i ⊆ DP). During execution of an operation op i in the pipeline path pp i , a set of data-transfer paths DP op i (DP op i ⊆ DPgrp i ) are used (activated). Therefore, the execution path ep op i for operation op i is, ep op i = pp i ∪ DP op i . Let us assume, operation op i has one opcode (opcode i ), m sources (∪ m j=1 src j ) and n destinations (∪ n k=1 dest k ). Each data-transfer path d p i (d p i ∈ DP op i ) is activated to read one of the sources or write one of the destinations of op i in execution path ep op i . Let val i , where val i = f opcode i (∪ m j=1 src j ), denote the result of computing the operation op i in execution path ep i . The val i has n components (∪ n k=1 val k i ). In the fault-free case, the destinations will contain correct values, i.e., ∀k dest k = val k i . Under a fault, at least one of the destinations will have incorrect value, i.e., ∃k dest k = val k i .

Fault Model for Pipeline Execution

The previous fault models consider only one operation at a time. An implementation of a pipeline is faulty if it produces incorrect results due to execution of multiple operations in the pipeline. The fault could be due to incorrect implementation of the pipeline controller. The faulty controller might have erroneous hazard detection, incorrect stalling, erroneous flushing, or wrong exception handling schemes.

Let us define stall set for a unit u (SS u ) as all possible ways to stall that unit. Therefore, the stall set for the architecture StallSet = ∪ ∀u SS u . Let us also define the exception set for a unit u (ES u ) as all possible ways to create an exception in that unit. We define the set of all possible multiple exception scenarios as MESS. Hence, the exception set for the architecture ExceptionSet = ∪ ∀u ES u ∪ MESS. We consider two types of pipeline interactions: stalls and exceptions. Therefore, all possible pipeline interactions (PIs) can be defined as: PIs = StallSet ∪ ExceptionSet. Let us assume a sequence of operations ops pi causes a pipeline interaction pi (i.e., pi ∈ PIs), and updates n storage locations. Let val pi denote the result of computing the operation sequence ops pi . The val pi has n components (∪ n k=1 val k pi ). In the fault-free case, the destinations will contain correct values, i.e., ∀k dest k = val k i . Under a fault, at least one of the destinations will have incorrect value, i.e., ∃k dest k = val k i .

Functional Coverage Estimation

We define functional coverage based on the fault models described in Section 4. Consider the following cases:

• a fault in register read/write is covered if the register is written first and read later.

• a fault in operation execution is covered if the operation is performed, and the result of the computation is read.

• a fault in execution path is covered if the execution path is activated, and the result of the computation is read.

• a fault in pipeline execution is covered if the fault is activated due to execution of multiple operations in the pipeline, and the result of the computation is read.

We compute functional coverage of a pipelined processor for a given set of test programs as the ratio between the number of faults detected by the test programs and the total number of detectable faults in the fault model.

Test Generation Techniques

In this section, we present test generation procedures for detecting faults covered by the fault models presented in Section 4. Different architectures have specific instructions to observe the contents of registers and memories. In this paper, we use load and store instructions to make the register and memory contents observable at the output data bus.

We first describe a procedure createTestProgram that is used by the test generation algorithms. The procedure accepts a list of operations as input and returns a modified list. It assigns appropriate values to the unspecified locations (opcodes or operands). Next, it creates initialization instructions for the uninitialized source operands. It also creates instructions to read the destination operands. Finally, it returns the modified list that contains the initialization operations, modified input operations, and the read operations (in that order).

Test Generation for Register Read/Write

Algorithm 1 presents the procedure for generating test programs for detecting faults in register read/write functions. The fault model for the register read/write function is described in Section 4.1. For each register in the architecture, the algorithm generates an instruction sequence consisting of a write followed by a read for that register. The function GenerateUniqueValue returns unique value for each register based on register name. A test program for register R i will consist of two assembly instructions: "MOVI R i , #val i " and "STORE R i , R j , #0". The move-immediate (MOVI) instruction writes val i in register R i . The STORE instruction reads the content of R i and writes it in memory addressed by R j (offset 0).

Test Generation for Operation Execution

Algorithm 2 presents the procedure for generating test programs for detecting faults in operation execution. The fault model for the operation execution is described in Section 4.2. The algorithm traverses the behavior graph of the architecture, and generates one test program for each operation graph using createTestProgram. For example, a test program for the operation graph with opcode ADD in Figure 2 has three operations: two initialization operations ("MOV R3 #333", "MOV R5 #212") followed by the ADD operation ("ADD R2 R3 R5"), followed by the reading of the result ("STORE R2, Rx, #0").

Test Generation for Execution Path

Algorithm 3 presents the procedure for generating test programs for detecting faults in execution path. The fault model for the execution path is described in Section 4.3. The algorithm traverses the structure graph of the architecture, and for each pipeline path it generates a group of operations supported by that path. It randomly selects one operation from each operation group. There are two possibilities. If all the edges in the execution path (containing the pipeline path) are activated by the selected operation, the algorithm generates all possible source/destination assignments for that operation. However, if different operations in the operation group activates different set of edges in the execution path, it generates all possible source/destination assignments for each operation in the operation group.

Test Generation for Pipeline Execution

Algorithm 4 presents the procedure for generating test programs for detecting faults in pipeline execution. The fault model for the pipeline execution is described in Section 4.4. The first loop (L1) traverses the structure graph of the architecture in a bottom-up manner, starting at leaf nodes. The second loop (L2) computes test programs for generating all possible exceptions in each unit using templates. The third loop (L3) computes test programs for creating stall conditions due to data and control hazards in each unit using templates. The fourth loop (L4) creates test programs to generate stall conditions using structural hazards. Finally, the last loop (L5) computes test sequences for multiple exceptions involving more than one units. The com-poseTestProgram function uses ordered 2 n-tuple units and combines their test programs. The function also removes dependencies across test programs to ensure the generation of multiple exceptions during the execution of the combined test program.

A Case Study

We applied our methodology on two pipelined architectures: a VLIW implementation of the DLX architecture [START_REF] Hennessy | Computer Architecture: A Quantitative Approach[END_REF], and a RISC implementation of the SPARC V8 architecture [19].

Experimental Setup

We developed our test generation and coverage analysis framework using Verisity's Specman Elite [18]. We captured executable specification of the architectures using Verisity's "e" language. This includes description of 91 instructions for the DLX, and 106 instructions for the SPARC V8 architecture. We refer to these as specifications. We implemented a VLIW version of the DLX architecture using Verisity's "e" language. It contains 5 pipeline stages: fetch, decode, execute, memory and writeback. The execute stage has four parallel execution paths: an ALU, a four-stage floating-point adder, a seven-stage multiplier, and a multi-cycle divider. We used the LEON2 processor [START_REF]LEON2 Processor[END_REF] that is a VHDL model of a 32-bit processor compliant with the SPARC V8 architecture. We refer these models (VLIW DLX and LEON2) as implementations. 2 The unit closer to completion has higher order Our framework generates test programs in three different ways: random, constrained-random, and our approach. Specman Elite [18] is used to generate both random and constrainedrandom test programs from the specification. Several constraints are used for constrained-random test generation. For example, to generate test programs for register read/write, we used the highest probability for choosing register-type operations in DLX. Since register-type operations have 3 register operands, the chances of reading/writing registers are higher than immediate type (2 register operands) or branch type (one register operand) operations. The test programs generated by our approach uses the algorithms described in Section 6. To ensure that the generated test programs are executed correctly, our framework applies the test programs on the implementation as well as the specification, and compares the contents of the program counter, registers and memory locations after execution of each test program.

The Specman Elite framework allows definition of various coverage measures that enables us to compute the functional coverage described in Section 5. We defined each entry in the instruction definition (e.g. opcode, destination and sources) as a coverage item in Specman Elite. The coverage for the destination operand gives the measure of which registers are written. Similarly, the coverage of source operands gives the measure of which registers are read. We used a variable for each register to identify a read after a write. Computation of coverage for operation execution is done by observing the coverage of the opcode field. The computation of coverage for execution path is performed by observing if all the registers are used for computation of all/selected opcodes. This is performed by using cross coverage of instruction fields in Specman Elite that computes every combination of values of the fields. Finally, we compute the coverage for pipeline execution by maintaining variables for stalls and exceptions in each unit. The coverage for multiple exceptions is obtained by performing cross coverage of the exception variables (events) that occur simultaneously. Currently, we consider only two simultaneous exceptions.

Results

In this section, we compare the test programs generated by our approach against the random and constrained-random test programs generated by the Specman Elite. The number 100% implies that the generated test programs covered all the faults in that fault model. For example, the Random technique covered all the faults in "Register Read/Write" function using 3900 tests. The number of test programs for operation execution are similar for both random and constrainedrandom approaches. This is because the constraint used in this case (same probability for all opcodes) may be the default option used in random test generation approach. We performed an initial study to evaluate the quality of our functional fault model using existing coverage measures. Table 2 compares our functional coverage against HDL code coverage. The first column indicates the functional fault models. The second column presents the minimum number of test programs generated by our test generation algorithms to cover all the functional faults in the corresponding fault model. The last column presents the code coverage obtained for the DLX implementation [17] using the test programs mentioned in the second column. As expected, our fault model performed well -a small number of test programs generated a high code coverage.

Table 3 shows the comparative results for different test generation approaches for the LEON2 processor. The trend is similar in terms of number of operations and fault coverage for both the DLX and LEON2 architectures. The random and constrainedrandom approaches obtained 100% functional coverage for the first three fault models using an order of magnitude more test vectors than our approach. We analyzed the cause for the low fault coverage in pipeline execution for the random and constraint-driven test generation approaches. These two approaches covered all the stall scenarios and majority of the single exception faults. However, they could not activate any multiple exception scenarios. Due to bigger pipeline structure (larger set of pipeline interactions) in the VLIW DLX, it has lower fault coverage than the LEON2 architecture in pipeline execution. This functional coverage problem will be even more important for today's deeply pipelined embedded processors.

Conclusions

Functional verification is widely acknowledged as a major bottleneck in microprocessor design due to lack of a suitable functional coverage estimation technique. This paper presented a functional coverage based test generation technique for pipelined architectures. The methodology made three important contributions. First, a general graph model was developed that can capture the structure and behavior (instruction-set) of a wide variety of pipelined processors. Second, we proposed a functional fault model that is used in defining the functional coverage. Finally, test generation procedures were presented that accept the graph model of the microprocessor as input and generate test programs to detect all the faults in the functional fault model. We are able to measure the goodness of a given set of random test sequences using our functional coverage metric. Our experimental results demonstrate that the required number of test sequences generated by our algorithms to obtain a given fault (functional) coverage is an order of magnitude less than the random or constrained-random test programs.

Our future work includes application of these test programs for functional validation of today's microprocessors. We also plan to perform further comparative studies with our functional coverage metric against existing coverage measures, such as code coverage, FSM coverage and stuck-at coverage.

Figure 1 .

 1 Figure 1. A Structure Graph of a Simple Architecture

Algorithm 2 :

 2 Test Generation for Operation Execution Input: Graph model of the architecture G. Output: Test programs for detecting faults in operation execution. begin /*** TestProgramList = {} ***/ for each operation oper in architecture G test prog oper = createTestProgram(oper);

	TestProgramList = TestProgramList ∪ test prog oper ;
	endfor
	return TestProgramList.
	end

Algorithm 3 :

 3 Test Generation for Execution Path Input: Graph model of the architecture G. Output: Test programs for detecting faults in execution path.

	TestProgramList = TestProgramList ∪ test prog oper ;
	endfor
	endfor
	endfor
	endfor
	return TestProgramList.
	end

begin /*** TestProgramList = {} ***/ for each pipeline path path in architecture G opgroup path = operations supported in path. exec path = path and all data-transfer paths connected to it oper path = randomly select an operation from opgroup path if (oper path activates all edges in exec path ) ops path = oper path else ops path = opgroup path endif for all operations oper in ops path for all source/destination operands opnd of oper for all possible register values val of opnd newOper = assign val to opnd of oper. test prog oper = createTestProgram(newOper).

Algorithm 4 :

 4 Test Generation for Pipeline Execution Input: Graph model of the architecture G. Output: Test programs for detecting faults in pipeline execution. begin /*** TestProgramList = {} ***/ L1: for each unit node unit in architecture G L2: for each exception exon possible in unit template exon = template for exception exon test prog unit = createTestProgram(template exon ); TestProgramList = TestProgramList ∪ test prog unit ; endfor L3: for each hazard haz in {RAW, WAW, WAR, control} template haz = template for hazard haz if haz is possible in unit test prog unit = createTestProgram(template haz ); TestProgramList = TestProgramList ∪ test prog unit ; endif endfor L4: for each parent unit parent of unit oper parent = an operation supported by parent resultOps = createTestProgram(oper parent ); test prog unit = a test program to stall unit (if exists) test prog parent = resultOps ∪ test prog unit TestProgramList = TestProgramList ∪ test prog parent ; endfor endfor L5: for each ordered n-tuple (unit 1 , unit 2 , ..., unit n ) in graph G prog 1 = a test program for creating exception in unit 1 ..... prog

n = a test program for creating exception in unit n test prog tuple = composeTestProgram(prog 1 ∪ ... ∪ prog n ); TestProgramList = TestProgramList ∪ test prog tuple ; endfor return TestProgramList. end

Table 1

 1 shows the comparative results for the DLX architecture. The rows indicate the fault models, and the columns indicate test generation techniques. An entry in the table has two numbers. The first one represents the minimum number of test programs generated by that test generation technique for that fault model. The second number (in parenthesis) represents the functional coverage obtained by the generated test programs for that fault model.

Table 1 . Test Programs for Validation of DLX Architecture

 1

	Fault Models	Test Generation Techniques
		Random	Constrained	Our Approach
	Register Read/Write	3900 (100%)	750 (100%)	130 (100%)
	Operation Execution	437 (100%)	443 (100%)	182 (100%)
	Execution Path	12627 (100%)	1126 (100%)	320 (100%)
	Pipeline Execution	30000 (25%)	30000 (30%)	626 (100%)

Table 2 . Quality of the Proposed Functional Fault Model

 2

	Fault Models	Test Programs	HDL Code Coverage
	Register Read/Write	130	85%
	Operation Execution	182	91%
	Execution Path	320	86%
	Pipeline Execution	626	100%

Table 3 . Test Programs for Validation of LEON2 Processor

 3

	Fault Models	Test Generation Techniques
		Random	Constrained	Our Approach
	Register Read/Write	1746 (100%)	654 (100%)	130 (100%)
	Operation Execution	416 (100%)	467 (100%)	212 (100%)
	Execution Path	1500 (100%)	475 (100%)	192 (100%)
	Pipeline Execution	30000 (40%)	30000 (50%)	248 (100%)

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)

In this paper we use the terms operation and instruction interchangeably. Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $

[START_REF]LEON2 Processor[END_REF].00 IEEE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

* This work was partially supported by NSF grants: CCR-0203813 and CCR-0205712.


Hossein M Sheini

Karem A Sakallah

A Modern Pseudo-Boolean SAT Solver

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Modern backtrack search SAT solvers augment the basic DPLL procedure with powerful conflict-based learning [START_REF] Marques-Silva | GRASP: a search algorithm for propositional satisfiability[END_REF] and efficient Boolean Constraint Propagation schemes [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF].

The closely-related 0-1 integer programming (IP) problem has also been studied extensively. In particular, the extension of SAT techniques to systems of CNF and socalled pseudo Boolean (PB) constraints was addressed in [START_REF] Aloul | Generic ILP versus specialized 0-1 ILP: An Update[END_REF]. Algorithms that combine the logic-based reasoning techniques of CNF SAT and the constraint relaxation and polyhedral analysis ("cutting planes") methods of IP were also explored with some success in [START_REF] Chai | A Fast Pseudo-Boolean Constraint Solver[END_REF].

In this paper we introduce Pueblo, a new CNF/PB SAT solver that integrates logic-based reasoning and new techniques to handle systems of CNF and PB constraints. Pueblo incorporates a novel watched-literal strategy and features several learning strategies including two that combine conflict-based CNF learning and cutting plane PB learning.

After covering some preliminaries, in Section 3 we describe our PB propagation method. Section 4 details various PB learning strategies. Experimental results are reported in Section 5. Conclusions and future work are presented in Section 6.

Preliminaries

A linear pseudo-Boolean (PB) constraint is said to be in normal form when expressed as:

(1) where denotes or . A PB constraint in which some coefficients are negative can be transformed to normal form by noting that . In general, a PB constraint is equivalent to a large, potentially exponential, number of CNF clauses [START_REF] Aloul | Generic ILP versus specialized 0-1 ILP: An Update[END_REF]. When the right-hand side and all left-hand side coefficients are equal to 1, however, a PB constraint is equivalent to a single CNF clause.

Pseudo-Boolean Propagation

In [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF] it was shown that watching just two literals per clause, regardless of clause size, is sufficient to detect when the clause becomes unit. The watched-literal concept was extended in [START_REF] Chai | A Fast Pseudo-Boolean Constraint Solver[END_REF] to handle PB constraints. The basic idea is to watch the fewest number of non-false literals such that when the unassigned watched literal with the largest coefficient is set to false a) the constraint is still guaranteed to be satisfied and b) the constraint can identify the literals that must now be implied to true. Specifically, let T and U denote the sets of true and unassigned literals in the constraint, and let denote the set of watched literals. We will refer to W as the watch list and to the sum of coefficients of the watched literals as the watched sum, i.e.,

We also introduce defined as:

The invariant that must be maintained to detect when the PB constraint becomes unit can now be succinctly expressed as:

. When a watched literal is set to false, it must be removed from the watch list and replaced by one or more non-false literals to maintain the above invariant. When that is no longer possible, the constraint becomes unit and any unassigned watched literal whose coefficient a satisfies the unit constraint condition must now be implied to true.

Empirical evaluation of this procedure suggests that about two thirds of its run time is spent in updating and corroborates the conclusion in [START_REF] Chai | A Fast Pseudo-Boolean Constraint Solver[END_REF] that the "watching scheme is beneficial for clauses and cardinality constraints, but not for LPB constraints; therefore we use counters to implement Boolean constraint propagation on LPB constraints." In other words, PB constraints are processed using a Watch All Literals strategy similar to that of PBS [START_REF] Aloul | Generic ILP versus specialized 0-1 ILP: An Update[END_REF].

Further analysis of the data, however, suggests a potentially more efficient hybrid watching strategy that differentiates between the literals with unit-and non-unit coefficients in the same PB constraint. Specifically, let L denote the set of literals whose coefficients are greater than 1 (the large literals) and let C denote those literals whose coefficients are equal to 1 (the cheap literals). Much of propagation time can be eliminated by applying the above procedure only to the literals in the (relatively small) L set. To achieve this, the computation of is modified to and if . Furthermore, the watch list W is modified to always include all of the literals in C. This modification requires a slight change to the manner in which the watched sum is calculated since the watched literals are no longer guaranteed to be true or unassigned. Specifically, the watched sum must now be decremented by 1 when a C literal is set to false, and incremented by 1 when a C literal is unassigned from false.

Pseudo-Boolean Learning

Generating and recording a so-called conflict-induced clause [START_REF] Marques-Silva | GRASP: a search algorithm for propositional satisfiability[END_REF], enables the solver to prune away a portion of the search 1 , , { 0 ,1 }

n i i i i i a x b a b x + = i x i x i x 1 i i x x = W T U i i W x W S a = max a max max{ } i i a a x U = max W S b a + W a S b > max a max a max max{ } i i a a x L U = max 1 a = L U =
Pueblo: A Modern Pseudo-Boolean SAT Solver

Hossein M. Sheini and Karem A. Sakallah Department of Electrical Engineering and Computer Science

University of Michigan Ann Arbor, MI 48109-2122 {hsheini, karem}@eecs.umich.edu space thus avoiding a recurrence of the same conflict. We will refer to this style of learning as CNF learning. An alternative approach, referred to as PB learning in this paper, based on cutting plane methods [START_REF]Edmonds Polytopes and a Hierarchy of Combinatorial Problems[END_REF], can be used to create a conflictinduced PB constraint instead. For details of this method, the readers are referred to [START_REF] Chai | A Fast Pseudo-Boolean Constraint Solver[END_REF].

Since PB constraints are generally more expressive than CNF clauses, a learned PB constraint has the potential of pruning more of the search space than a CNF clause. However, the steep overhead of manipulating PB constraints can more than offset their pruning benefits. (the high cost of unlimited PB learning and propagation is shown in Figure 1). Thus, an adaptive approach that combines CNF and PB learning, and introduces PB constraints selectively, might be superior to either approach alone. We describe next two variations on this theme. Scheme 1: Learn Strong PB Constraints. In this scheme, after detecting a conflict, both CNF and PB Learning procedures are followed simultaneously. A PB constraint is learned and recorded instead of a CNF clause if and only if all the following three conditions hold: 1. it is unit; it could be the case that the cutting plane generated from two constraints (conflicting and implying constraints) is not in conflict anymore due to over-satisfaction of the implying constraint. 2. it corresponds to more than just a single CNF clause; 3. the number of its large literals (those in the L set) is less than a given threshold; Scheme 2: Convert Learned PB Constraint to CNF. In this scheme, the learned PB constraint is recorded but not used in BCP. Rather, it is viewed as a compact representation of a set of CNF clauses, subsets of which can be extracted as needed during the search. Extraction of suitable CNF clauses from the PB constraint is carried out using a simple knapsack algorithm. The rationale for this scheme is to capitalize on the pruning power of the learned PB constraint without incurring its high propagation overhead. For instance, learning where and are false at the backtrack level, will result in learning the following clauses:

The first two clauses are unit and would result in the same implications as the original PB constraint. The PB constraint, on the other hand, is kept aside and retouched later during the search to extract other CNF clauses which could be more useful based on the variable assignments in effect at that time.

Experimental Results

We conducted several experiments to evaluate the strategies described above using Pueblo. Pueblo is built on top of Mini-SAT [START_REF] Eén | An Extensible SAT-solver[END_REF] and extends its VSIDS decision heuristic and its clause removal mechanism to PB constraints. It also adopts hybrid propagation strategy as explained earlier. All experiments were conducted on Pentium-IV 2.8GHz -1GB of RAM.

Table 1 depicts a comparison of Pueblo and galena [START_REF] Chai | A Fast Pseudo-Boolean Constraint Solver[END_REF] PB learning strategies on a set of benchmarks including the Routing instances of [START_REF] Aloul | Generic ILP versus specialized 0-1 ILP: An Update[END_REF]. Overall, scheme 1 performs robustly and compares favorably to the cardinality strategy of galena. All these methods perform much better than CNF learning in these types of problems. In these benchmarks, due to large number of unit-coefficient variables, the positive effects of the hybrid propagation strategy is more evident.

Conclusions and Future Work

As we learn more about the trade-offs involved in combining logic-based reasoning and IP methods, we will be able to develop effective integration strategies that outperform individual techniques. The concepts described in this paper do not exhaust all the possibilities for taking advantage of the pruning power of PB constraints while minimizing their computational overhead. Other ways of generating cutting planes, for example, that are provably superior to current approaches should be investigated.

Figure 1 :

 1 Figure 1: Effect of PB learning on number of decisions and run-time with a restriction on the maximum allowable number of learned PB constraints (X-axis) in s4-3-2pb [1].

Table 1 : Different PB learning strategies

 1

						Time (sec)
				Benchmark	Pueblo	Galena
					CNF	Sch. 1	Card.	LPB
				s4-3-2pb (SAT)	4.78	0.57	0.50	0.70
				s4-3-3pb (SAT)	3.35	0.64	0.50	0.70
				s4-3-4pb (SAT)	2.54	0.05	0.60	1.70
				s4-3-5pb (SAT)	3.12	0.73	0.80	0.15
				fpga11_9 (SAT)	41.19	0.09 43.39	>1000
				fpga12_14 (UNS) >1000	0	0.10	0
				fpga15_10 (SAT) >1000	7.45 >1000	85.40
				fpga15_14 (SAT) >1000	0.02	0.37	1.14
	6x 1 5x 2 4x 3 3x 4 2x 5 2x 6 + + + + +	12	x 2	x 4

x 1 x 2 + x 2 x 3 x 4 + + x 2 x 4 x 5 x 6 + + + , ,

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Acknowledgment

This work was funded in part by the National Science Foundation under ITR grant No. 0205288.


Tong Wang

The structures of particles traveling at the speed of light

In his seminal paper [START_REF] Einstein | Does the inertia of a body depend upon its energy-content?[END_REF] , Einstein proposed a relationship between mass and energy, transcribed below:

E√(1 -𝑣 2 /𝑐 2 )

If a particle with "ordinary" mass moves at the speed of light c, then the expression inside the radical on the left side of the equation (1 -𝑣 2 /𝑐 2 ) is zero. We also know that the particle's energy E is finite, so the left side of the equation must equal zero. If this is true, then the right side of the equation (mc [START_REF] Luttinger | On "Negative" mass in the theory of gravitation[END_REF] ) must equal zero as well. Since the speed of light c is finite, it follows that the particle's mass must be zero, and therefore we consider the particle to be massless.

However, if we consider a proposal that the particle consists of equal quantities of both mass and negative mass 23 , then it is possible that the net mass on the right side of the equation is still zero, and that the particle is in all other respects still considered massless.

According to the equivalence principle of general relativity we can deduce four fundamental attributes of negative mass (Bondi). They are important in later arguments and are listed below:

Attribute 1: Negative mass repels negative mass-i.e. negative masses move away from each other.

Attribute 2: Negative mass repels mass.

Attribute 3: Mass attracts negative mass-i.e. negative mass moves toward mass.

Attribute 4: Negative mass generates a gravitational field similar to that of mass, but with the opposite sign.

From Attribute 1 it can be deduced that a plural quantity of negative masses is unstable if no other forces bind them together. However the smallest unit of negative mass is stable (the unit will be referred to as a Yinon in this essay).

In Let us suppose that there exists a unit of "ordinary" mass that has an inertial mass equal to that of a yinon (the unit will be referred to as a Masson in this essay).

Because the inertial masses of a yinon and a masson cancel each other out exactly, if one considers a photon to consist of an equal number of yinons and massons, then the combination as a whole does not exhibit net inertial mass (in other words, it is observed to be massless). However, we do observe seemingly massless light being bent by large astronomical bodies, and this can be explained by the fact that both yinons and massons inside photons move toward mass (Attribute 3).

An existing explanation states that a photon's relativistic mass is responsible for the fact that light can be bent by gravity. However, upon further examination, this theory seems to be flawed. Specifically, because it can be concluded that there would be attraction between the photons making up light, those photons would eventually move toward each other. We should then observe a stream of light consolidate to form a giant photon after light has travelled through galaxies for many years. In reality, however, we have yet to observe this. For instance, assuming two red wavelength photons with relativistic mass 2.9 * 10 -36 kg are separated by 10 -9 m, then within 1.6 * 10 9 seconds the two red photons would collide with each other. This means that clumping, and the eventual formation of giant photons, would occur under this theory.

An alternative explanation, proposed by this essay, is that the relativistic mass is not responsible for light being bent by gravity, but rather that the yinons and massons making up a photon move toward the gravity sources. Thus, it is the combination of mass and negative mass that causes light to appear to be bent by gravity. Additionally, in this model, the photons will not collapse in on each other, which was the flaw in the existing explanation. This is because we can deduce from Attribute 4 that the active gravitational mass of the photon is zero because the gravitational fields of the yinons and the massons cancel each other out exactly. To see why this is the case, let d denote the diameter of the effective gravitational field of photon A. Let another photon B be placed at a distance ab from the photon A. If ab >> d then there is no gravitational attraction or repulsion between A and B, implying that the two photons A and B are in equilibrium. Therefore, in general, all photons inside a stream of light are in equilibrium.

A luxon is defined as a massless particle travelling at the speed of light. Suppose we have a luxon that consists of an equal number of yinons and massons. Based on this assumption, various stable configurations can be obtained. We do not consider a configuration to be stable if yinons or massons inside the configuration move away forever from their original locations. In Fig. 1, if the mass is a masson and the negative mass is a yinon then the configuration is not considered stable-the pair will move together forever and in the direction of the yinon toward the masson (Luttinger). In Fig. 2, a yinon rotates around a masson. This configuration is not considered stable because the pair will spiral outward from its original location. In the following paragraphs we will develop some stable configurations of luxons:

(1) Two yinons and two massons stick together in a line Fig. 3 shows two yinons and two massons stuck together in a line. There are four distinct ways these yinons and massons can be arranged in a line. Only the alignment of yinon-massonmasson-yinon is in equilibrium. Since the attraction on one outer yinon generated by the center massons is greater than the repulsion exerted on the same yinon by the other outer yinon, the yinons do not move away from the center massons (which also attract each other). We consider this configuration to be stable and thus a possible structure of a luxon. (3) Luxons consist of yinons and a charged mass Fig. 5 shows another structure of a luxon. If n massons can make up a mass and the mass can carry an electric charge, then a luxon can consist of n yinons and the mass. In this configuration, the luxon can have an electric charge but still be considered massless. Therefore, one can see that if we accept the existence of luxon structures consisting of mass and negative mass, there are many remarkable implications.

Fig. 1 ,

 1 let a particle A (blue) have a mass m a , and a particle B (green) have a negative mass -m b . Let r be the distance between A and B. The force exerted on B by A is F = G • -m b • 𝑚 𝑎 𝑟 2 , and points from A to B. However, the acceleration of B is a = G • 𝑚 𝑎 𝑟 2 , and points from B to A. According to Luttinger's analysis, if m a > m b , then B (negative mass) will move toward A (mass).

Fig. 1 A

 1 Fig.1 A negative mass moves toward a mass

Fig. 2 A

 2 Fig.2 A yinon rotates around a masson in a plane

Fig. 3 2 𝑑.

 32 Fig.3 Two yinons and two massons stick together in a straight line

Fig. 4

 4 Fig.4 Two yinons rotate around two massons in a plane

Fig. 5 n- 2 .

 52 Fig.5 n yinons rotate around a charged mass


Jacob Katz
email: jacob.katz@intel.com

Ziyad Hanna
email: ziyad.hanna@intel.com

Nachum Dershowitz
email: nachum.dershowitz@cs.tau.ac.il

Space-Efficient Bounded Model Checking

whether they are published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction *

Model checking is a technique for the verification of the correctness of a finite-state system with respect to a desired behavior. Symbolic model checking uses image computation to verify properties. Symbolic model checking methods include, among others, BDD-based techniques, SAT-based methods for image computation that use an explicit quantifier elimination, and SAT-based reachability analysis based on "all-solutions" SAT solvers. All these methods suffer from the memory explosion problem on modern test cases.

Bounded Model Checking (BMC) with a specific bound k represents the paths of length k in the system by "unrolling" the transition relation k times, and examines whether the set of states falsifying the property is reached by these paths. To implement a complete model checking procedure the bound should be increased iteratively up to the length of the longest simple path in the system, causing the number of copies of the transition relation within the formulae being checked for validity to increase from iteration to iteration up to an exponential number of times, * Due to space constraints references have been omitted in this text. leading, again, to a memory explosion for large systems and large bounds.

Induction based methods provide another technique for estimating whether a bound is sufficient to ensure a full proof, but there are still many cases where the induction depth is exponential in the size of the model.

Finally, the methods based on Craig interpolation as an over-approximation technique for image computation aimed at reducing the number of iterations for a complete model checking procedure. The interpolants are obtained as a by-product of the SAT solver used to check BMC problems. This technique, like other techniques based on image computation, also suffers from a potential memory blow-up.

In this paper we present a short abstract of our research on the usage of Quantified Boolean Formulae (QBF) for BMC, in which the unrolling of the transition relation is not performed and, thus, the memory explosion problem is avoided. We evaluate available general-purpose QBF solvers, and develop a special-purpose decision procedure for QBF used in BMC. We also compare our technique with the classical SAT-based BMC methods.

Formulations of bounded reachability checking problem

Given a system M=(S, I, TR), where S is the set of states, I is the characteristic function of the set of the initial states, and TR is the transition relation, the problem of reachability of the final states given by a characteristic function F in exactly k steps can be expressed in a number of ways.

As in classical BMC, the fact that the state Z k is reachable from the state Z 0 in exactly k steps may be formulated by "unrolling" the transition relation k times:

(1)

0 1 1 0 1 1 0 ( , ) ,..., : ( ) ( ) ( , ) k k k k i i k i R Z Z Z Z I Z F Z TR Z Z
The validity of this formula may be proven or disproved by performing the SAT decision procedure on its propositional part. Noticeably, the number of copies of the transition relation in this formula is as the number of steps being checked. To partially overcome the potential memory explosion, a QBF formulation of bounded reachability problem can be used:

(2)

0 1 1 0 1 1 0 ( , ) ,..., : ( ) ( ) , : ( ) ( ) ( , ) k k k k i i k i R Z Z Z Z I Z F Z U V U Z V Z TR U V
Note that (2) contains only one copy of the transition relation. Increasing the bound, thus, would mean an addition of a new intermediate state and a term of the form (U Z i ) (V Z i+1 ). Hence, the formula increase from iteration to iteration does not depend on the size of the transition relation, which is usually the biggest formula in the specification of the model.

The solution of (2) with a QBF solver usually requires a transformation of the propositional part of the formula into a CNF, which introduces artificial variables, resulting with a QBF having pattern of the quantifier prefix. The number of the universally quantified variables does not change in the QBF from iteration to iteration.

This approach to reachability checking partially solves the issue of formula growth, reducing the growth of the formula from iteration to iteration, but still requires an exponential number of iterations to fully verify the reachability.

To reduce the number of iterations, it is possible to apply the "iterative squaring" technique, similar to the one used in BDD-based model checking. In this technique, each successive iteration checks the reachability of a final state in twice as many steps as the previous iteration. Given a formula R k/2 (X,Y) for checking reachability in k/2 steps, the following formula checks the reachability in k steps:

(3)

0 0 0 / 2 ( , ) : ( ) ( ) , : ( ) ( ) ( ) ( ) ( , ) k k k k k R Z Z Z I Z F Z UV U Z V Z U Z V Z R UV
The transition relation appears in (3) only once, as in the previously described technique. However, the number of universally quantified variables and the number of quantifier alternations grows from iteration to iteration.

This technique allows reducing the number of iterations to be as the number of the state encoding variables in the model. Note that not all bounds are checked by this technique, but only the bounds that are a power of 2. It is possible, however, to overcome this problem by adding a self-loop in each state of the model, which would not change the reachability between states, but rather make (3) check reachability in k or fewer steps, instead of exactly k steps.

BMC using QBF

We have used a bounded model checker to generate the three kinds of formulae mentioned in the previous section. We have evaluated a few available state-of-the-art DPLLbased SAT and QBF solvers, to check the feasibility of the QBF formulations of the reachability checking problem on a set of thirteen proprietary Intel® model checking test cases of different sizes. It appeared that the general-purpose QBF solvers were unable to solve practically any of the formulae of the forms (2) and (3), while many of the corresponding propositional formulae of the form (1) were solved by the SAT solvers, the majority of them in a matter of seconds.

Motivated by the inefficiency of the general-purpose QBF solvers demonstrated on formulae of the form (2), we develop a special-purpose DPLL-based decision procedure, called jSAT, for formulae of this specific structure. As in (2), jSAT holds in memory the encoding variables representing the states Z 0 , Z 1 , …, Z k , U and V, but only holds the following propositional formula:

(4) 0 ( ) ( , ) ( ) k I Z TRU V F Z
The states Z i represent a path; the states U and V represent two neighboring states in that path. Instead of explicitly holding the fact that U and V represent a pair of neighboring states as done in (2) with assistance of the terms of the form (U Z i ) (V Z i+1 ), our algorithm implicitly assumes this information. The idea of the algorithm is to iteratively associate U and V with a pair of successive states, called the current state and the next state, until all states are decided.

Intuitively, jSAT algorithm can be seen as a depth-first search in the state graph of the system from the initial states to the final ones. The algorithm starts by associating U with Z 0 and V with Z 1 ; thus the formula (4) becomes semantically equivalent to:

(5)

0 0 1 ( ) ( , ) ( ) k I Z TR Z Z F Z
The states Z 0 and Z 1 are then decided, if possible, so that Z 0 is an initial state and Z 1 is its successor. As soon as they are decided, the algorithm makes Z 1 to be the current state and Z 2 to be the next one. The algorithm proceeds so on, until all states are successfully decided, or until it discovers that such a decision is impossible.

The first implementation of our algorithm succeeded to solve 143 out of 234 instances of the form (2) in our test base, compared to 184 corresponding SAT instances solved by the solver on which we based our implementation, and 3 instances solved by the general purpose QBF solvers, within 300 seconds time limit and 1GB memory limit.

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE


Tim Schattkowsky

Wolfgang Mueller

Achim Rettberg

A Model-Based Approach for Executable Specifications on Reconfigurable Hardware

UML 2.0 provides a rich set of diagrams for systems documentation and specification. Many efforts have been undertaken to employ different aspects of UML for multiple domains, mainly in the area of software systems. Considering the area of electronic design automation, however, we currently see only very few approaches, which investigate UML for hardware design and hardware/software co-design. In this article, we present an approach for executable UML closing the gap from system specification to its model-based execution on reconfigurable hardware. For this purpose, we present our Abstract Execution Platform (AEP), which is based on a Virtual Machine running an executable UML subset for embedded software and reconfigurable hardware. This subset combines UML 2.0 Class, StateMachine and Sequence Diagrams for complete system specification. We describe how these binary encoded UML specifications can be directly executed and give the implementation of such a virtual machine on a Virtex II FPGA. Finally, we present evaluation results comparing the AEP implementation with C code on a C167 microcontroller.

Introduction

We currently can identify multiple gaps in the design of embedded and electronic systems, from specification to a first implementation. In current practice, all approaches follow a platform-specific code generation. For most tools, various code generator targets are available for different microcontrollers such as C167 and different Real-Time Operating Systems (RTOSs) like OSEK [START_REF] Marwedel | Embedded Systems Design[END_REF]. There have been many efforts to investigate retargetable compilers to easily adopt them to different hardware platforms [START_REF] Leupers | Retargetable Compiler Technology for Embedded Systems[END_REF].

Most recently, the MDA approach (Model-Driven Architecture) [START_REF]The Object Management Group: Model Driven Architecture (MDA)[END_REF] became well recognized in the domain of embedded software and hardware systems. MDA is based on the idea of platform-independent development with platform-independent models (PIMs). PIMs have to be mapped to platform-specific models (PSMs), which are used for the actual implementation. In that context, the notion of Executable UML plays a significant role, as it enables a UML-based PSM to become executable.

We introduce a novel approach to efficiently execute specifications on FPGAs. The specifications are defined by an UML 2.0 subset with precise behavioral semantics executing on our Abstract Execution Platform (AEP). Our UML subset covers Classes, StateMachines, and Interactions (given as Sequence Diagrams) with software exceptions, interrupts, and timeouts. We apply a virtual machine concept to implement the AEP on a FPGA. The AEP virtual machine directly executes binary encoded specifications, which resemble the object-oriented structure of the UML specification and combine efficient execution of state-transition tables with Activities, and Actions compiled to a Motorola 68K-like bytecode with object-oriented extensions.

The remainder of this paper is structured as follows. The next section discusses related works. Section 3 introduces the UML subset defining syntax and semantics for AEP specifications. Section 4 presents the concept of direct execution of specifications on a virtual machine. Section 5 introduces our implementation on a FPGA before Section 6 closes with summary and conclusion.

Related Works

Based on Starr's approach to executable UML [START_REF] Starr | Executable UML How to Build Class Models[END_REF], which is mainly based on class and state diagrams, Project Technology developed X T UML [12] as an executable and translatable UML subset for embedded real-time systems in the areas of flight-critical systems, performance-critical fault-tolerant telecom systems, and resource-constrained consumer electronics. Their Nucleus Modeling tools basically integrate abstract, macro-like constructs, which are easily retargetable to the various C-dialects of different microcontroller platforms. A second approach to executable UML is xUML [START_REF] Raistrick | Model Driven Architecture with Executable UML[END_REF], which also includes a complete development methodology. The concept of xUML is based on the Action Specification Language (ASL), which defines the behavioral semantics of active objects for code generation. ASL has been integrated into the OMG-adopted UML Standard for precise action semantics [START_REF]The Object Management Group: Action Semantics for the UML[END_REF]. However, for creating an executable model, xUML still relies on a programming languagespecific code generation (e.g., for Ada, C, C++).

In the area of platform independent execution, the most prominent approaches to portable code are the UCSD Pascal p-Code and the bytecode of the Java Virtual Machine [START_REF] Lindholm | Java Virtual Machine Specification[END_REF]. The Java compiler generates low-level bytecode, which is executed on a Java Virtual Machine (VM). Though Java was originally designed for embedded systems, due to the large footprint of its runtime environment and the garbage collection memory management, the Java2 Standard Edition is not suited for small microcontrollers and real-time applications. Though, there exist Java profiles of the Java2 Micro Edition for limited devices like the CLDC (Connected Limited Device Configuration) and the CDC (Connected Device Configuration), we currently see no VM implementations for microcontrollers and no support for Real-Time Java for those platforms.. Considering execution on FPGAs, the Hardware Virtual Machine project targets at the specification of an abstract FPGA to overcome the problem of incompatible bit files. Designs for abstract FPGAs are automatically transformed into a bit file for a specific FPGA. The transformation is based on an automated creation of the design for the target FPGA from small fragments, which are then subject to place and route.

Lange and Kebschull introduce the idea of a virtual machine for abstracting hardware implementations from particular FPGA types [START_REF] Lange | Virtual Hardware Byte Code as a Design Platform for Reconfigurable Embedded Systems[END_REF]. The approach is based on the execution of a binary encoded register transfer level description of the logic that is referred to as bytecode. The bytecode is composed of blocks of instructions that are scheduled into multiple equal execution units within the actual virtual machine implementation. This virtual machine implementation is specific for a particular FPGA and may vary in the number of execution units. However, their bytecode describes low level hardware designs comparable with a direct FPGA implementation. High level constructs like control structures are not supported.

Our approach presents a runtime environment for FPGAs, which directly executes the binary representation of a platform independent UML specification. In contrast to other approaches, our concepts implement a completely model-based approach for the specification of real-time systems covering interrupts and timeouts. In contrast, to the Java Virtual Machine, we provide explicit separation of concerns by integrating StateMachines and Sequence Diagrams into one language. Hereby, the user has explicit control on the use of efficiently running control-oriented StateMachine and data-oriented Sequence Diagrams. Additionally, our approach supports object-orientation at the bytecode level, where the Java compiler elaborates the object-oriented constructs before the bytecode generation. To our knowledge, our work presents the first real modelbased approach, which generates binaries from UML for FPGA runtime environments.

Executing UML Models

Our approach is based on the concept of the Abstract Execution Platform (AEP). The AEP provides syntax and semantics for complete system specification based on a well-defined executable UML subset with precise execution semantics. Actual implementations of the AEP may apply inherently different techniques to implement the AEP semantics. Section 4 describes our AEP implementation given by a virtual machine on an FPGA. However, the AEP can also be implement as a complete software solution, e.g., on embedded microcontrollers.

The behavioral part of the UML is based on the concepts of StateMachines, Activities, and Interactions. StateMachines invoke Activities when executing states or state transitions as Entry, Do, Exit, or Effect Activities, which in turn are composed of Actions. Transitions of StateMachines fire when an event occurs. Interactions are based on the concepts of partially ordered traces and are represented by Sequence Diagrams.

Our concepts for executable UML are based on a UML 2.0 subset covering Class-, StateMachine-, and Sequence Diagrams. System specification is based on the definition of a Class Diagram with classes, their properties, and their operations. In contrast to other approaches, we consider each operation as a StateMachine and use Sequence Diagrams as an action language for describing the Activities. Note that the case of a trivial StateMachine (i.e., a single state with a single Activity) equals to the use of Sequence Diagrams for the definition of an operation.

We support StateMachines with composite and simple states. Concurrent States are intentionally not supported, because concurrency is already supported through asynchronous operations that may be described by StateMachines. For events, we support timeout, interrupts, exceptions, explicit events, and the completion of the embedded Activities/Actions. Fig. 1 gives a simple controller with interrupts and timeouts as an example. Interactions are embedded as Activities and have one active object representing the currently activated instance. The Activity is described by the sequence of outgoing invocations from that active object. An example is given in Fig. 3 and will be further discussed in the next section. Asynchronous operation calls are instantiations of StateMachines. This leads to a dynamic composition of multiple concurrent hierarchical StateMachines along the operation call hierarchy. Thus, state-and control-oriented modeling can be seamlessly combined following a fully object-oriented reactive concurrent system designs.

The AEP Virtual Machine

Our UML specifications are compiled to equivalent binary representations, which are directly executed on our Abstract Execution Platform (AEP). The AEP is realized as a virtual machine that can be implemented on different platforms, e.g., completely in software or directly in hardware on an FPGA.

In their binary specifications, StateMachines are encoded as binary state-transition tables, which we denote as Executable State Machines (ESMs). Interactions defining Activities are compiled into equivalent UML bytecode.

Fig. 2: AEP Virtual Machine -Architecture

The AEP virtual machine consists of the Model Execution Unit (MEU) and the Runtime Kernel (RK) as given in Fig. 2. The RK is an executable specification that on the hand is used for bootstrapping including initialization of the initial executable specification and on the other hand implements memory management, thread scheduling. The RK is executed by the MEU, which is composed of two interacting interpreters for the different parts of the binary UML representation; one for the Executable StateMachines (ESM) and another one for the Bytecode. A separate timer manages hard timeouts.

The ESM Interpreter performs immediate state transitions when events occur. Currently, five pre-defined events are supported: Completion, Interrupt, Timeout, Division-by-Zero, and Memory-Overflow. When a state is entered or a transition executed, the interpreter first checks, if an Activity in form of an Interaction with bytecode is defined. If there is bytecode in the embedded Activity, the bytecode interpreter is invoked. A generated bytecode sequence typically finishes with a COMPLETE instruction, which generates a completion event. If no Activity is defined or when the final state is reached, an immediate completion event is generated.

The Bytecode Interpreter executes the Bytecode in a microprocessor-like manner using an instruction pointer and a 32 bit word stack for program control. To provide a hardware-independent execution platform, the interpreter has no registers. All variables are managed on the stack.

Our UML bytecode is based on a instruction set derived from the Motorola 68K family [START_REF]M68000 Family Programmer's Reference Manual[END_REF], which is extended for the control of the ESM interpreter and the handling of classes and their instances (cf. Table 1).

Classes and interfaces are identified in our approach at runtime using unique identifiers. This allows late binding and lays the foundation for a software component architecture based on our approach like in COM [START_REF]The Component Object Model Specification[END_REF].

Each class is a single block of binary data in memory. It essentially consists of the unique class identifier (the CLASSID), a function table for the implemented operations, an absolute pointer to the base class in memory (if any), and a reference to the linked list of implemented interfaces. Each of the interfaces, like the class itself, has a table with references to the actual method implementations. All absolute references are resolved by the RK class loader when loading a class.

Because static class attributes are private in our approach, subclasses must use operations to access inherited attributes. Thus, there is no need to distinguish between local and inherited attributes, which in turn simplifies the address management. The attributes are trailing to the actual base address of the class to enable consistent access to the operation table of a class and its subclasses. Much like a C++ vtable (virtual function table), this table grows in subclasses when appending subclass operations. It is worth noting here, that in our approach, all non-private operations are technically virtual and can be overridden in subclasses. Private operations are directly resolved by the bytecode compiler and compiled into subroutines of the bytecode. Thus, these operations are not represented in those tables.

The table for each class includes three basic operations. These are the base constructor for filling the fields of an instance and two operations for initializing and finalizing the class when it is loaded or unloaded.

There is no need for code relocation in our approach, since the bytecode for an operation contains only relative branches. Thus, the code is completely relative except for operation invocations. Absolute instance and class references are used for such invocations, but are obtained during runtime.

Our bytecode introduces instructions to support object instantiation and destruction as well as operation invocations. The NEW instruction creates a new object allocating dynamic memory for the instance. The DESTROY instruction releases dynamically allocated instance memory. INVOKE* and FORK/JOIN execute synchronous and asynchronous operation calls using an operation identifier (the actual offset in the operation table) and the instance or interface as parameters. Synchronization is implemented by the SYNC and RELEASE instructions for obtaining and releasing a mutex semaphore on an instance. The TRYSYNC instruction is a non-blocking variant of SYNC.

Three additional instructions provide explicit ESM control. The TRANS instruction performs an immediate transition to an explicitly given new state with all side effects. The EVENT instruction causes the ESM interpreter to process the event in the context of the current state hierarchy. COMPLETE causes the immediate execution of the completion transition for the current state.

Finally, the CONTINUE instruction explicitly changes the execution context to the specified thread. The state of the current thread is saved on the stack before the state of the new thread is restored from the stack. This new thread will be passed to the RK scheduler implementation for immediate schedule for execution.

A called operation uses the stack to create local variables and hold temporary values during nested computations. For this, the bytecode interpreter distinguishes three address spaces on the stack denoted as frames, which are created when invoking an operation (cf. Fig. 4). The Parameter Frame holds all input and output parameters. Output parameters are pushed on the stack with their default values. The Local Frame is for local variables and temporary data. Both frames have fixed sizes, which can be computed at compile time. The Pass Frame holds the designated parameters for a suboperation call. That frame is dynamically expanded when additional parameters are pushed on the stack. The pass frame becomes the parameter frame during the invocation of that suboperation. It is extended with data for restoring the current state upon return, a reference to the parent state and, for non-static invocations, the reference to the called this instance.

An additional local address space is provided for accessing local instance attributes. All instructions fetching and storing stack data refer to one of the three stack frames or this local address space. This guarantees full memory protection, but comes at the cost of a significant overhead in stack use during operation invocations as address and size of parameter and local frames have to be saved when invoking an operation.

UML Bytecode Example

To illustrate our UML bytecode, we briefly outline it by the example of the get(index) operation of a linked list. The StateMachine for the operation is given by a trivial StateMachine with a single state and a single Activity for the completion of the state. Fig. 3 gives the Activity as a Sequence Diagram. The get() operation searches the linked list up to the given index. This is defined by a loop CombinedFragment for iterating the list until the given index or the end of the list is reached. Then, the data attribute of the ListNode is returned. The bytecode for that operation is given by the following sequence and the corresponding stack is shown in Fig. 4. Note that the this reference on the stack is added together with the parent stack frames of the non-static invoke instruction. The corresponding complete operation restores the parent frames from the stack and discards the this reference by adjusting the stack pointer accordingly.

Fig. 4: Stack for a get(index) operation call

Evaluation Results

We have implemented a prototype of the AEP virtual machine using Handel-C on a Celoxica RC 200 evaluation board equipped with a Virtex II XC2V 1000-4. The virtual machine resides on the SmartMedia Card (SMC) and the binary encoded UML programs are loaded to the SRAM via the RS-232 interface. The current implementation runs with 35 MHz. However, this is just a limitation of the RC 200 board due to the SMC card without any implications for our concepts.

Our evaluation focused on the runtime of the bytecode interpreter, as it is essential for computations. We implemented five different UML examples and compared their runtimes with C implementations on a C167 with 20 MHz. These examples include a factorial calculation (fak), an adder-tree (tree), a Fibonacci calculation (fib), a butterfly node (butterfly) with 4 multipliers and two adders, and a matrix addition (mmadd).

All program data including stacks and dynamically allocated memory resides in the SRAM. Each instruction has to be fetched from SRAM during execution. The test results are summarized in Table 2. All tests were repeated 1000 times and the average is presented. During these tests, no anomalies (e.g., strong variance) where detected. In summary, our AEP prototype achieves a per-clock performance comparable to the C167 embedded microprocessor running C code. Considering the early stage of our prototype and the high-level modelbased design method applying UML specifications, we think that this is a considerable result. However, the above examples are small and make no significant use of deep call hierarchies and state machines. While this is still not crucial for many designs, it is necessary to further explore the performance of more complex ESM models.

Conclusions and Outlook

We have presented a novel approach for executable UML specifications on FPGAs. This approach is based on an executable UML subset with precise execution semantics given by our Abstract Execution Platform (AEP). We have introduced the concept of a virtual machine for executing binary representations of UML specifications. Our evaluation compared our executable specifications on FPGA with corresponding C implementations on a C167 microcontroller. This showed promising results considering that we start from a modelbased, platform independent object-oriented UML specification and directly execute it on a virtual machine.

However, the evaluation of more complex programs is still necessary. Furthermore, we plan to evaluate different memory management and scheduling implementations

Fig. 1 :

 1 Fig. 1: StateMachine Example

  Stack Instructions move.[b,l,d] mem mem/im Dst Src push.[b,l,d] mem [-sp] Dst pop.[b,l,d] mem Dst [sp+] enter imm (Initialize local frame) Math Instructions add.[b,l,d] mem mem/im Dst Dst + Src sub.[b,l,d] mem mem/im Dst Dst -Src neg.[b,l,d] mem Dst 0 -Dst mul.[l,d] mem mem/im Dst Dst * Src div.[l,d] mem mem/im Dst Dst / Src mod.[l,d] mem mem/im Dst Dst % Src cmp.[b,l,d] mem mem/im [Flags according] Logical Instructions not.[b,l,d] mem Dst ~Dst and.[b,l,d] mem mem/im Dst Dst Src or.[b,l,d] mem mem/im Dst Dst Src xor.[b,l,d] mem mem/im Dst Dst Src Shift Instructions asl.[b,l,d] mem mem/im Dst Dst << Src asr.[b,l,d] mem mem/im Dst Dst >> Src lsl.[b,l,d] mem mem/im Dst Dst <<< Src lsr.[b,l,d] mem mem/im Dst Dst

Fig. 3 :

 3 Fig. 3: get(index) operation for a linked list

Table 1 : AEP Bytecode Instruction Set

 1

	Current Instance	Attributes	Parameters	Local
	this :List	First :ListNode	Last :ListNode	Result :Obj ect	Local :ListNode

Table 2 : Bytecode on AEP vs. C on C167

 2

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)

Acknowledgements

We gratefully acknowledge the work of Alexander Krupp and Jörg Viermann for implementing the examples.