Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs
Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs
复制标题
用于验证高级设计的信号转换一致性的符号检查
DOI：
10.1007/3-540-40922-x_28
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
T. Kashiwabara
中科院分区：
文献类型：
--
作者：
K. Hamaguchi;Hidekazu Urushihara;T. Kashiwabara
本文论述了高层次设计的验证，特别是寄存器传输级描述和行为描述的符号比较。作为这些描述的模型，我们使用状态机扩展的无量词的一阶逻辑与平等。由于这种描述的相应输出中的信号很少同时变化，因此我们不能采用状态机的经典等价概念。本文定义了一种基于相应输出的信号转换的一致性概念，并提出了一种从初始状态到有限步的一致性检验算法。一个简单的硬件/软件协同设计作为一个例子，高层次的设计。本文介绍了一个用于数字信号处理的C语言程序PARCOR滤波器，并给出了相应的寄存器传输级设计，该设计由VLIW结构和汇编代码组成。由于该示例在大约4500个步骤内终止，因此有限数目的步骤的符号探索足以验证描述。我们的原型验证器在31分钟内成功验证了该示例。
This paper deals with verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. As models of those descriptions, we use state ma- chines extended by quantifier-free first-order logic with equality. Since the signals in the corresponding outputs of such descriptions rarely change simultaneously, we cannot adopt the classical notion of equivalence for state machines. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algo- rithm for checking consistency of those descriptions, up to a limited num- ber of steps from initial states. A simple hardware/software codesign is taken as an example of high-level designs. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite num- ber of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.