11th Advanced Research Working Conference
on Correct Hardware Design and Verification Methods

4-7 September 2001
Institute for System Level Integration
Livingston, Scotland.

Tutorial Programme

The CHARME conference begins with a morning programme of tutorials on Tuesday, 4th September, at the Institute for System Level Integration. The theme of the tutorials is system-level design and validation from an industrial perspective. The first speaker is Robert Fairlie from Verilab Ltd., a design consultancy specialising in all aspects of hardware design verification. The second speaker is Gérard Berry from Esterel Technologies, who provide methodology and tools to develop formally validated system designs.

All participants are welcome to attend the tutorials; no extra fees are payable.

• Robert Fairlie
  Verilab Ltd.
  A Practical Approach to Verification in SoC Design

  Abstract. As design complexity increases the size of the verification task increases exponentially. At today's level of SoC integration a verification plan that fully validates all modes of operation would be totally inconceivable with conventional simulation techniques. This tutorial describes some of the approaches used in SoC design to reduce the overwhelming burden of verification, including alternative HDLs, specialist verification languages, statistical analysis of bug detection and alternatives to conventional simulation.

• Gérard Berry
  Esterel Technologies
  High-level Description, Synthesis, and Validation of Control-Dominated Designs

  Abstract. Control-dominated designs are ubiquitous: internal chip control, chipsets, glue logic and protocols, embedded systems, etc. They are notoriously hard to program using classical RTL-level HDLs, and hard to validate. Systems design level Synchronous languages have been developed in academia since 1983 to address this problem and they have now reached the industrial stage.

  We present the twins languages Esterel (textual) and SynchCharts (graphical) on which the Esterel Studio tool suite is based. These languages use control-specific primitives such as freely mixable sequencing, concurrency, preemption and exception constructs, hierarchical automata constructs, and instantaneous broadcasting of communication signals. They are rigorously defined by mathematical semantics.

  Originally designed for software applications, they have been recently extended to deal more specifically with hardware design. The synthesis algorithms are based on source-code driven efficient state-encoding techniques. They generate either C code ot statndard HDL code, fully respecting the semantics in both cases. BDD-based tools make it possible to perform safety property validation and coverage test generation.

Lunch will be provided after the tutorials and will be followed by the first session of submitted CHARME papers.