Correct-by-Construction Embedded System Design
Contact: Tobias Ludwig
In this research project we are developping a radically different design approach where RTL models and ESL models stand in a formally well-defined relationship to each other based on the notion of Path Predicate Abstraction (PPA).
Establishing system-level models as PPAs of RTL designs can change the role of system-level models fundamentally: rather than being “prototypes” and standing in an undefined relationship with the implementation they may be trusted as “design models”, just like RTL design models are trusted to be sound abstractions of the underlying gate level (by merit of formal equivalence checking). This can lead to fundamental changes in system-level design flows.
This page gives links to our most important papers in this area and provides supportive material for some of these papers.
- J. Urdahl, S. Udupi, T. Ludwig, D. Stoffel, W. Kunz: Properties First? A New Design Methodology for Hardware, and its Perspectives in Safety Analysis, IEEE/ACM International Conference on Computer Aided Design (ICCAD), Austin, USA, 2016.
- J. Urdahl, D. Stoffel, W. Kunz: "System- versus RT-Level Verification of Systems-on-Chip by Compositional Path Predicate Abstraction", Technical Report EDA-2013-01-29 (revision 2014-05-24)
- 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
Supportive material for these papers:
Example: Simplified SONET / SDH Framer
The proposed methodology is illustrated by this example. Formal verification proves a set of properties which creates path predicate abstractions for the considered modules. The compositionality of the technique is addressed in Technical Report EDA-2013-01-29. The abstract modules can be composed into a larger system. The resulting system of path predicate abstractions can be realized in any modelling language. The download contains an abstract model description written in Promela, the modelling language of the model checker Spin.
An overview of the example and the methodology applied is given in Sec. VI of the technical report.
RTL Design (Concrete Model)
|ITL (OneSpin Solutions proprietary language)|
System-Level Design (Abstract Model)