UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Combining stream-based and state-based verification techniques

Day, NA; Aagaard, MD; Cook, B; (2000) Combining stream-based and state-based verification techniques. In: (pp. pp. 126-142).

Full text not available from this repository.

Abstract

© Springer-Verlag Berlin Heidelberg 2000. Algebraic verification techniques manipulate the structure of a circuit while preserving its behavior. Algorithmic verification techniques verify properties about the behavior of a circuit. These two techniques have complementary strengths: algebraic techniques are largely independent of the size of the state space, and algorithmic techniques are highly automated. It is desirable to exploit both in the same verification. However, algebraic techniques often use stream-based models of circuits, while algorithmic techniques use state-based models. We prove the consistency of stream- and state-based interpretations of circuit models, and show how stream-based verification results can be used hand-in-hand with state-based verification results. Our approach allows us to combine stream-based algebraic rewriting and state-based reasoning, using SMV and SVC, to verify a pipelined microarchitecture with speculative execution.

Type: Proceedings paper
Title: Combining stream-based and state-based verification techniques
ISBN: 3540412190
ISBN-13: 9783540412199
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: http://discovery.ucl.ac.uk/id/eprint/1490876
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item