Semi-Formal Test Generation with Genevieve

This paper describes the first application of the Genevieve test generation methodology. The Genevieve approach uses semi-formal techniques derived from "model-checking" to generate test suites for specific behaviours of the design under test. An "interesting" behaviour is claimed to be unreachable. If a path from an initial state to the state of interest does exist, a counter-example is generated. The sequence of states specifies a test for the desired behaviour. To highlight real problems that could appear during test generation, we chose the Store Data Unit (SDU) of the ST100, a new high performance digital signal processor (DSP) developed by STMicroelectronics. This unit is specifically selected because of the following key issues:

• Type: Conference
• Year: 2001
• Where: DAC
• Authors: Julia Dushina, Mike Benjamin, Daniel Geist
• Keywords: DAC 2001, Design Automation, Genevieve Approach, Genevieve Test Generation, Test Suites