由于功能单一、结构相对简单,传统嵌入式控制器只需采用一般的验证方法即可完全覆盖产品的功能测试。而主要应用于金融业的嵌入式外设控制器的设计,则很难沿用原来的验证方法完全覆盖产品的功能测试。为此本课题提出结合模型检测与验证方法学,对金融领域嵌入式外设控制器进行全覆盖测试验证的方法进行研究。本文研究了国内外在硬件验证与模型检测的现状和相关技术,包括验证方法学分析,基于SystemVerilog验证关键技术以及模型检测硬件验证相关技术分析;之后对模型检测建模方法进行研究,其中包括用例模型转化状态模型方法研究,状态模型转化为nuSMV模型方法及其转换规则研究;然后又对模型检测属性设计方法进行研究,其中包括属性提取方法研究、属性分解方法研究,以及属性设计方法研究;最后进行实例分析,以实际开发项目A类点钞机为平台,对接触式图像传感器控制器进行用例建模、状态建模、nuSMV建模,用模型检测进行验证并产生反例,通过反例不断修改接触式图像传感器控制器,最终设计出稳定性好的接触式图像传感器控制器。本课题通过使用基于模型检测的验证方法完成了接触式图像传感器控制器的设计,解决了项目中接触式图像传感器控制器采集图像不稳定,图像质量差的问题。以后,在硬件设计领域基于模型检测的验证方法应用会越来越广泛。