Constraint solving for test case generation: a technique for high-level design verification

The use of constraint solving and symbolic execution to generate highly probing test cases is discussed. A system called AVPGEN, which uses such techniques for debugging high-level machine designs and has already proved useful in finding errors, is described. AVPGEN generates large numbers of architecture verification programs. It consists of a generator and a symbolic simulator. The generator uses constraint solving, symbolic values and undo capabilities to set up conditions. These conditions may be architecture specific or design specific. The simulator in AVPGEN, although not bug-free, is considerably simpler than any of the hardware implementations it is used to verify