Verification is an essential step of critical systems design flow with regard to safety and security. It supports respectively fault and vulnerability removal. Model-checking ensures that a design meets its specifications by using an exhaustive state exploration approach. It has been adopted to design critical and/or secure by design embedded hardware systems. On the one hand, model-checking is fully automated; on the other hand, it does not scale and faces state-space explosion when working with large industrial circuits and complex specifications. Compositional model-checking and theorem proving enable to verify large designs at the cost of finding abstractions and proving an implication of the specifications. In this paper, we present a method along with a framework to reduce this cost and improve hardware verification performances. We formally verified a hardware security monitor involved in a remote attestation scheme for microprocessors. This verification could not be achieved using classical approaches as it faces state-space explosion: the monitor is complex enough to be unfit for model-checking. So, we applied our method to the verification and successfully proved the security of remote attestation using symbolic model-checking and automatic theorem proving. Our verified security monitor is described with an hardware description language and its specifications are written in property specification language. Our method makes extensive use of compositional model-checking techniques to leverage the modular and partitioned aspects of most automata involved in hardware modelling. This method is fully automated in a framework build on top of free model checkers and automatic theorem provers. Automation relies on synthesis and translation tools which exploit the modular structure of sequential circuits and avoid having to re-design.