中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
门电路和不动点模型
作者: 陶猗萍
答辩日期: 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:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
N88257.pdf(1778KB)----限制开放-- 联系获取全文

Recommended Citation:
陶猗萍. 门电路和不动点模型[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1992-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[陶猗萍]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[陶猗萍]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace