Study on Model Checking for High-Level Hardware Design Descriptions

模型检验是一种验证硬件或软件设计正确性的技术，已经得到了广泛的应用。包含复杂算术运算的设计即使是小设计也很难处理。在本研究中，特别是对于高级设计描述，开发并实现了一种结合多种逻辑的方法，以抽象掉不必要的细节。因此，一些数字信号处理设计在模型检验方面变得容易处理。

Model checking is a technology for verifying the correctness of hardware or software designs, which has been widely used. Designs including complex arithmetic operations are hard to handle even for small designs. In this study, in particular, for high-level design descriptions, an approach that combines multiple logics has been developed and implemented, to abstract away unnecessary details. As a result, some digital signal processing designs have become tractable in term of model checking.