Tool Support for Hardware Verification


Institute for System Programming of the Russian Academy of Sciences has developed and use for hardware verification the following tools:

  • CTESK

    CTESK tool is originally destined to testing of C-software, but we have adapted it for simulation-based verification of HDL models of hardware components.

    CTESK implements UniTESK concepts of automated specification-driven test development. Target design (HDL model) is formally specified with the help of contract specifications in form of pre- and post-conditions of operations and micro-operations. Using such specifications one can automatically check design behavior and construct test sequence using FSM traversal techniques.

    CTESK is rather universal; there are no fundamental limitations on the kind of hardware or software under test. In particular, the tool is applicable to testbench development for synchronous parallel-pipeline designs.

  • C++TESK

    The development of C++TESK tool responded to the demand of complex hardware designs high-quality verification.

    C++TESK inherits the best features of CTESK: FSM-based stimuli generation, pre- and post- conditions for operations and micro- operations; in same time C++TESK invents new level of convenience as it utilizes C++ language with all its benefits.

    C++TESK includes a set of rules thoroughly describing the way of creating test systems and verifying target designs.

    The approximate time of test development by means of C++TESK depends on engineer qualification, but there is a practical estimation: each 2 thousand Verilog code requires one person-month to develop a moderate test.

  • MicroTESK

    MicroTESK tool is aimed to test program generation for microprocessors and other programmable devices.

    The tool automates creation of test program generators for microprocessors by using model-based approach. It allows specifying CPU instruction set, define test coverage, and to configure a generator for concrete verification goals. Test program generation is based on instruction set models and instruction-level test coverage. All components of a generator (CPU model and test coverage) are developed in Java programming language with the help of MicroTESK core library. The tool allows generating self-checking test programs.

    MicroTESK is applicable to a wide range of programmable devices: special- and general-purpose microprocessors, coprocessors, controllers, etc.