Using model checkers for automatic generation of VHDL test case with improved test coverage

Testing is an essential part of any circuit design flow as a design has to be tested for consistency with the specifications. ASICs are tested at different stages of the circuit design flow with functional testing at the design level being the most important, as a defect can be detected at an earlier stage. The use of a VHDL test bench to test a circuit built using VHDL is the most common validation method used during the design. Test inputs are chosen intuitively and applied within the test bench; obtained outputs are checked against the expected output values to verify the proper functioning of the circuit under test.;The research develops the use of model checkers for constructing test cases using circuit specifications and expected system properties. The test bench is converted into a timed automata model which is used to generate automated test cases by applying negated circuit properties to the model checker. The new transformation rules help in the conversation of VHDL code into the network of timed automata.;Complete coverage of the system property is assured in the generated test set and the test cases are generated automatically for different system properties. The new approach is implemented on the basic gates to address the transformation of gate models.