I. Introduction
Recent events on exploiting vulnerabilities of deployed systems rise concerns over security issues of implemented systems and even integrated circuit designs on silicon level. In a common design cycle there are several opportunities where malicious functionality, a so called hardware Trojan may be inserted. This could be achieved by an in-house “trusted” designer, by integrating external infected intellectual property (IP) cores[1] or generally by adding malicious functionality in the production phase. A hardware Trojan is commonly defined as a deliberate, malicious and undocumented modification (a physical circuit) of the silicon chip structure which has an eventually harmful impact on chip functionality [2]. Detection methodologies are starting to be evaluated as tailored countermeasures for future digital and mixed signal designs. This work investigates detection techniques concentrating on formal methods deduced from software verification, applied on pre-synthesized hardware models during design phase. Within these methods, a total Trojan absence can not be guaranteed, but a proposed “Trojan Assurance Level” (TAL) may be increased.