Automated Test Generation for Activation of Assertions in RTL Models
Yangdi Lyu, Prabhat Mishra
Abstract
A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.
Topics & Concepts
Computer scienceAssertionScalabilityAutomatic test pattern generationProgramming languageModel checkingTest (biology)Theoretical computer scienceOperating systemEngineeringElectronic circuitElectrical engineeringPaleontologyBiologySoftware Testing and Debugging TechniquesFormal Methods in VerificationSoftware Reliability and Analysis Research