Formal verification of embedded system designs at multiple levels of abstraction