Verification

This chapter emphasizes the critical need for thorough verification of embedded systems, building upon the advantages of SystemC models outlined in the previous chapter. SystemC models, being modular and offering multiple abstraction layers, serve as ideal early evaluation and reference models for hardware/software co-design. As SystemC Virtual Prototypes (VPs) are internally C/C \(++\) models, the proposed approaches take advantage from the well-established set of tools in computer science. Two main verification categories, hardware-centric and software-centric, are discussed, utilizing simulation-based and formal techniques. The industry emphasizes early hardware model verification to detect specification, design, and implementation flaws promptly. The chapter introduces novel verification approaches for real-world SystemC TLM peripherals using symbolic execution tools, cross-level verification of actual RTL models against TLM counterparts, and a pioneering method for early and accurate Dynamic Information Flow Tracking (DIFT) of binaries targeting embedded systems with custom peripherals. The effectiveness is demonstrated through extensive experiments, including security policy violation detection and analysis of an AES encryption peripheral.