Signal processing is an emerging area of research which provides the basis to build high-speed communcation systems. 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 researhc project, 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). Our main focus is both electronic and photonic signal processing systems. Following are two main active projects in our group at this time.

Current Projects

• Formal Analysis of Photonic Signal Processing Systems
• Formal Anlysis of Discrete-Time Linear Systems
• Formal Error Analysis and Verification of the Frequency Domain Equalizer

Past Projects

• Modeling and Verification of DSP Designs in HOL