评论摘要(共 0 条，得分 0 分，平均 0 分)
摘要：Pi演算已经在软件工程，Web服务等领域有了广泛的应用，取得很多的研究成果。该文尝试用Pi演算对数字电路进行仿真，分析数字电路的性质，为Pi演算在数字电路和芯片设计领域的应用基础。
关键词：Pi演算；数字电路；符号仿真
A Checking Approach for Digital Circuit Based on Pi-Calculus
LIU Rong-Sheng
(Department of Information Engineering, Hunan Railway Professional Technology College, Zhuzhou 412001, China)
Abstract: Pi-calculus has been applied in many fields, such as software engineering, Web services, and a lot of research results have been got. The Pi-calculus is used to simulate and analysis the digital circuit. The paper is the base for applying Pi-calculus to designing of digital circuit and chips.
Key words: Pi-calculus; digital circuit; symbolic simulation
在具体的系统设计中，由于集成电路器件十分复杂，为便于在实际制作之前观察设计结果，以确认电路能否满足设计要求，需要对设计电路进行仿真分析[1]。现在常用的数字电路系统仿真工具有Matlab、Verlog HDL、Spice和ModelSim等。但是使用这些工具对系统进行仿真分析时，准确的描述系统较为困难。MWB是一款支持Pi演算进行模型验证的工具软件，我们已经分别将基于MWB的验证技术应用于Web服务、移动计算等领域，取得了不错的验证效果。但是犹豫软件系统的复杂性，以及形式化验证技术中状态爆炸的问题，验证问题规模非常有限，在这里我们尝试使用MWB用于数字电路设计的验证。
1 MWB简介
MWB是一款基于Pi演算对移动系统进行形式化建模和验证的工具，其中需要验证的系统采用Pi演算进行建模，Pi演算的语法和语义分别如定义1及定义2所示。
定义1. 类型化Pi-演算语法
定义2. 类型化Pi-演算的规约语义
其中Г为进程c![y1,…,yn].R+S的类型上下文环境；
Δ为进程P+c?[x1,…,xm].Q的类型上下文环境
有关Pi演算更进一步的知识，可参考文献[2]。
2 Pi演算在数字电路设计中的应用
我们在设计电路时，需要知道一些重要的特性是否被满足[3]。如果用Mu演算公式描述设计人员想要的验证的特性。当电路的结构已知时，这个问题变可转换成Mu演算模型检验问题。在数字电路的设计中经常要使用的逻辑门电路有与、或、非和异或门等，为验证方便，先将这些基本的逻辑门用Pi演算公式表示如图1所示。
我们用模4计数器的例子说明MWB模型检验在数字电路设计中的应用。模4计数器数字电路的设计图如图2所示。
图2所示数字电路可以用Pi演算描述如图3所示。
系统的性质是希望v1与v0依次循环输出序对（0,0），（0,1），（1,0），（1,1）。通过对Pi演算表达式使用Pi演算规约语义进行推演，任意给定以上四个序对中的一个作为v1与v0的初始状态，都能依次得到上面4个序对的循环。因此设计符合设计要求。
3 总结
Pi演算已经在Web服务，软件工程等领域有了广泛的研究和应用，在这里我们尝试使用Pi演算对数字电路进行仿真检验。通过研究为Pi演算在数字电路设计领域的应用奠定了一个基础。
参考文献：
[1] 李哲英,骆丽.数字集成电路设计[M].北京:机械工业出版社,2008:30-31.
[2] 刘荣胜,高春鸣,黄邵.基于类型化Pi-演算的web服务组合相容性检测[J].计算机工程与应用,2007(3).
[3] 刘建元.数字电路设计中的符号模型验证技术[J].微电子学与计算机,2002(10).
本文由星论文网提供，星论文网提供资料均为独家发行，因水平高而被多家网站争先转载，转载请注明出处：http://www.starlunwen.com/article/html/list42-1.html
星网文化传媒中心( http://www.starlunwen.com/)，是一个专门从事期刊推广、计算机论文发表、计算机论文代写指导的机构
