Title :
Towards Test Case Generation for Synthesizable VHDL Programs Using Model Checker
Author :
Ayav, Tolga ; Tuglular, Tugkan ; Belli, Fevzi
Author_Institution :
Dept. of Comput. Eng., Izmir Inst. of Technol., Izmir, Turkey
Abstract :
VHDL programs are often tested by means of simulations, relying on test benches written intuitively. In this paper, we propose a formal approach to construct test benches from system specification. To consider the real-time properties of VHDL programs, we first transform them to timed automata and then perform model checking against the properties designated from the specification. Counterexamples returned from the model checker serve as a basis of test cases, i.e. they are used to form a test bench. The approach is demonstrated and complemented by a simple case study.
Keywords :
formal specification; hardware description languages; program testing; program verification; formal system specification; model checker; synthesizable VHDL programs; test case generation; timed automata; Automata; Automatic testing; Circuit synthesis; Computational modeling; Field programmable gate arrays; Mathematical model; Reliability engineering; Safety; Software testing; System testing; Test case generation; model checking; program transformation; synthesizable VHDL; timed automata;
Conference_Titel :
Secure Software Integration and Reliability Improvement Companion (SSIRI-C), 2010 Fourth International Conference on
Conference_Location :
Singapore
Print_ISBN :
978-1-4244-7644-2
DOI :
10.1109/SSIRI-C.2010.22