求形式验证方面的资料，非等效性分析

最近学习 形式验证 方面的知识，苦于没有工具，只好看文档，但是缺乏一个统一的demo 参照。
不知道坛子里有么有大神给个 model checking的完全demo给小弟参考一下，或者纯文档资料也行，但一定要讲解详细，如果是 step by step 就最好了。