LoLA
(only in english)
General Information
Download
Documentation
|
Verification of a GALS wrapper
A GALS circuit is a complex integrated circuit where several
components operate locally synchronously but exchange information
asynchronously. GALS technology promises lower energy consumption and
higher clock frequency.
In a joint project, researchers at Humboldt-Universität zu Berlin
and the Semiconductor Research Institute in Frankfurt/Oder analysed a
GALS circuit that implements a device for coding/decoding signals of
wireless LAN connections according to the 802.11 protocol. They were
particularly concerned with parts of the circuit they called wrapper.
A wrapper is attached to each synchronous component of a GALS circuit.
It is responsible for managing the asynchronously incoming data,
pausing the local clock in case of no pending data, and shipping the
outgoing signals to the respective next component. They modeled a
wrapper as a place-transition net and analysed the occurrence of
hazard situations. A hazard is a situation where, according to two
incoming signals within a very short time interval, output signals may
assume undefined values. In the model, a hazard situation corresponds
to a particular reachable state predicate. LoLA was used with stubborn
sets and the sweep-line method as reduction techniques. Analysis
revealed 8 hazard situations in the model. 6 of them were ruled out by
the engineers due to timing constraints which were not modeled. The
remaining 2 hazards were confirmed as real problems. The circuit was
redesigned and another verification confirmed the absence of hazard
situations.
More information: Milos Krstic, Eckhard Grass, and Christian Stahl.
Request-Driven GALS Technique for Wireless Communication System. In
Proceedings of the 11th International Symposium on Advanced Research
in Asynchronous Circuits and Systems (ASYNC 2005), New York, NY, USA,
pages 76-85, March 2005. IEEE Computer Society.
Next case study:  Validation of a Petri Net
Semantics for WS-BPEL
|