La verificación de hardware basada en propiedades proporciona una forma prometedora de descubrir vulnerabilidades de diseño. Sin embargo, desarrollar propiedades de seguridad que comprueben vulnerabilidades de seguridad altamente ocultas sigue siendo un desafío significativo. En este documento, proponemos un esquema, llamado HT-PGFV, para implementar la generación automática de afirmaciones de propiedades de seguridad de troyanos de hardware y la verificación formal de seguridad para diseños infectados por troyanos. En nuestro esquema, desarrollamos un método de generación de afirmaciones de propiedades de seguridad de troyanos de hardware para hardware automatizado que puede extraer propiedades de seguridad de troyanos de hardware de diseños infectados por troyanos realizando los tres pasos principales de identificación de señales infectadas por troyanos basada en coincidencia de características, identificación de rutas de troyanos basada en análisis de cono de influencia y minería de trazas de flujo de información, y formularlas como afirmaciones de SystemVerilog. Además, desarrollamos un método formal de verificación de seguridad basado en análisis de flujo de información que puede verificar formalmente propiedades de seguridad de troyanos de hardware y detectar troyanos de hardware que violan políticas de seguridad de flujo de información mediante la comprobación de la seguridad de flujos de información a través de nuestros modelos de seguridad de flujo de información de hardware a nivel de RT desarrollados. El método propuesto se demuestra en varios bancos de pruebas de troyanos de Trust-Hub. Los resultados experimentales muestran que nuestro esquema puede generar afirmaciones de propiedades de seguridad de troyanos de hardware para diseños infectados por troyanos y detectar fugas de información y cambios de funcionalidad de troyanos de hardware activados por entradas externas o condiciones internas.