| 林业机械设备控制芯片设计的模型检验方法 |
| |
| 引用本文： | 范德会,马光胜.林业机械设备控制芯片设计的模型检验方法[J].东北林业大学学报,2013,41(2):93-98,122. |
| |
| 作者姓名： | 范德会 马光胜 |
| |
| 作者单位： | 哈尔滨工程大学,哈尔滨,150001 |
| |
| 基金项目： | 黑龙江省教育厅科学技术研究项目(12511373) |
| |
| 摘 要： | 为解决林业机械设备控制芯片设计中模型检验问题,提出基于多项式理论的定界模型检验方法.首先,给出基于多项式形式的电路功能的统一描述.为了能够采用多项式形式描述电路功能,在传统的电路控制逻辑描述方法的基础上,将其进一步扩展,将传统方法中的原子命题转化为多项式形式,将布尔特征函数转化为多项式集合的形式.这样,可以与电路数据通路部分建立统一的多项式描述形式.其次,通过建立高级语言的关系模型,给出了电路在高层次描述中目标性质的抽取方法,通过该方法形成待验证性质的多项式形式描述,从而形成了待验证性质与电路功能统一的多项式形式.基于以上两点,将定界模型检验问题转化为基于多项式理论的定理证明问题.并采用计算多项式集合良好三角列的方法解决定理证明问题.与传统方法相比,该方法可在电路高级别抽象上直接进行定界模型检验.
|
| 关 键 词： | 林业机械 控制芯片 模型检验 多项式 电子设计自动化 |
Model Checking Method in Control Chip of the Forestry Machinery and Equipment |
| |
| Fan Dehui
,
Ma Guangsheng.Model Checking Method in Control Chip of the Forestry Machinery and Equipment[J].Journal of Northeast Forestry University,2013,41(2):93-98,122. |
| |
| Authors: | Fan Dehui Ma Guangsheng |
| |
| Institution: | (Harbin Engineering University,Harbin 150001,P.R.China) |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
