C++TESK Getting Started¶

Introduction¶

Hardware verification is usually understood as the process of checking behavior of hardware on conformity to its specification. Such a process can be done formally by means of, e.g., model checking, automatic theorem proving, etc. Also, verification can be done by means of simulation of separated hardware modules with the help of simulator.

Accounting the complexity of hardware models under verification, the task of automation should have usually been solved before the actual verification. The more processes will be done automatically and the less manual labor will be needed, the more effective check will be made. Without touching upon the formal verification methods, in this course we will focus only on simulation-based verification. Moreover, we will further speak only about one of the existing verification tool, created in the Institute for system programming of RAS. The tool''s capabilities allow speaking about it as a powerful and quite modern solution. So, we will speak about using C++TESK Testing ToolKit (or C++TESK for short).

C++TESK implements simulation based approach to verification. The main element of the tool is its core library, implemented in programming languages C and C++. All core components are arranged in one package and are available at http://forge.ispras.ru/projects/cpptesk-toolkit/files. The tool is designed for creating test systems using C++ for different models of synchronous hardware at different levels of abstraction. Test systems are created using any means, provided by C++, basing on the approach, macros and classes defined by C++TESK.

When creating test systems for simulation based verification, three main tasks are usually solved. The first one is test sequence construction, the second one is checking of behavior correctness, and the third one is test completeness estimation. C++TESK allows construction test sequences of two types: selection random stimulus set from the previously described stimuli at each simulation cycle or selective choice of stimuli based on techniques of exploration of implicitly defined FSMs. Checking of behavior correctness is made at each simulation cycle by means of executable reference model, created by verification engineer at some level of abstraction. External model (e.g., system simulator) can also be used. Test completeness is determined either by the number of testing cycles for randomly selected stimuli, or on the basis of the information about completeness of FSM exploration.

Common scheme of test system is represented in figure 1.