Unit-Level Approach: Testbench Automation

This page describes our approach to simulation-based verification of hardware designs at unit level. The approach is based on CTESK tool that automates creation of testbenches on the base of formal specifications. The tool allow specifying operations of design under test (DUT) with cycle-accuracy and to generate test sequences.

Cycle-Accurate Contract Specifications

We use so-called cycle-accurate contract specifications to automate testbench development for hardware units. Such specifications split each operation into a sequence of micro-operations corresponding to separate stages of the operation and defines each micro-operation in the form of pre- and post-conditions.

Thus, contract of the operation consisting of several micro-operations is formalized by the structure:

CONTRACT = <PRE, {(PRE[i], POST[i])}>,

where PRE is the pre-condition of the operation, PRE[i] is the pre-condition of the i-th microoperation (it is also called guard condition), and POST[i] is the postcondition of the i-th microoperation.

Pre-condition of operation restricts situations in which the operation can be supplied for execution. Guard condition of micro-operation is a negation of the interlock condition, i.e. the microoperation is interlocked, if and only if the corresponding guard condition does not hold. Post-condition of micro-operation implicitly describes its functionality in the form of predicate.

The approach is applicable not only for linear operations, but for branching operations as well. In this case, one should describe a control flow graph of operation and supply each micro-operation vertex with pre- and post-conditions.

Specification-Driven Testbench Automation

On the base of such specifications, the CTESK tool can automatically verify correctness of component behavior in response to test action and generate test sequences.

To check DUT behavior, testbench in each cycle of simulation should keep track which micro-operations are finished and check corresponding post-conditions. Roughly speaking, contract specifications are interpreted as special kind of automaton. State of the automaton is a set of pairs (OP, STAGE), where OP is an operation identifier and STAGE is an order number of micro-operation.

Let us assume that at some moment of time automaton state is STATE = {(OP[i], ST[i])} and testbench is starting execution of operation OP (precondition of the operation is fulfilled). Then, the post-state of the transition is a union of the following sets:

  • {(OP, 1)}
  • {(OP[i], ST[i]) | PRE(OP[i], ST[i]) = false}
  • {(OP[i], ST[i] + 1) | PRE(OP[i], ST[i]) = true and ST[i] < L[i]}

Test oracle for the transition is the conjunction of post-conditions of the executed micro-operations:

ORACLE(STATE) = {POST(OP[i], ST[i]) | PRE(OP[i], ST[i]) = true}.

The goal of verification can be defined formally as covering all feasible states of the automaton. To achieve the goal, we use irredundant algorithms for traversing directed graphs. The important feature of irredundant algorithms is that they operate with graphs defined implicitly by function that for each node calculates a set of possible stimuli. Test generation is done on-the-fly.

Test Development Process

Hardware designers provide test developers with documentation on the target hardware component: description of operations, standards, etc. Test developers create formal specifications and define test coverage. Both descriptions are used as inputs for the CTESK tool. Test sequence generation is performed automatically on-the-fly in an HDL simulator. The result of test execution is a detailed report on defects identified and testing coverage achieved during testing.