Institutional Repository
| 门电路和不动点模型 | |
| 陶猗萍 | |
| 1992 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 中国科学院软件研究所 |
| English Abstract | 一阶逻辑可以作为一种计算机硬件描述语言，它能严格描述数字设备的行为，对数字系统设计的正确性进行验证。本文提出了一种硬件描述及验证的方法：给出门电路（数字电路）波形传播的不动点模型，该模型可用UNITY[1]程序实现。并且，能用一阶逻辑来形式化描述及验证门电路波形传播的性质。作为这种方法的应用，本文给出了一个应用实例-形式化描述及验证D-触发器电路波形传播的性质。 |
| Abstract | 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. |
| Pages | 35 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/6838 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 陶猗萍. 门电路和不动点模型[D]. 中国科学院软件研究所. 中国科学院软件研究所,1992. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| N88257.pdf（1778KB） | 限制开放 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment