Simulator Semantics for System Level Formal Verification
This addresses a foundational gap in formal verification for system-level design, though it appears incremental as it builds on existing simulation-based methods.
The paper tackles the problem of verifying system-level formal verification approaches that rely on simulators without formal semantics, by introducing a formal semantics for simulators to ensure correctness.
Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to save computation time by saving and restoring the state of the system under simulation. However, even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator behaviour is not formally modelled and the proof of correctness of the proposed approaches basically relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the optimisations introduced to speed up the simulation do not actually omit checking relevant behaviours of the system under verification. The aim of this paper is to fill the above gap by presenting a formal semantics for simulators.