CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Safety Property Verification of Cyclic Synchronous Circuits

Koen Claessen (Institutionen för datavetenskap, Formella metoder ; Institutionen för datavetenskap, Funktionell programmering)
Electronic Notes in Theoretical Computer Science. SLAP 2003: Synchronous Languages, Applications and Programming, A Satellite Workshop of ECRST 2003, Porto, 1 July 2003 Vol. 88 (2003), p. 55-69.
[Konferensbidrag, refereegranskat]

Today's most common formal verification tools for hardware are unable to deal with circuits containing combinational loops. However, in the areas of hardware compilation, circuit synthesis and circuit optimization, it is quite natural for a subclass of these loops, the so-called constructive loops, to arise. These are loops that physically exist in a circuit, but are never logically taken. In this paper, we present a method for safety property verification of circuits containing constructive combinational loops, based on propositional theorem proving and temporal induction. It can be used to just prove constructivess of circuits, but also to directly prove safety properties of the circuits. Unlike previously proposed methods, no fixed point iteration is needed, we do not have to compute reachable states, and no cycle-free representation of the circuit has to be computed.

Nyckelord: synchronous programming, formal methods

Denna post skapades 2006-10-09. Senast ändrad 2013-02-28.
CPL Pubid: 2548


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)
Institutionen för datavetenskap, Funktionell programmering (2002-2004)


Information Technology

Chalmers infrastruktur