| 题名: | 门电路和不动点模型 |
| 作者: | 陶猗萍
|
| 答辩日期: | 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. |
| 语种: | 中文
|
| 内容类型: | 学位论文
|
| URI标识: | http://ir.iscas.ac.cn/handle/311060/6838
|
| Appears in Collections: | 中科院软件所
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| N88257.pdf（1778KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
陶猗萍. 门电路和不动点模型[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1992-01-01.
|
|
|
