In this paper, an efficient equivalence checking method for two C descriptions is described. The equivalence of two C descriptions is proved by symbolic simulation. Symbolic simulation used in this paper can prove the equivalence of all of the variables in the descriptions. However, it takes long time to verify the equivalence of all of the variables if large descriptions are given. Therefore, in order to improve the verification, our method identifies textual differences between descriptions. The identified textual differences are used to reduce the number of equivalence checkings among variables. The proposed method has been implemented in C language and evaluated with several C descriptions.
展开▼
机译:该文描述了一种针对两种C描述的高效等价性检查方法。通过符号模拟证明了两个C描述的等价性。本文使用的符号模拟可以证明描述中所有变量的等价性。但是,如果给出大量描述,则需要很长时间来验证所有变量的等价性。因此,为了提高验证效果,我们的方法识别了描述之间的文本差异。识别出的文本差异用于减少变量之间的等价检查次数。所提出的方法已用 C 语言实现,并使用多个 C 描述进行评估。
展开▼