论文部分内容阅读
本文提出对寄存器传送语言（RTL）描述的数字系统运用投影时序逻辑进行形式化描述并验证的方法。通过使用投影时序逻辑对RTL的形式语义进行定义，可把一个用寄存器传输语言描述的系统转换成投影时序逻辑的公式，从而使用投影时序逻辑可执行子集MSVL对系统行为和性质进行形式化的描述及验证，提高系统设计的可信性。