Here we illustrate our approach through the verification of an ARM CoreSight flow trace decompresser using symbolic model-checking of temporal logic and automatic theorem proving. Details are provided in paper "An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs", ERTS 2022: Embedded Real Time Systems, 30-31 March 2022, Toulouse, France -------------------------------------------------------------------------------- The goal is to prove that, for all "i" in range 0 to (1 << 7*8)-1, having input "in" set to "i" by sets of 8 bits (when "enable" is set) implies that output "data" is set to "i" when "ready" rises. We prove this specification from 7 local properties (to be verified with model-checking) available in files "abstract_*/property.smv". The proof is separated in 3 steps: - first step is to use uninterpreted functions abstraction to relieve the automatic theorem prover in solving the satisfiability problem: all functions "next_event_a()[j:j]()" and "next_event()()" are abstracted to booleans. This task is performed in folders "abstract_*". This step is unnecessary since abstraction is proven correct with coq: see folder "coq". - second step is to prove the implication of 2 intermediate properties, by sets of 3 or 4 bytes, where we merge uninterpreted functions into one boolean. This task is performed twice (to cover all 7 bytes) in folders "proof_01" and "proof_02". - third step is to finally prove the specification from 2 intermediate properties. This task is performed in folder "proof_final". To run the proof, several possibilities: - we can verify uninterpreted functions abstraction for all the 7 properties. This is long and unnecessary. But it can be done by running "make full". - we can only verify uninterpreted functions abstraction for the 2 first properties, then rely on the proof written in coq for all other 5 properties. This is quicker and can be done by running "make". - once we verified uninterpreted functions abstraction. We can also try to run the proof in only one step. This is longer and can be done by running "make one_step". Makefiles assume that Spot is installed in folder "/usr/local/lib/python3.7/site-packages/". Path to access Spot can be changed in file "Rules.mk".