DATE
2004
IEEE
2004
IEEE
Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements
14 years 4 months ago
We show how to automatically verify that complex XScale-like pipelined machine models satisfy the same safety and liveness properties as their corresponding instruction set archit...