基于动态奖惩的CDCL SAT求解器分支启发式算法

分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。     

铁电晶体管近似搜索存储器的电流模测量实现EI北大核心CSCD

在高硬件容错性模型中,近似搜索可应对数据量与运算量需求能效提高的问题.针对三态内容寻址存储器在近似搜索模式下精度低、可扩展性差等问题,提出了一种电流模测量方案.该方案基于铁电晶体管优化了存储单元的结构设计以降低面积与功耗;将阵列搜索不匹配度由原先的电压输出改为电流输出,提高了电路可扩展性;引入了将模拟电流信号转化为数字脉冲信号的感测放大器(sense amplifier,SA)作为外围电路以检测存储阵列的不匹配度输出.通过Hspice与Virtuoso仿真平台搭建瞬态仿真电路实验,验证了该方案成功地实现了高能效三态内容寻址存储器近似搜索.     

基于FFT的泊松方程快速求解器的硬件实现

针对传统的泊松方程求解算法执行效率低、功耗大,很难满足实际需要的缺点,设计了一种FPGA硬件平台的泊松方程快速求解器。设计采用软件与硬件结合的方式,由软件执行控制复杂、计算量较小的任务,而由硬件完成控制简单、计算量大的任务,从而达到硬件加速的目的。在FPGA平台上,独立设计的FFT协处理器可以流水和高度并行化的处理数据,提高了求解器的性能。实验结果表明,硬件实现的基于FFT的泊松方程快速求解器具有较高的计算性能和良好的可扩展性。     

低功耗双边沿触发计数器的设计

该文从消除时钟信号冗余跳变而致的无效功耗的要求出发,提出了应用并行技术和流水线技术,实现基于RTL级的双边沿触发计数器的设计。经EDA软件模拟仿真和FPGA硬件验证,表明该计数器具有正确的逻辑功能,能够正常地应用于数字系统的设计。由于时钟工作频率减半及所需工作电压的降低,可使系统功耗明显减少。     

无界模型检验中融合电路信息的SAT算法研究

针对从电路转化而来的SAT问题.通用SAT求解器存在一个缺陷-电路互连信息的缺失,这是造成很多无关推导的根源.文中提出了一个统一的基于CNF数据结构的电路SAT无界模型检验框架.首先作者提出了定值子句的概念,利用这一概念可以在CNF结构中保存电路的互连信息,在搜索过程中更早地识别可满足解,减少不必要的搜索.其次,文中提出了在CNF结构上的状态变量赋值精简方法,摆脱了以往基于SAT的无界模型检验中这一步骤对门级电路结构的依赖.实验数据表明,利用文中方法进行前像计算能够取得明显的加速.同时,文章比较了两种搜索顺序在多时帧搜索中的效果.实验结果表明利用文中方法可以验证传统模型检验方法难以验证的复杂电路属性.     

基于FPGA的单轴数字磁通门传感电路设计

针对传统磁通门传感器模拟电路受温度影响较大的问题,设计了一种基于FPGA的单轴数字磁通门传感器。磁通门的模拟式传感电路由A/D转换器和FPGA取代,调制信号发生器、数字解调及滤波等环节均在FPGA内部编程实现。详细介绍了基于FPGA的磁通门传感电路硬件结构与软件设计,并进行了初步实验测试,证明了设计方案的可行性。     

精密离心机测控与加速度计标校自动化系统设计

惯导加速度计在精密离心机上的标校试验,涉及精密离心机动态半径和静态半径精密测量、转速精确测控以及被校加速度计信号的正确采集与实时传输等,需严格控制各类测控仪器的动作时序逻辑实现精密离心机测控与加速度计标校试验的自动化操作;介绍一种精密离心机测控与加速度计标校试验自动化系统设计,硬件上基于LAN总线组网集成精密离心机各类测控仪器,构建分布式测控系统,并应用外部光栅编码器脉冲信号作为触发信号控制测控仪器的硬件同步时序逻辑;软件上应用共享变量技术实现各类测控参数的有序传输,针对动态波形类大数据测试信号的共享变量传输可靠性差问题,提出一种基于文件动态拷贝的网络数据传输方案,设计严格的共享变量传输逻辑机制,实现了各类测控参数正确有序采集与传输;应用试验表明,设计的测控与加速度标校试验自动化系统满足加速度计在精密离心机上的标校自动化应用需求,显著提高了加速度计标校试验效率。      

一种基于SAT的运算电路查错方法

基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF,通过采用了标志子句技术的E-SAT求解器进行求解.实验表明该方法自动化程度高,能处理大规模的运算电路,有较强的查找错误能力.     

一种改进的基于FPGA的32位对数变换器的设计与实现

对数变换器是对数乘法器的重要组成部分,它们以精度换取更快的速度.设计并实现了一种基于FPGA的32位二进制对数变换器,主要由先导"1"检测电路、移位逻辑和误差校正电路组成,通过有效的误差校正算法提高了计算精度;给出了一种新的4位、16位和32位的基于FPGA的并行先导"1"检测电路PLOD,在保持低延时的同时,减小了先导"1"检测电路的功耗和面积;改进了现有的6-域校正算法,在提高精度的同时保持了硬件电路的规整性,降低了系统复杂度及面积和功耗开销;分两站流水实现校正操作,提高了系统的吞吐率;改进后的校正电路将对数操作的最大误差由30%降低到20%,区域1的平均误差大幅度降低.     

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

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

A survey of recent advances in SAT-based formal verification

Dramatic improvements in SAT solver technology over the last decade and the growing need for more efficient and scalable verification solutions have fueled research in verification methods based on SAT solvers. This paper presents a survey of the latest developments in SAT-based formal verification, including incomplete methods such as bounded model checking and complete methods for model checking. We focus on how the surveyed techniques formulate the verification problem as a SAT problem and how they exploit crucial aspects of a SAT solver, such as application-specific heuristics and conflict-driven learning. Finally, we summarize the noteworthy achievements in this area so far and note the major challenges in making this technology more pervasive in industrial design verification flows.     

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

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

直接数字频率合成技术在超声波振荡电路中的应用

针对传统的超声波振荡电路因采用模拟或数字自激振荡器存在输出频率不稳定的问题,提出了一种采用直接数字频率合成技术设计超声波振荡电路的方案,详细介绍了直接数字频率合成技术的基本工作原理以及采用该技术设计的超声波振荡电路的硬件和软件实现。实际应用表明,采用直接数字频率合成芯片AD9850设计的超声波振荡电路稳定可靠,并且不易受温湿度变化的影响,能解决矿用仪器仪表电路中超声波振荡电路的频率漂移问题。     

A BDD SAT solver for satisfiability testing: An industrial case study

The satisfiability problem (SAT) is a fundamental problem in mathematical logic, constraint satisfaction, VLSI engineering, and computing theory. Methods to solve the satisfiability problem play an important role in the development of computing theory and systems. In this paper, we give a BDD (Binary Decision Diagrams) SAT solver for practical asynchronous circuit design. The BDD SAT solver consists of a structural SAT formula preprocessor and a complete, incremental SAT algorithm that is able to find an optimal solution. The preprocessor compresses a large size SAT formula representing the circuit into a number of smaller SAT formulas. This avoids the problem of solving very large SAT formulas. Each small size SAT formula is solved by the BDD SAT algorithm efficiently. Eventually, the results of these subproblems are integrated together that contribute to the solution of the original problem. According to recent industrial assessments, this BDD SAT solver provides solutions to the practical, industrial asynchronous circuit design problems.This research is supported in part by the 1993 ACM/IEEE Design Automation Award, by the Alberta Microelectronics Graduate Scholarship, by the NSERC research grant OGP0046423, and was supported in part by the NSERC strategic grant MEF0045793.Presently, Jun Gu is on leave with the Department of Computer Science, Hong Kong University of Science and Technology, Clear Water Bay, Kowloon, Hong Kong.     

Simulating Circuit-Level Simplifications on CNF

Boolean satisfiability (SAT) and its extensions have become a core technology in many application domains, such as planning and formal verification, and continue finding various new application domains today. The SAT-based approach divides into three steps: encoding, preprocessing, and search. It is often argued that by encoding arbitrary Boolean formulas in conjunctive normal form (CNF), structural properties of the original problem are not reflected in the CNF. This should result in the fact that CNF-level preprocessing and SAT solver techniques have an inherent disadvantage compared to related techniques applicable on the level of more structural SAT instance representations such as Boolean circuits. Motivated by this, various simplification techniques and intricate CNF encodings for circuit-level SAT instance representations have been proposed. On the other hand, based on the highly efficient CNF-level clause learning SAT solvers, there is also strong support for the claim that CNF is sufficient as an input format for SAT solvers. In this work we study the effect of CNF-level simplification techniques, focusing on SatElite-style variable elimination (VE) and what we call blocked clause elimination (BCE). We show that BCE is surprisingly effective both in theory and in practice on CNF formulas resulting from a standard CNF encoding for circuits: without explicit knowledge of the underlying circuit structure, it achieves the same level of simplification as a combination of circuit-level simplifications and previously suggested polarity-based CNF encodings. We also show that VE can achieve many of the same effects as BCE, but not all. On the other hand, it turns out that VE and BCE are indeed partially orthogonal techniques. We also study the practical effects of combining BCE and VE for reducing the size of formulas and on the running times of state-of-the-art SAT solvers. Furthermore, we address the problem of how to construct original witnesses to satisfiable CNF formulas when applying a combination of BCE and VE.     

Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware

We propose to utilize a formal verification algorithm to reduce the fitness evaluation time for evolutionary post-synthesis optimization in evolvable hardware. The proposed method assumes that a fully functional digital circuit is available. A post-synthesis optimization is then conducted using Cartesian Genetic Programming (CGP) which utilizes a satisfiability problem solver to decide whether a candidate solution is functionally correct or not. It is demonstrated that the method can optimize digital circuits of tens of inputs and thousands of gates. Furthermore, the number of gates was reduced for the LGSynth93 benchmark circuits by 37.8% on average with respect to results of the conventional SIS tool.     

利用近似解加速求解SAT问题的启发式完全算法

结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.     

Analysing the Robustness of Surfing Circuits

Surfing is a technique for implementing high-speed digital pipelines that exploits the analog dynamics of the underlying circuits. Thus, verification must consider the analog behaviour of the design. We have presented a method for analysing the robustness of surfing circuits. We formulate noise margin analysis as a non-linear optimization problem where we find the smallest disturbance waveform that results in a qualitative change in the behavior of the circuit. We present a practical method for solving these optimization problems based on deriving a sensitivity matrix for the small-signal response of the circuit.