TDM／TDMA比特同步系统研究

本文根据 TDM/TDMA 扩频移动通信的特点,提出了一种性能优越而实用的比特同步系统.文中介绍了其主要原理,给出了有关理论、实验结果以及波形照片.值得提出的是:本同步系统亦适用于非时分系统.     

基于数字锁相环的新型频相检测方法研究

在经典DPLL(数字锁相环)的基础上,提出了一种在中频过采样背景条件下利用过采样值进行相位捕捉和跟踪的新型数字锁相环。该方法利用两级鉴频器实现频率锁定,同时利用高频过采样实现数字锁相,对相位误差一步调整到位而不需连续多次调整。最后讨论了波形失真和随机抖动的影响;利用相对阈值法使性能得到很大改善。该方法解决了锁定精度和锁定时间不能同时兼顾以及抗干扰能力差等若干问题。     

锁相环频率合成器的方案研究

频率合成技术是现代通信的重要组成部分,在无线电技术与电子系统的各个领域中均得到广泛的应用。分析了MC145152芯片的特点和功能,结合外围电路设计了909~915 MHz步进25 kHz的"吞除脉冲"式数字锁相频率合成器,该频率合成器具有结构简单、性能稳定、精度高、易实现等特点。并且满足了通信设备的高集成度和超小型化的要求,特别适合某些特殊场合的应用。     

DPLL在高频逆变电源中的分析与设计

采用基于DSP的数字锁相环(DPLL)对高频逆变电源输出频率的实时控制，可实现逆变器工作频率对负载谐振频率的同步跟踪，确保逆变器开关器件工作在零电压电流软开关(ZVZCS)状态，显著减小功率器件的开关损耗和提高装置效率。本文在给出DPLL控制的逆变电源拓扑结构基础上，推出了适用于高频逆变电源的锁相环数学模型，在Z域中对二阶数字锁相环进行了稳定性分析和动态设计。在对锁相环Z域传递函数分析的基础上，得出二阶数字锁相环的稳定条件，并用MATLAB对其进行了仿真分析，最后进行了实验验证。仿真和实验结果表明在Z域中对基于DSP的二阶数字锁相环的动态分析和设计是合理可行的，用此方法设计的电源具有良好的动态响应和抗扰性能。     

嵌入式数字锁相环的设计与实现

介绍了应用VHDL技术设计嵌入式数字锁相环的方法，给出了系统仿真结果，并用可编程逻辑器件FPGA予以实现。该锁相环能够实现正交锁定或反相锁定，并具有控制灵活、锁定频率高和系统稳定性好等特点。     

数字中频感应加热电源的研究

针对传统模拟中频控制系统的不足,对新型数字中频控制系统进行了研究和设计。提出一种基于DSP DS80C320微控制器为控制核心,主开关元件采用IGBT的数字感应加热系统,设计了系统的主电路、控制电路的结构。针对串联型感应加热电源频率跟踪的要求,阐述了一种新型的数字锁相环(DPLL)控制方法,并对相位补偿与启动问题进行了探讨,最终给出了实验电路和实验结果。实际应用证明具有功率调节范围宽、频率变化小的优点,适用于在中频感应加热中的应用。     

Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.     

求解极小SMT不可满足子式的宽度优先搜索算法

极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.     

SMT求解技术简述

SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重介绍并分析了这些技术,包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点,包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望,量词的处理、优化问题和解空间大小的计算等尤其值得关注。     

Modelling and solving temporal reasoning as propositional satisfiability

Representing and reasoning about time dependent information is a key research issue in many areas of computer science and artificial intelligence. One of the best known and widely used formalisms for representing interval-based qualitative temporal information is Allen's interval algebra (IA). The fundamental reasoning task in IA is to find a scenario that is consistent with the given information. This problem is in general NP-complete.In this paper, we investigate how an interval-based representation, or IA network, can be encoded into a propositional formula of Boolean variables and/or predicates in decidable theories. Our task is to discover whether satisfying such a formula can be more efficient than finding a consistent scenario for the original problem. There are two basic approaches to modelling an IA network: one represents the relations between intervals as variables and the other represents the end-points of each interval as variables. By combining these two approaches with three different Boolean satisfiability (SAT) encoding schemes, we produced six encoding schemes for converting IA to SAT. In addition, we also showed how IA networks can be formulated into satisfiability modulo theories (SMT) formulae based on the quantifier-free integer difference logic (QF-IDL). These encodings were empirically studied using randomly generated IA problems of sizes ranging from 20 to 100 nodes. A general conclusion we draw from these experimental results is that encoding IA into SAT produces better results than existing approaches. More specifically, we show that the new point-based 1-D support SAT encoding of IA produces consistently better results than the other alternatives considered. In comparison with the six different SAT encodings, the SMT encoding came fourth after the point-based and interval-based 1-D support schemes and the point-based direct scheme. Further, we observe that the phase transition region maps directly from the IA encoding to each SAT or SMT encoding, but, surprisingly, the location of the hard region varies according to the encoding scheme. Our results also show a fixed performance ranking order over the various encoding schemes.