Constraint solving for test case generation: a technique for high-level design verification
- 2 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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.Keywords
This publication has 7 references indexed in Scilit:
- Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generatorIBM Systems Journal, 1991
- Experiments in automated analysis of concurrent software systemsPublished by Association for Computing Machinery (ACM) ,1989
- Cesar: a static sequencing constraint analyzerPublished by Association for Computing Machinery (ACM) ,1989
- Design verification of the WE 32106 math accelerator unitIEEE Design & Test of Computers, 1988
- Formal Verification and Implementation of a MicroprocessorPublished by Springer Nature ,1988
- On sets of Boolean n-vectors with all k-projections surjectiveActa Informatica, 1983
- Hints on Test Data Selection: Help for the Practicing ProgrammerComputer, 1978