SOURCE ARCHIVE
EXTRACTED CONTENT
27,863 chars Specification-Driven Testbench Development for
Synchronous Parallel-Pipeline Designs
Mikhail Chupilko, Alexander Kamkin
Institute for System Programming of the Russian Academy of Sciences
25, A. Solzhenitsyn Street, Moscow, 109004, Russia
E-mail: {chupilko, kamkin}@ispras.ru
Abstract— In this paper an approach to testbench development tion IV the CTESK toolkit is briefly described. Section V is for synchronous parallel-pipeline designs is considered. The a case study. Section VI concludes the paper. approach is based on cycle-accurate formal specifications of a design under verification. Specifications include descriptions of II. RELATED WORK control flow graphs of the design’s operations and definitions of the microoperations with the help of Hoare triples. The There are a lot of research and industrial papers on approach allows to automate testbench development for complex semi-formal verification methods. This gives evidence that synchronous designs with control flow branching and parallel specification-driven testbench development is the promising starting operations. The important feature of the proposed direction for hardware verification. The main question is what method is that specifications are used to perform all tasks of kind of specifications and models are preferable. To automate functional testbenches: checking of design correctness, estimation of test completeness, and generation of test sequences. The different tasks of testing, distinct types of models are usually approach was successfully used in several industrial projects on used. For example, stimuli generation can be performed on hardware verification. the base of FSM models, while correctness checking can be I. INTRODUCTION done by means of temporal assertions. This has a certain disadvantage. Two models require maintenance during the Functional verification is a well-known bottleneck in hard- design process to keep up their mutual consistency. ware design process. Ensuring the functional correctness of The most of the papers are dedicated to the methods of hardware consumes about 70% of the design efforts [1]. The test sequence generation. Many of them suggest using explicit situation is only going to get worse as designs grow in size and cycle-accurate models to generate test sequence, e.g., Ur et complexity. There are two different approaches to checking al. [4] and Mishra et al. [5] use SMV models; Ho et al. [6] hardware: formal verification and simulation-based verification utilize Synchronous Murϕ. The main differences between [2]. It is known that formal methods are exhaustive but not the approaches are concentrated in the following methods: scalable, while simulation techniques are scalable but not ex- a method of model construction (manual development [4], haustive [3]. A good balance of exhaustiveness and scalability automatic derivation from an RTL description [6], and au- is provided by semi-formal methods, which combine formal tomatic derivation from specifications [5]) and a method of specifications (or models) and simulation. test sequence generation (FSM traversal [4], [6] and model In this work a semi-formal approach to testbench devel- checking [5]). opment is suggested. A testbench is an environment used to Manual development of a model is error-prone, while au- verify a design via simulation. A typical testbench has three tomatic derivation from an RTL description does not scale key components: a stimulus generator, a response checker, well on complex hardware designs. In our opinion, the most and a coverage tracker. The stimulus generator creates input promising method of model construction is automated extrac- stimuli to the design under verification. The response checker tion from formal specifications. Speaking about test gener- estimates the correctness of the design behavior. The cov- ation, model checking techniques are not intended for full- erage tracker evaluates the test completeness. The approach scale functional verification. They are aimed to verification of described in the paper automates construction of the testbench a relatively small number of properties. The most usable way components on the base of formal specifications. of test sequence generation is based on FSM traversal. The rest of the paper is organized as follows. Section II In the suggested method, a model for test sequence gener- describes the existing approaches to semi-formal verification ation, so-called generalized FSM model, is almost automati- of hardware designs. In Section III the suggested method is cally derived from specifications. The approach uses implicit discussed. This section consists of five subsections, which specifications in the from of pre- and post-conditions and describe the method for specifying synchronous designs (A), irredundant algorithms for FSM traversal. The distinction organization of adapters between specifications and an im- feature of the approach is that it does not require two different plementation (B), and usage of formal specifications of the models for checking design correctness and for test sequence introduced kind for construction of response checkers (C), generation. All testing tasks are carried out basing on formal coverage trackers (D), and stimuli generators (E). In Sec- specifications.
true: To define which operations can be started in parallel, a no-
om tion of execution channels is used. Each channel is associated
with a set of operations that can be executed via it. A channel
(=) can handle only one operation per cycle. Sets of operations for
different channels are able to have non-empty intersections.
false Moreover, each channel supports an empty operation nop.
be started simultaneously, if that combination of operations is
forks (=) Operations associated with different execution channels can
permitted.
Fig. 1. An example of a control flow graph Let k be a number of execution channels and X1, ..., Xk
be sets of operations associated with the channels. Possibility
III. SUGGESTED METHOD of parallel starting of k operations via different execution
channels is defined by a Boolean function sim : X1 × ... ×
Our approach to testbench development is based on cycle- Xk → {true, f alse}. If the design has several execution accurate formal specification of the design behavior. Each channels, one can define a generalized operation (multistim- operation of the design is described with the help of a ulus) as a k-tuple (x1, ..., xk) ∈ X1 × ... × Xk such that control flow graph having two types of nodes: control nodes sim(x1, ..., xk) = true. The precondition of the generalized and operational nodes. Control nodes specify control flow operation is a conjunction of the preconditions of x1, ..., xk. branching, creation of concurrent threads, etc. Operational Execution of a microoperation requires exactly one cycle. nodes describe one-cycle microoperations. Creation of parallel threads, checking branch condition and A. Design Specification making decision which branch should be taken are performed instantly. To interpret specifications, a set of current stages State of the design is formalized by a finite set of variables. is used. At the beginning of simulation the set is empty. Among the variables, there are input and output parameters On every cycle of simulation, a generalized operation with of the operations. All predicates and functions mentioned satisfied precondition is applied to the design. All initial stages below are defined over that set of variables. Functionality of of the operation are added into the set of current stages. After the design is described for separate operations. Specification that, the set of active stages is calculated among the current of an operation includes its precondition, which restricts stages. situations in which the operation is permitted to be started. A stage is called active, if its precondition P is true; If the precondition does not hold, then the operation’s result otherwise a stage is called interlocked. For each active stage is unpredictable. In general case, execution of an operation the corresponding command C is executed. In theory, the requires several cycles. A one-cycle part of an operation is commands of the active stages are executed in parallel. Af- called a microoperation. ter execution, the postconditions Q of the active stages are Structure of an operation’s control flow is described by a checked. Then, the active stages are removed from the set of directed graph in which four kinds of nodes are admitted: current stages. If an active stage is not final, then its successive cond, f ork, join (control nodes), and stage (operational stages are added into the set. A successor relation is defined nodes). Obviously, control flow graphs must fulfill certain on the base of the control flow graphs. Given a stage s and an requirements, e.g., out-degree of a stage node is not greater outgoing edge e, define the set of successive stages. Depending than one, a cond node has exactly two outgoing edges, on the type of the node the edge leads to, there are four which are marked by true and f alse, etc. An example of different cases: an operation control flow graph is shown on Fig. 1. The graph • If e leads to a stage node, then that stage is a successive on the picture consists of nine nodes: one cond, one f ork, one. one join, and six stages. • If e leads to a cond node, then the branching condition If in-degree of a stage node is equal to zero, the node is estimated and choice among two alternative edges is is called initial. If out-degree is equal to zero, the node is made. The same algorithm is applied recursively for the called final. An operation is allowed to have more than one chosen edge. initial stage and more than one final stage. Each cond node • If e leads to a f ork node, then the algorithm is applied is supplied with a predicate that represents a condition for recursively for each outgoing edge of the node. Then, the choosing control flow direction. Each stage node is described calculated sets of successive stages are unified. by a Hoare triple (microoperation’s contract) {P }C{Q}, • If e leads to a join node, then for each ingoing edge where P is a precondition, C is a command, and Q is a the finishing condition of the corresponding thread is postcondition [7]. Semantics of a microoperation precondition checked. If all threads are finished, the algorithm is is as follows. If the precondition is not satisfied, it does applied recursively for the outgoing edge of the node; not mean that the microoperation’s result is unpredictable. It otherwise the set of successive stages is empty (the node simply indicates that the microoperation is interlocked (it will will be processed again when another ingoing thread is be unlocked, when the precondition becomes true). finished).
ook stages. To check correctness of the design behavior in response
to a certain set of stimuli, the testbench works as follows.
frm ©) | • At the beginning of the cycle:
of © TTTⁱ ® – The testbench calculates the set of active stages:
Enabled ← {s ∈ S | Ps(·) = true}.
pi ©) – Then, it executes the drivers of the active stages in
p some order. The order is unimportant, because the
stages are independent.
TT • At the end of the cycle:
Fig. 2. Cycle-by-cycle execution of the operation – The testbench executes the commands of the active
stages.
Specifications of the described type are called cycle- – Then, it executes the monitors of the active stages
accurate contract specifications. Originally, they were intro- – and the mediator.
duced for linear multi-cycle operations to specify pipelined After that, the testbench estimates the design be-
designs [8]. havior by checking the postconditions of the active
B. Connection between Specifications and Implementation stages: Check(·) = ∧ Qs(·).
Fig. 2 shows cycle-by-cycle execution of the operation s∈Enabled
presented on Fig. 1. It is assumed that the operation’s stages – Finally, it updates the set of current stages:
have no interlocks (the preconditions of all microoperations ⋃
are identically true) and the branching condition cond is not S ← {s | s ∈ S \ Enabled} ∪ succs(·).
satisfied. On the first cycle the initial stage start is executed. s∈Enabled
This stage is responsible for setting the operation’s strobe Here, succ
and for assigning the input parameters of the operation to s is a function that returns the set of
the corresponding inputs of the design. The second cycle successive stages of the stage s.
is occupied by stage1. At the end of the second cycle the D. Test Coverage Description
branching condition cond is estimated. Under our assumption,
the condition is false. During the third cycle two one-cycle In the suggested approach to testbench automation, a test
threads stage3 and stage4 are executed in parallel. The last adequacy criterion is defined on the base of formal specifi- cycle is taken by the final stage end. cations. Test coverage has a hierarchical structure describing To perform simulation-based verification, a testbench should different aspects of the design functionality. It consists of three connect specifications with an implementation. For this pur- levels of granularity. pose, one should develop special testbench components: stage Microoperation-level coverage defines test situations on drivers, stage monitors, and a mediator. The stage driver is microoperation interlocks (interlock coverage) and on func- responsible for setting the input signals required by the stage. tional branches inside individual microoperations (functional Usually, input signals (an operation strobe and parameters) are coverage). In the simplest case, interlock coverage includes set by initial stages. The driver is executed at the beginning of two situations, which describe whether the stage is interlocked the cycle on which the stage is carried out. The stage monitor or not. General-case coverage takes into account a structure reads the output signals and the internal data affected by the of the logical formula that describes the interlock. A typical stage and converts them into the specification representation. microoperation has no local branching; therefore its functional The information obtained by the monitor is used for checking coverage consists of only one element. the stage correctness. The monitor is executed at the end Operation-level coverage specifies test situations on an of the corresponding cycle. The mediator reads the output operation in terms of paths in the operation’s control flow signals and the internal data shared by all operations of the graph. Usually, a control flow graph is acyclic. In this case, it design and converts them into the specification representation. is reasonable to define test situations as paths from the initial It synchronizes the specification state with the implementation nodes to the final ones. one. The mediator is executed at the end of each cycle of Pipeline-level coverage describes test situations connected simulation. with parallel calls of operations (multistimulus coverage) and C. Organization of Response Checkers simultaneous execution of microoperations (control state cov- erage). The goal of test generation is to create all feasible Assume that each stage s is specified by a Hoare triple combinations of simultaneously executing microoperations. To {Ps}Cs{Qs} and supplied by a driver Ds and a monitor Ms. this effect, one needs to use all possible paths in operations In addition, a mediator M is defined. Let S be a set of current and all possible interlock situations.
Operations executed by a design=) V. CASE STUDY
The suggested method and the CTESK toolkit have been
©)
© =) <> ©) cotont FSM used in several industrial projects on hardware verification.
stats calculation
( eneralized model)model The most complex project is the testbench development for
\ L2 cache of the MIPS64-compatible microprocessor.
The cache under verification is a direct-mapped 256 KB
.| > cache that consists of 8192 rows and serves both data and
Setotcurontsiages instructions. It implements operations for loading and storing
data, for loading instructions, for modifying control informa-
=) tion, and some others (total number of the operations is 6). All
operations are multistage pipelined operations (total number of
the microoperations is 92). Many of them contain branching
as S of control flow. Some operations can be started in parallel
(maximum number of parallel starting operations is 3).
Fig. 3. Construction of an generalized FSM model Specifications of the microoperations were represented in
the form of Hoare triples. It should be emphasized that all re-
E. Test Sequence Generation quirements were cheaply formalized (total number of the non-
trivial preconditions, commands and postcondition is 120).
To create test sequencies for a design under verification, we The volume of specifications is about 3 KLOC in SeC. The
use a generalized FSM model of the design. Roughly speaking, labor costs of the testbench development are approximately 6
a state of genereralized model is idenfied by a set of current man-months (20-30% of RTL development efforts). In this
stages (see Fig. 3). The state graph of the generalized model project we have found 12 functional errors in the design
is created on the fly. Test generation is complete when all implementation including very critical ones.
reachable states (all feasible combinations of simultaneously VI. CONCLUSION
executing microoperations) are visited.
In order to make the model deterministic, a verification The method described in the paper is applicable to a
engineer should include some additional information into wide rage of synchronous hardware including parallel-pipeline the FSM state. For example, if there are interlocks in the designs with control flow branching and parallel threads in- microoperations, one should add a certain information that de- side individual operations. The usage of formal specifications terministically determines the interlock conditions; if there are allows to automate the main tasks of simulation-based verifica- branches in the operations, one should add some information tion: test sequence generation, checking of design correctness, that determines the branching conditions, and so on. This part and estimation of test completeness. The distinction feature of of the approach is not fully automated. the approach is that the same specifications are used for all To compile several operations from different execution tasks of testing. This simplifies maintenance of testbenches and channels into a multistimulus, we have a temporary buffer [9]. reduces verification efforts. The suggested approach has been Every operation except nop is put into the buffer before it is successfully used in real-life projects on hardware verification. applied to the design. Multiple operations targeted at the same REFERENCES channel are prohibited to be added. When nop is applied, all [1] J. Bergeron. “Writing testbenches: functional verification of HDL mod- operations stored in the buffer are applied to the design in els”. Kluwer Academic Publishers, 2000. parallel, and the buffer is flushed. [2] W. Lam. “Hardware design verification: simulation and formal method- based approaches”. Prentice Hall, 2005. IV. TOOL SUPPORT [3] S. Qadeer, S. Tasiran. “Promising directions in hardware design verifi- The suggested approach to specification-driven testbench cation”. Proc. of International Symposium on Quality Electronic Design, 2002. development is supported by the CTESK toolkit developed [4] S. Ur, Y. Yadin. “Micro architecture coverage directed generation of test at ISPRAS [10]. This toolkit is originally intended for testing programs”. Proc. of Design Automation Conference, 1999. software systems written in C programming language, but it [5] P. Mishra, N. Dutt. “Functional coverage driven test generation for validation of pipelined processors”. Proc. of Design, Automation and Test has been adapted for verification of RTL models of hardware in Europe, 2005. designs. [6] R. Ho, C. Yang, M. Horowitz, D. Dill. “Architecture validation for CTESK uses SeC language for development of testbench processors”. Proc. of International Symposium on Computer Architecture, 1995. components. SeC is a C extension, which has additional [7] C.A.R. Hoare. “An axiomatic basis for computer programming”. Com- constructs for description of specifications, drivers, monitors, munications of the ACM, 12(10):576-580,583, 1969. and other components. The toolkit supports the advanced [8] A. Kamkin. “Contract specification of pipelined designs: application to testbench automation”. Proc. of Spring Young Researchers’ Colloquium FSM-based techniques for test sequence generation. Testbench on Software Engineering, 2007. functionality connected with interpretation of cycle-accurate [9] M. Chupilko. “Constructing test sequences for hardware designs with contract specifications and response checking is implemented parallel starting operations using implicit FSM models”. Proc. of East- West Design & Test Symposium, 2009 as a library extension of CTESK. [10] http://hardware.ispras.ru