Towards the formal verification of optical interconnects

Optical solutions have been proposed for on-die interconnect utilizing the speed-of-light signal propagation and the large bandwidth of the waveguides. However, the inability to efficiently analyze photonic devices, which are continuous in nature, using traditional analysis approaches somewhat limits their applications. In this paper, we present the formalization of two of the most widely used structures in optical interconnect systems, i.e., the planar waveguide and Fabry-Pérot cavity, using a higher-order-logic theorem prover. The proposed formalization can be utilized to precisely analyze many fundamental components of an optical interconnect system.