现代片上系统（SoCs）的复杂性不断增加，使得在短时间内交付可靠且可信的芯片变得越来越具有挑战性。特别是在测试芯片的情况下，其目的是研究设计的可行性，时间成为一个关键因素。硅前功能验证是产品开发周期中的主要贡献者之一。验证工程师通常对测试芯片进行松散的验证，这些芯片在硅上最终无法正常工作，最终导致昂贵的重新设计。为了将验证工作提前，形式验证是一种强大的方法，旨在全面验证设计，从而提高整体质量的信心。本文重点研究了一种混合信号知识产权（IP）的实用形式验证，该IP结合了数字和模拟模块。本文讨论了一种将模拟行为模型纳入形式验证设置的新方法。数字和模拟混合信号（AMS）设计在本质上存在根本差异，但在形式验证设置中无缝集成，这一概念可以称为“模拟对齐”。我们的形式验证设置利用了强大的形式技术，如FPV、CSR验证和连接性检查。用于FPV的属性是使用元建模框架自动生成的。本文还讨论了所面临的挑战，特别是与状态空间爆炸、形式验证与AMS模型的不兼容性以及缓解这些问题的技术（如k-归纳法）相关的问题。通过这种验证方法，我们能够在合理的时间内全面验证设计，并达到足够的覆盖率。我们还报告了在早期阶段发现的几处错误，使得整个设计验证过程变得迭代且有效。