Properties First—Correct-By-Construction RTL Design in System-Level Design Flows

摘要

This paper presents a new Property-Driven Design (PDD) method that starts from an abstract system model and integrates formal property checking early into a top-down design methodology for register transfer level (RTL) hardware. In PDD the role of formal verification is not limited to "bug hunting" alone. Instead, the formal techniques are applied in such a way that a formal relationship is provided between the abstract system model and its concrete implementation at the RTL. In order to avoid the high efforts associated with verification by property checking the proposed PDD approach automatically generates abstract properties from a system-level description and later refines them along the design process. The advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional design flows with property checking. The main benefit of the proposed approach results from the fact that a formally sound system model is available together with the RTL design. Specifically, LTL properties proven on the abstract model also hold on the concrete implementation. This facilitates many complex analysis and verification tasks in today's design flows and contributes to emancipating system-level models from prototypes to golden design models. Several open-source and industrial case studies are reported that demonstrate the high potential of a PDD-based design paradigm.