林业机械设备控制芯片设计的模型检验方法

编号 zgly0000811022

文献类型 期刊论文

文献题名 林业机械设备控制芯片设计的模型检验方法

作者 范德会  马光胜 

作者单位 哈尔滨工程大学 

母体文献 东北林业大学学报 

年卷期 2013(2)

页码 93-98

年份 2013 

分类号 S776.02 

关键词 林业机械  控制芯片  模型检验  多项式  电子设计自动化 

文摘内容 为解决林业机械设备控制芯片设计中模型检验问题, 提出基于多项式理论的定界模型检验方法。首先, 给出基于多项式形式的电路功能的统一描述。为了能够采用多项式形式描述电路功能.在传统的电路控制逻辑描述方法的基础上, 将其进一步扩展, 将传统方法中的原子命题转化为多项式形式.将布尔特征函数转化为多项式集合的形式。这样, 可以与电路数据通路部分建立统一的多项式描述形式。其次.通过建立高级语言的关系模型, 给出了电路在高层次描述中目标性质的抽取方法, 通过该方法形成待验证性质的多项式形式描述.从而形成了待验证性质与电路功能统一的多项式形式。基于以上两点, 将定界模型检验问题转化为基于多项式理论的定理证明问题。并采用计算多项式集合良好三角列的方法解决定理证明问题。与传统方法相比.该方法可在电路高级别抽象上直接进行定界模型检验。