吴丽佳，于 琼，靳庆庚

(广西民族大学 广西混杂计算与集成电路设计分析重点实验室，广西 南宁 530006)



一种基于System C语言的模型检测方法*

吴丽佳，于 琼，靳庆庚

(广西民族大学 广西混杂计算与集成电路设计分析重点实验室，广西 南宁 530006)

System C语言在软硬件协同设计过程中被广泛用来建模和仿真.笔者提出了一种验证System C设计的方法，即通过把System C设计映射成为一个具有良好定义语义的UPPAAL时间自动机.System C设计的结构和非正式定义的行为在形成的UPPAAL时间自动机中得到了完整的保留.产生的UPPAAL模型允许使用UPPAAL模型检查器和其配套工具来进行验证.模型检查器用来验证设计的一些重要属性，比如活性，死锁问题和时间约束属性.通过对两个实例的活性、安全性和时间属性的验证来证明该方法的适用性.

System C；时间自动机；模型检测

1 System C语言介绍

System C[1-3]语言是一种系统级的硬件描述语言，它继承和扩展了C++，这使得它可以建模不同抽象级别的包括软件和硬件的复杂电子系统，它既可以描述纯功能模型和系统体系结构，也可以描述软硬件的具体实现，但核心是进行电子系统级设计、建模和验证[2].System C具有所有硬件描述语言所共有的基本特征，包括模块、进程、端口和信号等.

一个System C设计的仿真语义可以总结为以下几个步骤：1)初始化：每个进程被执行一次；2)求值：所有待执行的进程以顺序被执行；3)更新：原始通道被更新；4)如果有△延迟通知，则相应的进程被触发并重复步骤2)和3)；5)如果有定时时间通知则仿真时间被推进到响应的定时通知并且重复步骤2)～4)；……