利用SMT约束分解方法求解RTL可满足性问题

随着集成电路技术与工艺的不断发展,目前工业界所采用的形式验证工具已很难适应集成电路规模的飞速增长.为了对RTL电路的可满足性问题进行形式验证,提出基于超图划分的约束分解实现可满足性模理论(SMT)求解的分级验证方法.通过分析RTL电路的结构约束,对约束集合中的元素和相关变量进行约束建模,并构建带有合适权重的超图模型;利用超图划分的机制寻找带有最小割集的等量划分,实现约束分解,完成RTL电路的定界模型检验.实验结果表明,该方法能够减小处理问题的规模和求解过程中的搜索空间,提高验证效率.     

采用二元CSP引擎求解RTL数据通路的可满足性

针对寄存器传输级(RTL)验证和测试过程中非常重要的数据通路可满足性求解问题,提出一种基于二元约束满足问题(CSP)的求解方法,包括数据通路提取、二元CSP建模和搜索求解3个步骤.数据通路提取通过对接口布尔变量和某些字变量赋值,为各个数据通路器件建立环境;二元CSP建模则根据该环境和各个数据通路器件的功能,将数据通路的可满足性问题转化为二元CSP描述;该二元CSP问题的描述被送入到二元CSP引擎,并采用冲突引导的回跳搜索策略进行求解,获得有解的例证或无解的判定.实验结果表明,即使在没有采取很多优化策略的条件下,该方法仍有较好的性能,并优于基于线性规划(LP)的求解方法.     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

RTL验证中的混合可满足性求解

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.     

LDPChecker一个实时和混成系统模型检验工具

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模．虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机．其对于线性时段性质的满足性能够通过线性规划方法加以检验．为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker．工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息．     

RTL数据通路模拟矢量自动生成方法研究与实现

针对已有的RTL数据通路模拟矢量自动生成方法的不足，提出一种利用约束逻辑编辑(CLP)自动生成数据通路模拟矢量的新方法．该方法首先对给定的Verilog RTL描述采用程序切片进行设计化简，然后对化简后的结果基于位向量算术原理生成CLP约束，并利用CLP求解器GProlog进行约束求解，最终生成满足输出要求的模拟矢量．该方法约束求解速度快，生成的约束是统一的，得到的模拟矢量较完备，能满足模拟验证的要求．实验结果表明，文中方法是一种高效的RTL数据通路模拟矢量自动生成方法．     

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.     

龙芯2号微处理器浮点除法功能部件的形式验证

基于决策图的字级模型检验方法虽然能完全验证运算电路,但它从有缺陷的设计中发现系统规范的反例所需时间较长．而基于SAT的有界模型检验方法虽然能较快地发现反例,但它不支持包含数学公式的系统规范,因而难以用于验证运算电路．提出了基于SAT的字级模型检验方法,该方法将CNF扩展为能混合布尔公式和数学公式的E—CNF用以表示设计和系统规范,并对有界模型检验工具和SAT求解器进行字级的扩展,使它们能分别生成和处理E—CNF．龙芯2号微处理器浮点除法功能部件验证同时采用了基于＊PHDD和基于SAT的字级模型检验方法．数据表明,基于SAT的字级模型检验方法能快速地发现运算电路中的设计缺陷．两种方法互为补充,在能完全验证设计的同时显著缩短了设计周期．     

可满足性求解器中一种可观无关性利用方法

为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.     

基于一阶逻辑的可满足求解方法研究进展

基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。     

Debugging Larch shared language specifications

The checkability designed into the LSL (Larch shared language) is described, and two tools that help perform the checking are discussed. LP (the Larch power) is the principal debugging tool. Its design and development have been motivated primarily by work on LSL, but it also has other uses (e.g. reasoning about circuits and concurrent algorithms). Because of these other uses, and because they also tend to use LP to analyze Larch interface specifications, the authors have tried not to make LP too LSL-specific. Instead, they have chosen to build a second tool, LSLC (the LSL checker), to serve as a front-end to LP. LSLC checks the syntax and static semantics of LSL specifications and generates LP proof obligations from their claims. These proof obligations fall into three categories: consistency (that a specification does not contradict itself), theory containment (that a specification has intended consequences), and relative completeness (that a set of operators is adequately defined). An extended example illustrating how LP is used to debug LSL specifications is presented     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

Encoding RTL Constructs for MathSAT: a Preliminary Report

Formal checking at Register-Transfer Level (RTL) is currently a fundamental step in the design of hardware circuits. Most tools for formal checking, however, work at the boolean level, which is not expressive enough to capture the abstract, high level (e.g., structural, word level) information of RTL designs. Tools for formal checking are thus confronted with problems which are “flattened” down to boolean level, so that a predominant part of their computational effort is wasted in performing useless boolean search on the bitwise encoding of integer data and arithmetical operations. In this paper we present a way of encoding RTL constructs into SMT formulas, that is, boolean combinations of boolean variables and quantifier-free constraints in Integer Linear Arithmetic. Such formulas can be handled by the MathSAT tool (and others) directly, without flattening to boolean level, so that to reduce drastically the computational effort.We propose a mixed boolean/ILP encoding, in which control variables are encoded as boolean variables, datapath variables as integer variables; control constructs are handled as boolean combination of control variables and predicates over datapath variables, and datapath constructs are encoded, as much as possible, as linear arithmetical constraints over datapath variables.     

形式验证中同步时序电路的VHDL描述到S2-FSM的转换

符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ,ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法．由于验证时间和有限状态机模型的大小是直接相关的,因而模型的大小就成为ＳＭＣ中的关键问题．本文提出一种基于同步电路行为描述的新的有限状态机模型Ｓ２－ＦＳＭ,并给出从同步电路的ＶＨＤＬ描述建立这种模型的过程．由于该模型的状态转换函数是基于时钟周期的,消去了与时钟无关的大量中间变量,所以同Ｄｅｈａｒｂｅ提出的模型相比,它的状态数大大减少．若干电路的实验结果表明,该模型由于减少了状态规模,建模时间和可达性分析时间大大减少,效果十分显著．     

UC-based Approximate Incremental Reachability

In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in safety-critical areas. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This study analyzes and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, Unsatisfiable Core (UC)-based Approximate Incremental Reachability (UAIR), mainly utilizes the UC to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, this study uses the UC obtained by the satisfiability solver to construct the candidate safety invariant, and if the transition system itself is safe, the obtained initial invariant is only an approximation of the safety invariant. Then, while checking the safety, the study incrementally improves the candidate safety invariant until it finds a true invariant that proves the system is safe; if the system is unsafe, the method can finally find a counterexample to prove the system is unsafe. The brand new method exploits UCs for safety model checking and achieves good results. It is known that there is no absolute best method in the field of model checking. Although the proposed method cannot surpass the current mature methods such as IC3 and complement Approximate Reachability (CAR), in terms of the number of solvable benchmarks, the method in this paper can solve three cases that other mature methods are unable to solve. It is believed that the method can be a valuable addition to the model checking toolset.     

An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems

This paper presents a bounded model checking tool called Hydlogic{\texttt{Hydlogic}} for hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Our Hydlogic{\texttt{Hydlogic}} implementation successfully handled several examples including those with nonlinear constraints.     

地方财政收费稽查选案系统的研究与设计

收费稽查的计算机选案，是指根据科学的选案指标，以计算机为辅助工具，对现有的内外部收费信息进行加工处理、分析筛选，以发现存在收费异常的执收单位。该文提出了基于决策树的财政收费稽查选案模型，提出了支持收费稽查选案的元数据组织方法，阐述了稽查选案主题的提取方法和多维模型构建的方法，并将决策树方法应用于收费的稽查选案。基于收费稽查的选案模型，设计并实现了收费稽查计算机选案系统，提高了收费稽查工作的准确性和科学性。     

Symbolic model checking for self-stabilizing algorithms

A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors