The General Product Machine: a New Model for Symbolic FSM Traversal

Proving the equivalence of two Finite State Machines (FSMs) has many applications to synthesis, verification, testing, and diagnosis. Building their product machine is a theoretical framework for equivalence proof. There are some cases where product machine traversal, a necessary and sufficient check, is mandatory. This is much more complex than traversing just one of the component machines. This paper proposes an equivalence-preserving function that transforms the product machine in theGeneral Product Machine (GPM). Using the GPM in symbolic state space traversal reduces the size of the BDDs and makes image computation easier. As a result, GPM traversal is much less expensive than product machine traversal, its cost being close to dealing with a single machine.     

时序电路等价性检验中的存储元素映射方法研究

随着集成电路规模越来越大,系统的功能日益复杂,功能验证已成为整个设计流程的瓶颈.对于大规模的时序电路,传统基于状态空间遍历的等价性检验方法可能会遇到内存爆炸问题.为了降低等价性检验方法的复杂度,提高验证效率和处理大规模电路的能力,通常需要构造两个被验证电路的存储元素映射之间的映射关系,从而将时序电路等价性检验问题转化为组合电路等价性检验问题.较全面地介绍了时序电路等价性检验的基本方法及其研究进展,讨论了基于存储元素映射的时序电路等价检验方法的基本思想,并介绍了若干具有代表性的存储元素映射方法,展望了集成电路等价检验方法的研究发展方向.     

Binary particle swarm optimization (BPSO) based state assignment for area minimization of sequential circuits

State assignment (SA) for finite state machines (FSMs) is one of the main optimization problems in the synthesis of sequential circuits. It determines the complexity of its combinational circuit and thus area, delay, testability and power dissipation of its implementation. Particle swarm optimization (PSO) is a non-deterministic heuristic that optimizes a problem by iteratively trying to improve a candidate solution with regard to a given measure of quality. PSO optimizes a problem by having a population of candidate solutions called particles, and moving them around in the search-space according to a simple mathematical formulae. In this paper, we propose an improved binary particle swarm optimization (BPSO) algorithm and demonstrate its effectiveness in solving the state assignment problem in sequential circuit synthesis targeting area optimization. It will be an evident that the proposed BPSO algorithm overcomes the drawbacks of the original BPSO algorithm. Experimental results demonstrate the effectiveness of the proposed BPSO algorithm in comparison to other BPSO variants reported in the literature and in comparison to Genetic Algorithm (GA), Simulated Evolution (SimE) and deterministic algorithms like Jedi and Nova.     

Checking Combinational Equivalence of Speed-Independent Circuits

We introduce the notion of combinational equivalence to relate two speed-independent asynchronous (sequential) circuits: a golden hazard-free circuit C ₁ and a target circuit C ₂ that can be derived from C ₁ through only combinational decomposition and extraction. Both circuits are assumed to be networks of single-output basic gates; multiple output gates such as arbiters, toggles, and dual-rail function blocks are not considered. We say that the circuits are combinationally equivalent if the decomposition and extraction preserves the essential functionality of the combinational blocks in the circuit and does not introduce hazards. The paper's focus is the bottleneck of the verification procedure, checking whether C ₂ is hazard-free. We show that C ₂ is hazard-free if and only if all of its signals are monotonic and acknowledged . We then show how cubes that approximate sets of reachable circuit states can be used to give sufficient conditions for monotonicity and acknowledgement. These sufficient conditions are used to develop a verification technique for combinational equivalence that can be exponentially faster than applying traditional, more general verification techniques. This result can be useful for verifying logic synthesis and technology mapping procedures.     

Structural decomposition as a tool for the optimization of an FPGA-based implementation of a mealy FSM

Two models of logic circuits are proposed for the implementation of Mealy FSMs. The models are underlain by FPGAs with embedded memory blocks and are based on a transformation of object codes. To decrease the number of lookup table elements, it is proposed to decrease the number of irregular functions representing FSMs. An example of design and results of experiments are given for the proposed synthesis method based on the transformation of codes of collections of microoperations into state codes of FSMs.     

Studying the separability relation between finite state machines

Several authors have studied the relationships between non‐deterministic finite state machines (FSMs). These relationships can be used, for example, for deriving conformance tests from specifications represented by FSMs. In this paper, the separability relation between FSMs is studied. In particular, an algorithm is presented that derives a shortest separating sequence of two non‐deterministic FSMs. Given FSMs S with n states and T with m states, it is shown that the upper bound on the length of a shortest separating sequence is 2^mn−1. Moreover, the upper bound is shown to be reachable. However, according to the conducted experiments, on average, the length of a shortest separating sequence of FSMs S and T states is less than mn and the existence of a separating sequence significantly depends on the number of non‐deterministic transitions in these FSMs. The proposed algorithm can also be used for deriving a separating sequence of two different states of a single FSM or for deriving a separating sequence of three or more FSMs. Copyright © 2007 John Wiley & Sons, Ltd.     

Synthesis of finite state machines for improved state verification

Finite State Machines (FSMs) are used in diverse areas to model hardware and software systems. Verification of FSMs is essential to ensure reliability of systems. To verify that a machine is in an expected state in testing, Unique Input/Output (UIO) sequences are used. The aforementioned testing methodology requires that each state in the FSM has an UIO. However, it is possible for a given machine that few or even none of its states have an UIO sequence. This paper presents a guided heuristic algorithm for synthesizing FSMs such that each state has an UIO sequence. The states of an FSM with identical I/O labels on transitions are grouped in order to identify the states which do not possess UIO sequence. The transitions are then augmented by adding extra output terminals incrementally so that new UIO sequences are created for the states. A greedy approach is used to optimize the number of added outputs. Initially, the transitions which lead to state convergence (i.e., transitions with identical input/output labels taking a set of states to the same next state) and constrained self-loop (i.e., transitions taking a set of states either to itself or leads to state convergence) are identified since a state with only these transitions will never have a UIO sequence. Extra output terminals are added to the FSM which are used only while testing and the augmented output labels make sure that the states are neither convergent nor has constrained self-loop, thereby ensuring UIO sequence. The proposed algorithm, referred to as AUGP, was tested with a large number of FSMs including the Microelectronics Center of North Carolina (MCNC) FSM benchmarks. The augmented state transition table was used as input to a UIO computation algorithm (developed by the same authors [Ahmad I, et al. IEE Proc Comput Digital Tech 2004;151(2):131]) to check the performance of the augmentation algorithm and the tested FSMs were found to possess UIO sequence for all states.     

基于Verilog HDL的高速可综合FSM设计

有限状态机（finite state machine,FSM）广泛应用于数字系统的控制器设计中,用Verilog设计的可综合状态机有多种编码风格,通常这些编码风格生成的状态机带有组合逻辑输出.时序分析指出组合逻辑输出型状态机不适合高速系统,提出了一种适合高速系统的寄存器输出型状态机.最后通过实例给出了寄存器输出型状态机的状态编码方法及其可综合Verilog编码风格.     

From Pre-Historic to Post-Modern Symbolic Model Checking

Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating expressions that represent state sets. Traditionally, symbolic model-checking tools are based on backward state traversal; their basic operation is the function pre, which, given a set of states, returns the set of all predecessor states. This is because specifiers usually employ formalisms with future-time modalities, which are naturally evaluated by iterating applications of pre. It has been shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which, given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only parts of the state space that are reachable from an initial state and relevant for the satisfaction or violation of the specification are explored; that is, errors can be detected as soon as possible.In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation, and the post- calculus is based on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.     

Logic programming and digital circuit analysis

We show how the unique character of logic programming can be exploited for the purpose of specifying and automatically reasoning about electrical circuits. Although propositional logic has long been used for describing the truth functions of combinational circuits, the more powerful predicate calculus on which logic programming is based has seen relatively little use in design automation. Previous researchers have introduced a number of techniques similar to logic programming, but many of the useful consequences of the methodology have not been demonstrated. We describe particular consequences of using this method for writing directly executable specifications of circuits, including the use of quantified variables, verification of hypothetical states, and sequential simulation. We have used these methods to solve problems in gate assignment, specialization of standard definitions, and determination of signal flow.     

Constructive Boolean circuits and the exactness of timed ternary simulation

We classify gate level circuits with cycles based on their stabilization behavior. We define a formal class of combinational circuits, the constructive circuits, for which signals settle to a unique value in bounded time, for any input, under a simple conservative delay model, called the up-bounded non-inertial (UN) delay. Since circuits with combinational cycles can exhibit asynchronous behavior, such as non-determinism or metastability, it is crucial to ground their analysis in a formal delay model, which previous work in this area did not do.     

Formula-Dependent Equivalence for Compositional CTL Model Checking

We present a polytime computable state equivalence that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser equivalences. This equivalence can be used to reduce the complexity of model checking a system of interacting FSMs. Additionally, we show that in some cases our techniques can detect if a formula passes or fails, without forming the entire product machine. The method is exact and fully automatic, and handles full CTL.     

划分有限状态机的低功耗实现模型

通过引入映射状态,使得单状态机的状态分配算法可直接应用于被划分的有限状态机,提出了实现划分有限状态机的通用物理模型.对13个MCNC基准电路,采用文中模型进行测试,实验结果与已发表的结果相比,文中模型在功耗和面积的改进方面有一定的优势.     

基于重定时的时序逻辑优化策略

提出了一种去除同步时序电路中冗余逻辑的方法．针对时序冗余难于识别的问题,这种方法引入重定时技术,将电路中的时序冗余转换为冗余的组合逻辑,然后利用已有的比较成熟的组合逻辑优化工具将具去除．这样避免了提取电路的状态表及电路状态空间的遍历,从而能够大大降低时序电路冗余识别和支除的复杂度．将相关算法应用于ＩＳＡＳ’８９基准电路集,结果验证了其有效性。     

Modeling Combinational Circuits Using Linear Word-level Structures

In many applications of circuit design and synthesis, it is natural and in some instances essential to manipulate logic functions and model circuits using word-level representations and arithmetic operations in contrast to bit-level representations and logic operations. This paper reviews linear word-level structures and formulates their properties for combinational circuit modeling. The paper addresses the following problem: given a library of gates with their corresponding word-level representations such as linear arithmetic expressions or respective graph structures, find a word-level model of an arbitrary combinational circuit/netlist using that library of gates and minimizing memory allocation and time delay requirements. We present a comprehensive study on linearization assuming various circuit processing strategies. In particular, we develop a new approach to manipulate linear word-level representations by means of cascades. The practical applicability of linear structures and developed algorithms is strengthen by considering the problem of timing analysis. All this is supported by the experimental study on benchmark circuits.     

基于电路拓扑结构分析的等价性验证方法

随着集成电路设计规模的日益增大,结合多种推理引擎已成为组合电路形式化等价性验证的重要手段.提出一种基于电路拓扑结构分析的组合等价性验证方法,将电路的拓扑结构与验证算法的复杂性关联起来.在验证过程开始之前,利用min-cut方法计算表征电路复杂性的"电路宽度",以确定最佳的推理引擎,避免了传统的引擎切换过程,提高了算法的效率.针对ISCAS85电路的实验结果表明了该方法的效率和可行性.     

A three-step decomposition method for the evolutionary design of sequential logic circuits

Evolvable hardware (EHW) refers to an automatic circuit design approach, which employs evolutionary algorithms (EAs) to generate the configurations of the programmable devices. The scalability is one of the main obstacles preventing EHW from being applied to real-world applications. Several techniques have been proposed to overcome the scalability problem. One of them is to decompose the whole circuit into several small evolvable sub-circuits. However, current techniques for scalability are mainly used to evolve combinational logic circuits. In this paper, in order to decompose a sequential logic circuit, the state decomposition, output decomposition and input decomposition are united as a three-step decomposition method (3SD). A novel extrinsic EHW system, namely 3SD–ES, which combines the 3SD method with the (μ, λ) ES (evolution strategy), is proposed, and is used for the evolutionary designing of larger sequential logic circuits. The proposed extrinsic EHW system is tested extensively on sequential logic circuits taken from the Microelectronics Center of North Carolina (MCNC) benchmark library. The results demonstrate that 3SD–ES has much better performance in terms of scalability. It enables the evolutionary designing of larger sequential circuits than have ever been evolved before.     

The mechanical generation of fault trees for reactive systems via retrenchment II: clocked and feedback circuits

The retrenchment approach to the mechanical construction of fault trees, introduced in the first paper for combinational logic circuits, is extended to handle clocked circuits and then feedback circuits. The temporal behaviour of clocked circuits is captured using their causal relations, and the potentially unbounded behaviour of cyclic circuits is decomposed into an iteration over their acyclic counterparts. The repercussions of all this for the theory of retrenchment are elaborated. For clocked circuits, the techniques we present allow glitches and other transient errors to be properly described. For feedback circuits, the plethora of behaviours that can occur, give rise to infinitary fault trees of an appropriate kind. All this paves the way for automated fault tree generation for reactive systems.     

组合压缩在存储测试系统中的应用

在某些特殊的测试环境中,存储测试系统中既要求大容量数据存储又要求微体积.为解决这一矛盾,在研究了游程压缩和LZW两种算法的基础上,提出了以FPGA为核心实现两种算法的无损组合压缩,利用FPGA芯片内的RAM来建立字典,用VHDL语言和状态机实现该压缩算法.仿真和综合验证表明,通过FPGA实现该组合算法,压缩效果显著,压...     

Verification of consensus algorithms using satisfiability solving

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes.