Formal methods have been advocated for the verification of digital design where correctness is proved mathematically. In contrast to digital designs, the verification of analog and mixed signal systems is a challenging task that requires lots of expertise and deep understanding of their behavior. In this paper, we present a run-time verification methodology based on monitoring the behavior (solution flow) of analog circuits. Monitors are deterministic timed automata that can be synthesized from temporal properties. For illustration purposes, we applied our methodology on the verification of the oscillation property of a tunnel diode oscillator. Categories and Subject Descriptors B.7.2 [Integrated Circuits]: Design Aids—Verification General Terms Verification
Mohamed H. Zaki, Sofiène Tahar, Guy Bois