It has long been the practice to create models in C or C++ for architectural studies, software prototyping and RTL verification in the design of Systems-on-Chip (SoC). It is often the case that by the end of a design project, multiple C models exist for different uses. Clearly, this leads to wasted effort on the part of model developers, and creates risk of functional divergence across models. In this paper we present some guidelines for system-level modeling and RTL design to allow for efficiently leveraging the system-level model for RTL verification via simulation based techniques, as well as via sequential equivalence checking. The paper presents the challenges of keeping system-level models and RTL synchronized from a functional perspective and presents some techniques for overcoming these challenges. Categories and Subject Descriptors B.5.2 [RTL Implementation] Design Aids General Terms Reliability, Verification. Keywords System-level models, equivalence checking, simulation, RT...