A flexibilidade de fpgas sram é uma opção atrativa para o projeto de satélites artificiais. sistemas críticos como o mencionado requerem a verificação funcional do projeto em hdl (hardware description language). verificação formal utilizando model checking representa um sistema em um modelo formal que pode ser automaticamente gerado por ferramentas de síntese. no entanto, as propriedades que descrevem o comportamento esperado necessárias para provadores de modelo, são usualmente elaboradas de forma manual, o que é mais suscetível a erro humano, aumentando custo e tempo de verificação. este trabalho apresenta uma nova abordagem para geração automática de propriedades para verificação de sistemas descritos em hdl. o estudo de caso industrial é o subsistema de comunicação de um satélite artificial que foi desenvolvido em parceria com o instituto nacional de pesquisas espaciais (inpe).