Verification at RTL Using Separation of Design Concerns

Design-for-test, logic built-in self-test, memory technology mapping and clocking concerns require team-months of verification time as they traditionally happen at gate-level. We present a novel concern-oriented methodology that enables automatic insertion of these concerns at the register-transfer-level where verification is easier. The methodology involves three main phases: (1) flipflop inference and instantiation algorithms that handle parametric RTL modules, (2) transformations that take entry RTL and produce RTL modules where memory elements are separated from functionality, and (3) a concern weaving tool that automatically inserts memory related design concerns implemented in recipe files into the RTL modules. The transformation is sound as proven and validated by equivalence checking using formal verification. We implemented the methodology in a tool that is currently used in an industrial setting wherein it reduced design verification time by more than 40%. The methodology is also effective with open source embedded system frameworks.