A Model-checking Approach for HDL Descriptions Using Data Dependency Analysis
Waseem Muhammad, Mohammed Omer · Infotech@Aerospace 2012 · 2012
Embedded systems used in avionics and spacecraft industry require high degree of condence in functionality and performance. Traditional simulation based testing methods cannot guarantee the systems behavior under all circumstances. Formal verication is used to verify the functionality of critical embedded system. We present a verication technique based on static formal analysis of data paths in RTL and gate level designs in Verilog and VHDL (HDL descriptions).