- 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
- 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?