Sciweavers

Share
VLSID
2007
IEEE

Efficient Microprocessor Verification using Antecedent Conditioned Slicing

13 years 2 months ago
Efficient Microprocessor Verification using Antecedent Conditioned Slicing
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-t...
Shobha Vasudevan, Vinod Viswanath, Jacob A. Abraha
Added 30 Nov 2009
Updated 30 Nov 2009
Type Conference
Year 2007
Where VLSID
Authors Shobha Vasudevan, Vinod Viswanath, Jacob A. Abraham
Comments (0)
books