Building a Correct-by-Construction Model from High-Level Specification Down to RTL > Training > November 20-21, 2008

[training]

Title: ECSI Workshop on TLM Users Experience

Building a Correct-by-Construction Model from High-Level Specification Down to RTL   Munich, Germany November 20-21, 2008 Free of charge training   This course addresses innovative design and verification techniques for predominantly electronic systems in a general ESL design flow. The methodology presented here is the result of the SPRINT project, more precisely of WP2-High level modelling, tasks 2.1.2 Formal verification of SPRINT Entry-Level Models and 2.4 Abstraction Level Transactors and Equivalence Checking (Methods for equivalence checking : SLM/TLM and TLM/RTL ). In this tutorial we present through a case study - a multimedia console, four of the stages from the specs down to the synthesise-able RTL:   1-      Building the entry level specification model (SLM) while formally verifying the model through refinement 2-      Building an architectural hierarchy 3-      Building a TLM model while formally verifying the refinement relationship with the SLM model. 4-      Building a RTL model + transactor while formally verifying the refinement relationship with the TLM model.   This methodology allows to obtain correct by construction models at each abstraction level, with executable counterparts at TLM and RTL level. The equivalence checking is not done after the model is build, but during the building process, through intermediate refinement steps.   November 20, 2008   16:00 -   17:30 The role of formal methods in the design flow. Why using theorem proving technique? Overview of a top-down ESL methodology. November 21, 2008   9:00 -   10:30   From requirements to a Specification Formal Model (SFM): How to build a specification formal model from informal data. Links between the SPRINT entry Level Model ( SLM) and the SFM. Coffee break   11:00 -   12:30 Building a functional hierarchy model through refinement and decomposition. Introducing TLM communication and platform structure (a correct by construction SystemC TLM model is obtained). Lunch   14:00 -   15:30 TLM to RTL proof-controlled synthesis with proven transactor generation (the result is a correct by construction VHDL module + the corresponding SystemC transactor from TLM interface to RTL interface).   To register please contact the ECSI Office: [EMAIL PROTECTED] +33 4 76 63 49 34    To remove from the mailing list > please reply to this e-mail with the subject REMOVE

_________________________________________________________________________________
mozart-users mailing list                               
mozart-users@mozart-oz.org
http://www.mozart-oz.org/mailman/listinfo/mozart-users