Schammer, LutzLutzSchammerMartino, GianlucaGianlucaMartinoFey, GörschwinGörschwinFey2025-09-032025-09-032025-0328th Workshop "Methods and Description Languages for Modeling and Verification of Circuits and Systems", MBMV 2025https://hdl.handle.net/11420/57209Information Flow Analysis (IFA) is an established approach to understand designs and their vulnerabilities with respect to information leaks. Dynamic simulation-based analysis methods have been proposed and are widely used due to their computational efficiency. However, they may miss to identifiy all possible information flow in a design. On the other hand less scalable formal IFA is exact, but may not be capable of analyzing larger designs. The actual comparison has not been done before. We compare formal and dynamic analysis to investigate the trade-offs. We give examples of their limitations. We explain how IFA runs using a solver for Satisfiability Modulo Theories (SMT) and show experimental results demonstrating the effects on real designs.enTechnology::600: TechnologyConference PaperConference Paper