### Skapa referens, olika format (klipp och klistra)

**Harvard**

Claessen, K. (2003) *Safety Property Verification of Cyclic Synchronous Circuits*.

** BibTeX **

@conference{

Claessen2003,

author={Claessen, Koen},

title={Safety Property Verification of Cyclic Synchronous Circuits},

booktitle={Electronic Notes in Theoretical Computer Science. SLAP 2003: Synchronous Languages, Applications and Programming, A Satellite Workshop of ECRST 2003, Porto, 1 July 2003},

pages={55-69},

abstract={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.},

year={2003},

keywords={synchronous programming, formal methods},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 2548

A1 Claessen, Koen

T1 Safety Property Verification of Cyclic Synchronous Circuits

YR 2003

T2 Electronic Notes in Theoretical Computer Science. SLAP 2003: Synchronous Languages, Applications and Programming, A Satellite Workshop of ECRST 2003, Porto, 1 July 2003

SP 55

OP 69

AB 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.

LA eng

DO 10.1016/j.entcs.2003.05.004

LK http://dx.doi.org/10.1016/j.entcs.2003.05.004

OL 30