Hardware Trojans hidden in RTL don´t cares ? Automated insertion and prevention methodologies

Don´t cares in RTL code have long plagued chip verification due to hard-to-diagnose “X-bugs” resulting from ambiguous X simulation semantics, yet prevail in modern designs because of enormous opportunities for area/performance/power optimization during synthesis. We analyze don´t cares specified at the RTL level from a security perspective and propose a novel class of Hardware Trojans which leak internal circuit node values using only existing design don´t cares. Detection of this Trojan class is impossible using either functional simulation/verification or a perfect sequential equivalence checker. We then provide a formal automated X-analysis technique which both prevents the insertion of this new Trojan type and also has the potential to uncover accidental X-bugs as well. We provide several examples, including an Elliptic Curve Processor, illustrating both Trojan insertion and our prevention technique.