The advancements in electronic systems and technology miniaturization have revolutionized the world in the last couple of decades. The higher complex ity of modern designs, economic constraints, and unprecedented pressure of time-to-market dictate the rationale of Integrated Circuit (IC) manufacturing from the third-party fabrication facilities. This rising trend of globalization in circuit design using nanoscale process technologies has increased their vulner ability against malicious intrusions and modifications. Such modifications, also referred as Hardware Trojans (HTs), can lead to highly detrimental con sequences like causing a circuit to subvert normal operation, leak sensitive information or inducing Denial of Service (DoS). These emerging issues are imposing formidable threats to security-critical applications particularly in the domains of military, communications, and Internet of Things (IoT). The conventional side channel analysis-based HT detection techniques mostly rely on simulations, which are typically exhaustive and computationally intensive. Moreover, it takes substantial resources and time for all-encompassing veri fication and analysis of the circuits. In this thesis, we apply the strengths of formal verification to complement simulation-based HT detection techniques by detailed behavioral analysis of circuits at the early stage of design. Formal methods are conclusive and well-established techniques which are used for description of complex sys vi vii tems in the form of mathematical models, and then use those models for rigorous analysis. In particular, we present a model checking-based formal framework that is broadly used to: (i) mathematically model an individual circuit for its functional and behavioral verification; (ii) analyze and quan tify vulnerability of a region in circuit against different types of HTs using multiple side-channel parameters; and (iii) identification of secure bounds for circuit operations in terms of its side-channel parameters. The outcome of the formal framework is used to design side channel-based sensor that comprehends the behavior of the circuit using a machine learning technique while incorporating the impacts of random process variations. The proposed framework serves to achieve the primary thesis goal of implanting intelligent sensor leveraging rigorous a-priori assessment of IC characteristics. The im plemented sensor can be subsequently used for post deployment identification of the HT-infected IC. To illustrate the practical effectiveness of the proposed infrastructure, we present the detailed analysis of multiple benchmark circuits. The formal framework and automated analysis technique, formulated during this thesis, proved effective in examining the impacts of malicious intrusions on multi ple side-channel parameters. Moreover, it provides flexibility in identifying the appropriate sensing units to incorporate security in the circuits while minimizing additional hardware.