Zur Hauptnavigation / To main navigation

Zur Sekundärnavigation / To secondary navigation

Zum Inhalt dieser Seite / To the content of this page

Sekundärnavigation / Secondary navigation

Inhaltsbereich / Content

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.

Publications

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)

top.vhd
framer.vhd
monitor.vhd

Property Suites 

SVA
framer.sv
monitor.sv
ITL (OneSpin Solutions proprietary language)
framer.vhi
monitor.vhi
uP_interface.vhi
completeness.vhi

System-Level Design (Abstract Model)

Promela (Spin)

abstractModel.pml

 

 


 

  • J. Urdahl, D. Stoffel, W. Kunz: "Architectural System Modeling for Correct-by-Construction RTL Design", Proc. Forum on Specification and Design Languages (FDL), Barcelona, Spain, September 2015.

 

Supportive material: