资源描述：
《SPIN在同步时序逻辑中的应用》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、计算机科学2005Vo1.32Ns.8(增刊)SPIN在同步时序逻辑中的应用ApplicationofSPINinSynchronousSequentialLogicCircuits章超李彩虹李廉(兰州大学信息科学与工程学院兰州730000)AbstractSPINisamodelcheckerwhichtargets.efficientsoftwareverification.ThispaperpresentsanapplicationofSPINinsynchronoussequentiallogicci
2、rcuitswhicharedesignedwithVerilogHDL.Inordertousesoftwareverifi-cationtoolstoassisthardwaredesign,twocircuitsaremodelledinPROMELAandverifiedwithSPIN.KeywordsSynchronoussequentiallogiccircuits,Verilog,SPIN,PROMELA有错误为止。1引言2应用实例同步时序逻辑是指表示状态的寄存器组的值只可能在唯一确定的触发条
3、件发生时改变，而异步时本节讲述了如何将SPIN应用到同步时序逻辑序逻辑是指触发条件由多个控制因素组成，任何一中。鉴于说明问题的方便，也限于篇幅，这里选取两个因素的跳变都可以引起触发。同步时序逻辑比异个较小的同步时序逻辑电路作为实例。在解题的过步时序逻辑具有更可靠、更简单的逻辑关系，因此在程当中，给出详细的分析过程，并重点讲解了实际设计中应尽量避免使用异步时序逻辑。PROMELA建模过程，最后用SPIN验证了电路的Ve'rilogHDI.是目前应用最广泛的一种硬件描某些LTL属性。述语言，用于数字电子系统设计。
4、用VerilogHDL例1用Verilog设计一个微波炉(micro-设计的可综合模块，必须避免使用异步时序逻辑，这wave)，满足下列要求:不但是因为许多综合器不支持异步时序逻辑的综使用微波炉前，先打开门(opendoor)，然后放合，而且也因为用异步时序逻辑确实很难来控制由人食物，最后关上门(closedoor)。不要将金属容器组合逻辑和延迟所产生的冒险和竞争。放人炉中。按下开始(start)按钮，微波炉将加热SPIN是贝尔实验室开发的一个优秀的模型检(heat)30秒，然后开始烹饪(cooking)。一
5、旦烹饪结验器，主要面向分布式软件系统的验证。SPIN的束(done)，则微波炉停止工作(stop)。在烹饪过程规范语言是PROMELA，并使用线性时序逻辑中打开门微波炉也会停止工作。如果打开门的时候(LTL)表示属性，使用偏序规约方法来减少系统状微波炉已经开始工作，则会发生错误(error)，此时要用到重置(reset)按钮。态规模。解:①根据题目要求，用Verilog描述micro-借助协议验证工具来辅助硬件设计的观点早在wave的状态机如下:文〔1」中就已经提出来了。按照这种思想，本文将modulemic
6、rowave(clock,reset,openDoor,closeDoor,SPIN应用到硬件设计中做了有益的尝试。我们选done);取实际设计中广泛使用的同步时序逻辑作为研究对inputclock;inputreset,openDoor,closeDoor,done;象，并采用Verilog来描述同步时序逻辑。具体的regStart,Close,Heat,Error;initialbegin做法是:先根据电路要求设计出同步时序逻辑的Start=0;Close=0;Verilog描述，为了应用SPIN验证其正
7、确性，须将Heat=0;Error=0;其转换成等价的PROMELA模型，接着用SPIN来End验证该PROMELA模型是否满足电路所需的性质。always@(posedgeclock)begincase({Error,Heat,Close,Start))如果发现错误，则需对原来的设计(Verilog描述)进4'1)0000:if(closeDoor)行修改，然后重新建模、验证，重复这一过程直到没{Error,Heat,Close,Start)二4'1)0010:章超硕士研究生，研究方向:软硬件的形式化验证。
8、李彩虹硕士研究生研究方向:数字硬件的形式化验证。李廉博士生导师。3·else{Error=0;Heat=0;Close=l;Start=l)‘Error,H4ea'bt1,洁一Start’一4'b]001，fi::(Error二二0)&-(Heat二二0)&.(Close二=1)冬,(Start(Error,Heat,Close,Start}二4'b1011;=二1)一，atomic4'61011:
