Extending the scope of translation validation by augmenting path based equivalence checkers with SMT solvers

The initial behavioural specification of an embedded system goes through significant optimizing transformations, automated and also human guided, before being mapped to an architecture. Establishing the validity of these transformations is crucial to ensure that the intended behaviour of a system has not been faultily altered during synthesis. Finite state machines with datapath (FSMDs) have traditionally been used to model the specification and the implementation. Path based equivalence checkers over this model have been proposed to validate the translation process. Since specification for digital systems implementing algorithmic computations over integers involves the whole of integer arithmetic which is undecidable, majority of these equivalence checkers employ a normalization technique that tries to reduce two computationally equivalent expressions e₁ and e₂ to a syntactically identical form. This normalization technique, however, is not applicable to reason over finite precision datatypes. In this work, we propose to augment the normalization module, wherever necessary, with an SMT solver to determine the validity of e₁= e₂. The scope of translation validation can be extended to handle bit-vectors, user-defined datatypes and more sophisticated transformations by leveraging the capability of SMT solvers while keeping the basic equivalence checking framework intact. We have explored three state-of-the-art SMT solvers namely, Yices2, CVC4 and Z3. The experiments demonstrate improvement in terms of its scope of application over the existing methodology.