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

【Abstract】 A method of the bound model checking(BMC) based on the polynomial theory was proposed to achieve model checking in the control chip of the forestry machinery and equipment.First,a unified description for the circuit function was proposed based on the polynomial theory.The traditional description method of the control logic of the circuit was developed to describe the circuit function with the polynomial theory.The polynomial was used to represent the atomic proposition,and the Boolean characteristic function was transformed into a set of polynomial.Therefore,the circuit function can be established with the polynomial.Second,through the relation model of the high level language,the extracting method of target property was proposed to get the description of the property with uniform polynomial of circuit function and target property.Based on above two points,the tradition BMC problem can be transferred into a problem of the theorem proving,and the set of polynomial triangular column is calculated to solve the theorem proving.BMC can be conducted directly at the high level abstract compared with the tradition methods.更多还原