Sciweavers

Share
FMCAD
1998
Springer

Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification

9 years 16 days ago
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification
We present a new approach to the verification of hardware systems with data dependencies using temporal logic symbolic model checking. As a benchmark we take Tomasulo's algorithm [10] for out-of-order instruction scheduling. Our approach is similar to the idea of uninterpreted function symbols [4]. We use symbolic values and instructions instead of concrete ones. This allows us to show the correctness of the machine independently of the actual instruction set architecture and the implementation of the functional units. Instead of using first order terms as in [4], we represent symbolic values with a new compact encoding. In addition, we apply some other reduction techniques to the model. This significantly reduces the state space and allows the use of highly efficient symbolic model checkers like SMV instead of special decision procedures. The correctness of the method has been proven formally with the PVS theorem prover.
Sergey Berezin, Armin Biere, Edmund M. Clarke, Yun
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where FMCAD
Authors Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu
Comments (0)
books