DeepTrans - Extending the Model-based Approach to Functional Verification of Address Translation Mechanisms

This paper presents a new test case generation technology, specifically targeted at verifying systems that include address translation mechanisms. The ever-growing demand for performance makes these mechanisms more complex, thereby increasing the risk of bugs and increasing the need for such technology. DeepTrans is a package that extends existing test generators with address translation testing capabilities. It uses a declarative modeling language that includes constructs for describing the address translation process, commonly used translation resources, and architecture rules related to translation. The address translation model is converted to a constraint satisfaction problem that is solved simultaneously with the problem formulated by the generator. DeepTrans is currently used by two different IBM test generators