| 门电路和不动点模型 |
| 陶猗萍
|
| 1992
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 摘要 | 一阶逻辑可以作为一种计算机硬件描述语言，它能严格描述数字设备的行为，对数字系统设计的正确性进行验证。本文提出了一种硬件描述及验证的方法：给出门电路（数字电路）波形传播的不动点模型，该模型可用UNITY[1]程序实现。并且，能用一阶逻辑来形式化描述及验证门电路波形传播的性质。作为这种方法的应用，本文给出了一个应用实例-形式化描述及验证D-触发器电路波形传播的性质。 |
| 其他摘要 | First-order logic can be adapted for describing hardware: it allow behaviours of digital devices to be rigorously specified, and correctness of digital system designs to be formally verified. The approach in the paper to specification and verification of hardware is based on the first-order logic. As a case study of this approach, a behavioured specification for and edgetriggered D-type flipflop is formulated, and the correctness of a commonly used implementation of the flipflop is verified. |
| 页数 | 35
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/6838
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
陶猗萍. 门电路和不动点模型[D]. 中国科学院软件研究所. 中国科学院软件研究所,1992.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论