Using Abstract Specifications to Verify PowerPCTM Custom Memories by Symbolic Trajectory Evaluation
Using Abstract Specifications to Verify PowerPCTM Custom Memories by Symbolic Trajectory Evaluation
复制标题
使用抽象规范通过符号轨迹评估来验证 PowerPCTM 自定义存储器
DOI：
10.1007/3-540-44798-9_30
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
M. Abadir
中科院分区：
文献类型：
--
作者：
J. Bhadra;Andrew K. Martin;J. Abraham;M. Abadir
我们提出了一种方法，在该方法中，使用抽象的参数化正则表达式指定的开关级设备的行为。这些规范用于生成有限自动机，表示由一组这样的交换机级设备组成的存储器块的行为的抽象。该自动机与器件的高效内存模型[1]、[2]结合，形成了一个符号仿真模型，表示嵌入在分析中的更大设计中的阵列核心的抽象。使用符号轨迹评估，我们checktheequivalence之间的寄存器传输级的描述和原理图的描述与抽象规范增强嵌入在MPC7450 PowerPC处理器的自定义存储器之一。
We present a methodology in which the behavior of a switch level device is specified using abstract parameterized regular expressions. These specifications are used to generate a finite automaton representing an abstraction of the behavior of a blockof memory comprised of a set of such switch level devices. The automaton, in conjunction with an Efficient Memory Model [1], [2] for the devices, forms a symbolic simulation model representing an abstraction of the array core embedded in a larger design under analysis. Using Symbolic Trajectory Evaluation, we checkthe equivalence between a register transfer level description and a schematic description augmented with abstract specifications for one of the custom memories embedded in the MPC7450 PowerPC processor.