Contact: Tobias Ludwig

With "Property-First Design" or "Property-Driven Design (PDD)" we propose a new method that starts from an abstract system model and integrates formal property checking systematically 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 technology is applied in such a way that a formal relationship is provided between the abstract system model and its concrete implementation at the Register Transfer Level (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, however, 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. We have already reported several case studies on open-source and industrial designs that demonstrate the potential of a PDD-based design paradigm.

Sample designs and property sets, manuals and the supporting tool DeSCAM can be found on github

Further reading:

• T. Ludwig, J. Urdahl, D. Stoffel, W. Kunz:
  Properties First – Correct-By-Construction RTL Design in System-Level Design Flows
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (to be printed)
• T. Ludwig, M. Schwarz, J. Urdahl, L. Deutschmann, S. Hetalani, D. Stoffel, W. Kunz:
  Property Driven Development of a RISC-V CPU
  Proceedings DVCON US, 2019
• S. Udupi, J. Urdahl, D. Stoffel, W. Kunz:
  Exploiting Hardware Unobservability for Low-Power Design and Safety Analysis in Formal Verification-Driven Design Flows
  IEEE Transactions on Very Large Scale Integration Systems, Vol. 27 , No. 6 , June 2019 
• J. Urdahl, D. Stoffel, W. Kunz:
  Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 33, No. 2, Feb. 2014, pp. 291-304