RTL数字系统的形式化描述  

Formal Description of RTL System

作　　者：张鹏飞[1] 

机构地区：[1]淮北师范大学计算机科学与技术学院,安徽淮北235000

出　　处：《安徽科技学院学报》2014年第6期41-46,共6页Journal of Anhui Science and Technology University

基　　金：淮北市科技局人才基金项目(20120309)

摘　　要：本文提出对寄存器传送语言(RTL)描述的数字系统运用投影时序逻辑进行形式化描述并验证的方法。通过使用投影时序逻辑对RTL的形式语义进行定义,可把一个用寄存器传输语言描述的系统转换成投影时序逻辑的公式,从而使用投影时序逻辑可执行子集MSVL对系统行为和性质进行形式化的描述及验证,提高系统设计的可信性。A formal approach of specification and verification of RTL system using PTL（ Projection Temporal Log- ic） is proposed in this paper. With this approach, RTL code＇ s formal semantics are defined with PTL, and then PTL and its executable subset （MSVL） can be used for formal specification and verification in the design of a system for increasing creditability of the design.

关 键 词：投影时序逻辑 形式化描述 寄存器传送语言 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]