Arithmetic Circuit Design Explicit and Inplicit Automata Verification by Model-Checking

Registration Fee:

3,000 THB (coffee breaks and lunch included)

Accommodation:

ASIAN'99 accommodation rates are applicable to attendees for the Asian School.

The Prince of Sogkhla University also provides comfortable
accommodation on campus at a very reasonable rate.

 Digital synchronous circuits DSC provide a mathematical representation for a wide class of electronic circuits. As such, they present the most efficient known implementations for algorithms at large.

 In a first part, we review the known correspondances between DSC, automata and BDD, through their truth-tables. Basic circuit synthesis techniques follow, and links are made with the other two topics.

 The rest specializes in the construction of basic arithmetic circuits (add, subtract, multiply and divide), in relation with bit-ordering (low to high, high to low) and carry rules. Systematic time/space tradeoffs are constructed. The theory is presented through actual applications, arising from image processing and high energy detectors.

 Finite automata are one of the most fundamental structures of Computer Science. They have been extensively studied in several contexts: language theory, hardware circuits design, process calculi, reactive systems, etc. Our aim is to present a modern course on automata encompassing all these aspects.

 In the first part, we review the classical properties of deterministic and non-deterministic automata, and we study in depth the translation from various kinds of regular expressions into automata. This translation is essential for most of the linguistic developments based on automata, such as reactive languages. Then, we study the implicit presentation of automata as Boolean functions and we present various normal forms for sequential functions. This parts links the course with both arithmetic circuit design and verification.

 We survey the basic techniques for verifying properties of logical systems (circuits, automata) by exploring their state space. These techniques are now of common usage in hardware verification, and their use for software becomes more and more important.

 A first part is devoted to the verification of safety properties (something "bad" never happens), which can be verified by traversing the reachable (or unreachable) states of the system. This traversal can be done enumeratively, or symbolically (by encoding sets of states by means of Binary Decision Diagrams).

 In a second part, we consider general properties, expressed in the temporal logic CTL. We show how the (BDD of the) set of states satisfying a CTL formula can be computed.

Contact us: Olivier Nicole

Last update: Oct 1999