Photonic signal processing is an emerging area of research, which provides unique prospects to build high-speed communication devices. Recent advancements in the fabrication technology allow on-chip manufacturing of such signal processing devices. This poses an additional challenge of accurate modeling and analysis due to the complex nature of light and optical components. In this paper, we propose to use higher-order-logic theorem proving to improve the analysis accuracy by overcoming the known limitations of incompleteness and soundness of existing approaches (e.g., paper-and-pencil based proofs and simulation). In particular, we formalize the notion of transfer function using the signal-flow-graph theory which is the most fundamental step to model photonic circuits. Consequently, we formalize and verify the important properties of the stability and the resonance of photonic circuits.

HOL Code:

Download Page