论文导读：如：硬件描述语言（VerilogHDL或VHDL）来进行设计。用VerilogHDL采门级描述为：。简介。。VerilogHDL的ITL形式语义及其应用。
关键词：硬件描述语言，VerilogHDL，ITL，Tempura
1、引言
几十年前，人们所做的复杂数字逻辑电路及系统的设计规模比较小也比较简单，其中所用到的FPGA或ASIC设计工作往往只能采用厂家提供的专用电路图输入工具来进行。为了满足设计性能指标，工程师往往需要花好几天或更长的时间进行艰苦的手工布线。硕士论文，ITL。工程师还得非常熟悉所选器件的内部结构和外部引线特点，才能达到设计要求。这种低水平的设计方法大大延长了设计周期。
近年来，FPGA 和ASIC 的设计在规模和复杂度方面不断取得进展，而对逻辑电路及系统的设计的时间要求却越来越短。硕士论文，ITL。这些因素促使设计人员采用高水准的设计工具，如：硬件描述语言（Verilog HDL 或VHDL）来进行设计。
然而，Verilog HDL 硬件描述语言缺乏对于电路逻辑关系描述和分析的形式化方法，尤其是缺乏基于时序的逻辑描述。这对于化简和检验正确性都带来了麻烦。而ITL语言描述则提供了另一套基于时序的形式化解决方法，对Verilog HDL 硬件描述语言起到了很好的补充作用。
2、ITL简介
区间时态逻辑(interval Temporal logic，ITL)是一种用于描述离散区间或时段的逻辑系统，它是时态逻辑的一个分支。我们可以把一个区间(interval)看作是一个有限的状态序列;这里的状态就是从所有变量到其值的映射。区间的长度定义为该区间内状态数减 1。因此，只含有一个状态的区间的长度为0。一个区间s0… sn 的长度是n。一个只有单个状态的区间的长度是0。
ITL 的基本表达式和公式的语法如下所示
表达式：
公式：
其中，μ为一个整数值;a 为静态变量(在区间内不改变);A 为状态变量(在区间内
值可变);g 是函数符号;p 为谓词。硕士论文，ITL。下面我们以RS 触发器为例来说明ITL的使用：
一个RS 触发器是一个简单的储存和保持一位数据的记忆单元。两个输入决定了互补的输出 和 。S（Set）为置一，R（Reset）为置零。
 
图1 RS 触发器结构图图2 RS 触发器的真值表
按照传统的方法，根据真值表列出输入输出变量的逻辑方程，得到：
Qn+1=S+￢R*Qn
S*R=0
而用 ITL描述可以直接把逻辑关系（动作、谓词）写出来，再化简：
把时间等参数变量考虑进去，我们就可以得到RS触发器的结构方程：
3、Tempura
用ITL 能够方便准确地描述基于时序的数字电路，然而缺乏可执行能力，运算公式不能直接进行计算机仿真和验证。Tempura 则是ITL 强有力的可编程可执行的工具集，大大增强了ITL 的实用性。Tempura 是一种可直接执行的数字电路时序逻辑设计方式，是 ITL 的一个可执行子集。发展到今天，Tempura 已经能够直接在Windows 环境下运行。硕士论文，ITL。只要熟悉ITL 的语句，对照着Tempura 自带的指导工具，使语法公式一一对应就可以进行编程和仿真，十分方便。硕士论文，ITL。
下面我们还是以RS 触发器为例来说明
用VerilogHDL采用门级描述为：
moduleRS_FF(R,S,Q,QB);
input R,S;
output Q,QB;
nor (Q,R,QB);
nor (QB,S,Q);
endmodule
用VerilogHDL采用行为描述为：
moduleRS_FF(R,S,Q,QB);
input R,S;
output Q,QB;
reg Q;
assign QB=~Q;
always@(R or S)
case({R,S})
2'b01:Q<=1;
2'b10:Q<=0;
2'b11:Q<=1'bx;
endcase
endmodule
而根据前文所述的用 ITL描述的RS触发器改写成Tempura 语言，代码如下：
为了检验设计结果，需要输入仿真参量，代码如下：
(S=0) and (R=0)and (Q=0) and (Qbar=0) and
for lis<<1,0>,<0,0>,<0,1>,<1,0>,<0,0>>
do (len(5)and (Sgets l0) and (R gets l1)
)
and
(S,R)latch(Q,Qbar)
仿真结果如下，和真值表一样。
图3 仿真结果
传统的数字电路设计方法繁琐且不严谨，而且往往缺乏时序逻辑的描述能力。针对这个问题，HDL的使用为硬件设计师提供了一个非常好的分析和设计数字硬件的工具，也为沟通软件和硬件提供了一种方法。然而，这些 HDL 一般是为模拟数字硬件的功能而设计，往往比较适用于较低层级的设计。同时传统的HDL 设计方法缺乏对数字硬件推理和证明的机制；对行为描述的能力较弱，缺乏形式设计或验证的支持工具。形式化的设计方法则提供另一种强有力的数字电路描述。在软件工程中，形式方法已经取得一些引人注目的成就。但是在硬件设计领域，形式方法的应用研究和成就仍然在起步阶段。在国内的面向市场的数字电路设计，情况更是这样，形式方法的使用很是有限。ITL 等形式方法（特别是配以成熟高效的可执行工具，如Tempura）， 将有效提高我们描述和设计数字电路。硕士论文，ITL。正如本文开头所说，在硬件设计速度赶不上软件速度的今天，形式方法将给我们带来一种新的突破思路，这在未来的电路设计领域将有广阔的应用和发展空间。
参考文献
[1]Benjamin C. Mosszkowski. ITL HandbookDecember 6, 2007
[2]Antonio Cau. Interval Temporal Logic Anot so short introduction 2009
[3]舒风笛。《面向嵌入式实时软件的需求规约语言及检测方法》，武汉大学，2004
[4]夏宇闻。《Verilog 数字系统设计教程》，2008年，北京：北京航天航空大学出版社。
|
