First ACM & IEEE International Conference on

Formal Methods and Models for Codesign (MEMOCODE'2003)

Programming models, formal analysis methods and verification techniques for high-level
system design and (re)engineering: towards convergence of formal methods and industrial trends.

June 24th.-26th., 2003 -- Mont Saint-Michel, France

Home page
Aims and scope
Call for papers
Industrial case studies

I. Conformance checking
Arvind, Stan Liao, Nancy Lynch, Carl Pixley, Rob Slater, Marten Van Hulst

II. Hierarchical verification
Forrest Brewer, Hans Eveking, Grant Martin

III. Abstraction vs. optimization
Brian Bailey, Stephen Edwards, Rajesh Gupta, James Hoe

IV. Incremental verification
Harry Foster, Hillel Miller, Marten Van Hulst

V. Post-production patchability
Forrest Brewer, Masahiro Fujita

Industrial case studies. Prospective authors are invited to submit novel and unpublish work devoted to the presentation of position papers and scientific contributions on actual design problems proposed by members of the program committee from major EDA industry companies.

Problem II : Hierarchical verification

Authors : Forrest Brewer, Hans Eveking, Grant Martin.

In many design situations, pre-designed blocks ("IP's") are used to build a system. We assume that each of the blocks is correctly designed with respect to some formal specifications, and measures (high-level block-functional specification, set of proven block-properties, etc.). How can the following problems be solved:

(a) If the blocks which are known to be correct are composed to build a system - what is a definition of correctness of the system and how can it be specified, represented and used?

(b) Blocks typically make assumptions about their environment. If the assumptions are not satisfied the blocks do not work correctly. A necessary prerequisite for the correctness of a composed system is the verification of the block-assumptions. How can such assumptions be specified, composed and efficiently verified for large systems?

(c) How can a model of a system be built (i) which is smaller than the composition of all blocks and (ii) which can be used to prove partial properties like successful communication of some blocks? How can we guarantee that the smaller model is conservative, i.e., still allows verification and not only bug-finding?

(d) How can we solve problems (a) - (c) if (as is commonly the case) the internal details of some the blocks are unknown?

(e) Is there a role for standardized protocols for block communication? Is there a possibility to re-use verification knowledge of these protocols?

(f) How can the notion of a block functional specification be formalized so that efficient system functional specifications can be composed from block specifications?