Efficient microprocessor verification using antecedent conditioned slicing

Shobha Vasudevan, Vinod Viswanath, Jacob A. Abraham

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a technique for automatic verification of pipelined microprocessors using model checking. Antecedent conditioned slicing is an efficient abstraction technique for hardware designs at the Register Transfer Level (RTL). Antecedent conditioned slicing prunes the verification state space, using information from the antecedent of a given LTL property. In this work, we model instructions of a pipelined processor as LTL properties, such that the instruction opcode forms the antecedent. We use antecedent conditioned slicing to decompose the problem space of pipelined processor verification on an instruction-wise basis. We pass the resulting smaller, tractable problems through a lower level verification engine. We thereby verify that every instruction behaves according to the specification and ensure that non-target registers are not modified by the instruction. We use the SMV model checker to verify all the instruction classes of a Verilog RTL implementation of the OR1200, an off-the-shelf pipelined processor.

Original languageEnglish (US)
Title of host publicationProceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems
Pages43-49
Number of pages7
DOIs
StatePublished - Dec 1 2007
Externally publishedYes
Event20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems, VLSID'07 - Bangalore, India
Duration: Jan 6 2007Jan 10 2007

Publication series

NameProceedings of the IEEE International Conference on VLSI Design
ISSN (Print)1063-9667

Other

Other20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems, VLSID'07
CountryIndia
CityBangalore
Period1/6/071/10/07

Fingerprint

Microprocessor chips
Computer hardware description languages
Model checking
Engines
Specifications
Hardware

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

Vasudevan, S., Viswanath, V., & Abraham, J. A. (2007). Efficient microprocessor verification using antecedent conditioned slicing. In Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems (pp. 43-49). [4092021] (Proceedings of the IEEE International Conference on VLSI Design). https://doi.org/10.1109/VLSID.2007.70

Efficient microprocessor verification using antecedent conditioned slicing. / Vasudevan, Shobha; Viswanath, Vinod; Abraham, Jacob A.

Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems. 2007. p. 43-49 4092021 (Proceedings of the IEEE International Conference on VLSI Design).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Vasudevan, S, Viswanath, V & Abraham, JA 2007, Efficient microprocessor verification using antecedent conditioned slicing. in Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems., 4092021, Proceedings of the IEEE International Conference on VLSI Design, pp. 43-49, 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems, VLSID'07, Bangalore, India, 1/6/07. https://doi.org/10.1109/VLSID.2007.70
Vasudevan S, Viswanath V, Abraham JA. Efficient microprocessor verification using antecedent conditioned slicing. In Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems. 2007. p. 43-49. 4092021. (Proceedings of the IEEE International Conference on VLSI Design). https://doi.org/10.1109/VLSID.2007.70
Vasudevan, Shobha ; Viswanath, Vinod ; Abraham, Jacob A. / Efficient microprocessor verification using antecedent conditioned slicing. Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems. 2007. pp. 43-49 (Proceedings of the IEEE International Conference on VLSI Design).
@inproceedings{8947ac9b0f8a4c06a11b51c41c8ed9d9,
title = "Efficient microprocessor verification using antecedent conditioned slicing",
abstract = "We present a technique for automatic verification of pipelined microprocessors using model checking. Antecedent conditioned slicing is an efficient abstraction technique for hardware designs at the Register Transfer Level (RTL). Antecedent conditioned slicing prunes the verification state space, using information from the antecedent of a given LTL property. In this work, we model instructions of a pipelined processor as LTL properties, such that the instruction opcode forms the antecedent. We use antecedent conditioned slicing to decompose the problem space of pipelined processor verification on an instruction-wise basis. We pass the resulting smaller, tractable problems through a lower level verification engine. We thereby verify that every instruction behaves according to the specification and ensure that non-target registers are not modified by the instruction. We use the SMV model checker to verify all the instruction classes of a Verilog RTL implementation of the OR1200, an off-the-shelf pipelined processor.",
author = "Shobha Vasudevan and Vinod Viswanath and Abraham, {Jacob A.}",
year = "2007",
month = "12",
day = "1",
doi = "10.1109/VLSID.2007.70",
language = "English (US)",
isbn = "0769527620",
series = "Proceedings of the IEEE International Conference on VLSI Design",
pages = "43--49",
booktitle = "Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems",

}

TY - GEN

T1 - Efficient microprocessor verification using antecedent conditioned slicing

AU - Vasudevan, Shobha

AU - Viswanath, Vinod

AU - Abraham, Jacob A.

PY - 2007/12/1

Y1 - 2007/12/1

N2 - We present a technique for automatic verification of pipelined microprocessors using model checking. Antecedent conditioned slicing is an efficient abstraction technique for hardware designs at the Register Transfer Level (RTL). Antecedent conditioned slicing prunes the verification state space, using information from the antecedent of a given LTL property. In this work, we model instructions of a pipelined processor as LTL properties, such that the instruction opcode forms the antecedent. We use antecedent conditioned slicing to decompose the problem space of pipelined processor verification on an instruction-wise basis. We pass the resulting smaller, tractable problems through a lower level verification engine. We thereby verify that every instruction behaves according to the specification and ensure that non-target registers are not modified by the instruction. We use the SMV model checker to verify all the instruction classes of a Verilog RTL implementation of the OR1200, an off-the-shelf pipelined processor.

AB - We present a technique for automatic verification of pipelined microprocessors using model checking. Antecedent conditioned slicing is an efficient abstraction technique for hardware designs at the Register Transfer Level (RTL). Antecedent conditioned slicing prunes the verification state space, using information from the antecedent of a given LTL property. In this work, we model instructions of a pipelined processor as LTL properties, such that the instruction opcode forms the antecedent. We use antecedent conditioned slicing to decompose the problem space of pipelined processor verification on an instruction-wise basis. We pass the resulting smaller, tractable problems through a lower level verification engine. We thereby verify that every instruction behaves according to the specification and ensure that non-target registers are not modified by the instruction. We use the SMV model checker to verify all the instruction classes of a Verilog RTL implementation of the OR1200, an off-the-shelf pipelined processor.

UR - http://www.scopus.com/inward/record.url?scp=48349101362&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=48349101362&partnerID=8YFLogxK

U2 - 10.1109/VLSID.2007.70

DO - 10.1109/VLSID.2007.70

M3 - Conference contribution

SN - 0769527620

SN - 9780769527628

T3 - Proceedings of the IEEE International Conference on VLSI Design

SP - 43

EP - 49

BT - Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems

ER -