Invariance Checking Based Trojan Detection Method for Three-Dimensional Integrated Circuits