电子电路设计随着大规模集成电路的迅速发展而受到了广泛的关注，并取得了一定的研究进展，但是还是远远赶不上大规模集成电路的发展速度，成为了电子电路产业中发展的滞后点，传统的电路验证已经远远的不能满足现在大规模集成电路的需求，需要更加快速和更大规模的验证算法及验证平台，形式化方法应运而生。本文主要在广义符号赋值算法的研究和实现上做出了一定的工作，主要实现了以广义符号赋值算法为验证基础的验证平台。现今已有的验证平台中伯克利大学开发的VIS和公司流行使用的Cospan等验证平台都是基于CTL和LTL语言描述验证性质的平台，广义符号赋值算法则是基于断言图描述验证性质的平台，弥补了这两个平台在一些验证问题上的缺陷。本文中设计出的平台填补了在形式化验证领域中没有基于广义符号赋值算法验证平台的空白，更加的完善了在形式化验证领域的验证平台的种类，使得在解决不同问题时有了更多的选择，可以通过对比时间和空间复杂度来选用一款比较适合解决这类问题的平台本文首先会简单的介绍广义符号赋值算法的背景以及发展历史，接下来会介绍VIS验证平台，并完成对我们自己设计的验证平台的介绍，然后会介绍在平台实现中对广义符号赋值算法的重点难点问题的解决和实现，以及一些在研究和实现以广义符号赋值算法为基础的验证平台时对算法的创新点。电路设计验证过程中最重要的一点是找到电路设计是否满足设计者所设想的要求，在广义符号赋值算法中是通过对模型和性质的抽象，来验证模型是否满足性质的方法来验证电路设计的正确性。算法中的核心是找到不动点或出错点，若算法找到不动点，则电路满足设计者所提要求；若算法找到出错点，则根据设计的回溯算法找出错误路径，提示用户沿着这条路径，电路设计中会出现不满足设计者要求的结果。最后在进行研究的过程中，发现平台依然存在一些问题，在求解一些大规模的电路过程中，会遇到一些时间上和空间上不足的问题，这些问题也是当今流行的验证软件同样很难解决的问题，在平台设计技术以及编码技术上的改进不能在根本上去解决这个问题，而解决这个问题的根本方法是在算法上的创新，如果算法上能够把解决这类问题的时间复杂度控制在多项式时间范围内，才能真正的完成在有限时间内完成对大规模集成电路的验证工作。在最后给出基于广义符号赋值算法的验证平台下一步的改进方案和建议，以便能够更好的完善验证平台，能够更好的适应现今大规模集成电路的发展速度。