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 I : Levels of Abstraction, Notion of Conformance and Equivalence

Authors : Arvind, Stan Liao, Nancy Lynch, Carl Pixley, Rob Slater, Marten Van Hulst.

Many companies these days deliver high-level models (C, C++, SystemC, etc.) to their customers - even before the RTL is written. Early availability of models has many benefits including verification, software development, and performance evaluation. Currently, there is no automated way to compare the high-level models to the RTL or gate-level models. This is counter to the industry trend to compare all models automatically, from RTL to gate to switch to transistor. Boolean and switch-level logic checking has become routine in the semiconductor industry. However, there are no such tools for high-level models.

Are some high-level models more amenable to equivalence checking than others? Must the model be clock-cycle accurate -- at least at the chip boundary? If not, what is the notion of equivalence that one might employ? Is there a methodology that can make the equivalence problem easier? Are there algorithms that can handle equivalence-checking on realistic models.

Papers are invited to illuminate any of these problems.