Functional verification is an important aspect of electronic design automation. Traditionally, simulation at the register transfer-level has been the mainstream functional verification approach. Formal verification and various static analysis checkers have been used to complement specific corners of logic simulation. However, as the size of IC designs grow exponentially, all the above approaches fail to scale with the design growth. In recent years, logic emulation have gained popularity in functional verification, partly due to their performance and scalability benefits. There are two main approaches to logic emulation: ASIC and commercial field-programmable gate array (FPGA). In this paper, we focus on commercial FPGA based logic emulation and present various challenging problems in this area for the academic community.

Automatic hardware/software partitioning relies on characterization, estimation and design space exploration of the system performance and cost metrics. In real world situations, such estimates are complicated and cannot be 100 percent accurate. Furthermore, hardware/software co-design is so complicated nowadays that simply considering the bipartitioning between hardware and software is not sufficient. It is important to consider some of the other key design parameters and resource sharing together with the hardware/software partitioning problem. Under variable requirements of smart systems, more flexibility on the resource usage should be incorporated in system modelling. This paper considers uncertainty modeling for system partitioning with an enhanced set of parameters for hardware/software resource sharing. We harness state-of-the-art uncertainty theory for linear uncertain distribution and normal uncertain distribution. Our derivations convert the uncertainty model back to a regular constraint optimization problem. Experimental results show the effectiveness of our approach.

Affine equivalence classification of Boolean functions has significant applications in logic synthesis and cryptography. Previous studies for classification have been limited by the large set of Boolean functions and the complex operations on the affine group. Although there are many research on affine equivalence classification for parts of Boolean functions in recent years, there are very few results for the entire set of Boolean functions. The best existing result has been achieved by Harrison with 15768919 affine equivalence classes for 6-variable Boolean functions. This paper presents a concise formula for affine equivalence classification of the entire set of Boolean functions as well as a formula for affine classification of Boolean functions with distinct ON-set size respectively. The method outlined in this paper greatly simplifies the affine group's action by constructing an isomorphism mapping from the affine group to a permutation group. By this method, we can compute the affine equivalence classes for up to 10 variables. Experiment results indicate that our scheme for calculating the affine equivalence classes for more than 6 variables is a significant advancement over previous published methods.

Effective verification methods are necessary for finding bugs in complex system design. Given domain specific knowledge, design verification engineers typically specify cross coverage for certain risky areas where bugs tend to appear. This paper proposes a pragmatic coverage model based on cross coverage. We address the verification on user specified cross coverage regions. The proposed analysis models the probability of exposing the bug within a given number of samplings, and derives the expected number of samples until bug detection. The approach is applicable to random, round-robin, and hybrid sampling strategies in recurring and nonrecurring cases based on our cross coverage model. We have written Matlab and C programs that use our formulas to calculate the probabilities. Experimental results show that our analysis is consistent with Monte Carlo simulation.

Theorem proving has been demonstrated as a powerful technique for datapath verification. This paper considers a generic logic-level architecture of end-around-carry adder, which is extensively used in floating-point arithmetic. The architecture is component-based and parameterized for easy customization. The design architecture is formalized and verified in the mechanical theorem prover Coq. The scalable proof provides necessary underpinnings for verifying customized and new implementations.

Motion planning is an important problem with many applications in robotics. In this paper, we focus on motion planning with rectangular obstacles parallel to the X, Y or Z axis. We formulate motion planning using Satisfiability Modulo Theories (SMT) and use SMT solvers to find a feasible path from the source to the goal. Our formulation decompose the robotic path into N path segments where the two ends of each path segment can be constrained using difference logic. Our SMT approach will find a solution if and only if a feasible path exists for the given constraints. We present extensive experimental results to demonstrate the scalability of our approach.

This paper combines symmetry reduction with generalized symbolic trajectory evaluation (GSTE) to tackle state explosion. The inherent correlation between structure symmetry and property symmetry is formalized as a theorem, which provides the soundness of our symmetry reduction method. We introduce a practical strategy to effectively integrate the symmetry-reduction approach in a hybrid verification environment which combines theorem proving and GSTE. The effectiveness of our method is demonstrated by case studies.

Network-on-chip (NoC) communication architectures present promising solutions for scalable communication requests in large system-on-chip (SoC) designs. Intellectual property (IP) core assignment and mapping are two key steps in NoC design, significantly affecting the quality of NoC systems. Both are NP-hard problems, so it is necessary to apply intelligent algorithms. In this paper, we propose improved intelligent algorithms for NoC assignment and mapping to overcome the drawbacks of traditional intelligent algorithms. The aim of our proposed algorithms is to minimize power consumption, time, area, and load balance. This work involves multiple conflicting objectives, so we combine multiple objective optimization with intelligent algorithms. In addition, we design a fault-tolerant routing algorithm and take account of reliability using comprehensive performance indices. The proposed algorithms were implemented on embedded system synthesis benchmarks suite (E3S). Experimental results show the improved algorithms achieve good performance in NoC designs, with high reliability.

Programmable Logic Controllers (PLC) are widely used in industry. The reliability of the PLC is vital to many critical applications. This paper presents a novel approach to the symbolic analysis of PLC systems. The approach includes, (1) calculating the uncertainty characterization of the PLC system, (2) abstracting the PLC system as a Hidden Markov Model, (3) solving the Hidden Markov Model with domain knowledge, (4) combining the solved Hidden Markov Model and the uncertainty characterization to form a regular Markov model, and (5) utilizing probabilistic model checking to analyze properties of the Markov model. This framework provides automated analysis of both uncertainty calculations and performance measurements, without the need for expensive simulations. A case study of an industrial, automated PLC system demonstrates the effectiveness of our work.

Embedded systems are becoming increasingly popular due to their widespread applications and the reliability of them is a crucial issue. The complexity of the reliability analysis arises in handling the sequential feedback that make the system output depends not only on the present input but also the internal state. In this paper, we propose a novel probabilistic model, named sequential dependency model (SDM), for the reliability analysis of embedded systems with sequential feedback. It is constructed based on the structure of the system components and the signals among them. We prove that the SDM model is s Dynamic Bayesian Network (DBN) that captures: the spatial dependencies between system components in a single time slice, the temporal dependencies between system components of different time slices, and the temporal dependencies due to the sequential feedback. We initiate the conditional probability distribution (CPD) table of the SDM node with the failure probability of the corresponding system component. Then, the SDM model handles the spatial-temporal correlations at internal components as well as the higher order temporal correlations due to the sequential feedback with the computational mechanism of DBN, experiment results demonstrate the accuracy of our model.

The train control system is a safety-critical embedded system. In this system, all buses and devices share the real time communication protocol, which is described in the standard IEC 61375. Many systems that comply the standard have been implemented and used in the real world railway, however, their safety checking is highly nontrivial. In this paper, we focus on the formal verification and implementation of the protocol described in the standard. The protocol is modeled as a network of timed automata, which are synchronized to describe the procedure of connection establishment and data transmission among vehicles. The stochastic factors such as time delay and packet loss are modeled in the channel module. Afterwards, we abstract some safety critical properties that are important to guarantee the correctness of the protocol. These properties are verified with the model checker Uppaal. Two properties are violated in the verification, and two corresponding bugs in the standard are fixed and proposed to the IEC. In order to prove the bugs we find, we implement two versions of the standard. The first is for the original description of the standard, and the second is for our fixed description. Both versions are tested with the D113 (a widely used general Multifunction Vehicle Bus control system implemented by the Duagon company), and we find that the second version works well, while the first fails. The second version for the fixed protocol is now used in the real world subway.

Programmable logic controller (PLC) system is a typical kind of embedded system that is widely used in industry. The complexity of reliability analysis of safety critical PLC systems arises in handling the temporal correlations among the system components caused by the run-time execution logic of the embedded ladder program. In this paper, we propose a novel probabilistic model for the reliability analysis of PLC systems, called run-time reliability model (RRM). It is constructed based on the structure and run-time execution of the embedded ladder program, automatically. Then, we present some custom-made conditional probability distribution (CPD) tables according to the execution semantics of the RRM nodes, and insert the reliability probability of each system component referenced by the node into the corresponding CPD table. The proposed model is accurate and fast compared to previous work as described in the experiment results.

This paper presents a novel efficient satisfiability (SAT) algorithm based on maxterm covering. The satisfiability of a clause set is determined in terms of the number of relative maxterms of the empty clause with respect to the clause set. If the number of relative maxterms is zero, it is unsatisfiable, otherwise satisfiable. A set of synergic heuristic strategies are presented and elaborated. We conduct a number of experiments on 3-SAT and k-SAT problems at the phase transition region, which have been cited as the hardest group of SAT problems. Our experimental results on public benchmarks attest to the fact that, by incorporating our proposed heuristic strategies, our enhanced algorithm runs several orders of magnitude faster than the extension rule algorithm, and it also runs faster than zChaff and MiniSAT for most of k-SAT (k≥3) instances.

In this work, we present our results on formally verifying hardware design of round-robin arbiter which is the core component in many real network systems. Our approach is enhanced STE, which explores fully symbolic simulation for not only one round of round-robin arbitration, but also the sequential behaviors of the arbiter. Our experiments demonstrate that the enhanced STE specification for real-world hardware design can be finished automatically in a reasonable time and memory usage.

This paper investigates the synthesis of quantum networks built to realize hybrid switching circuits in the absence of ancilla qudits. We prove that all hybrid reversible circuits can be constructed by hybrid Not and Multiple-Controlled-Not gates. We also prove that any hybrid reversible circuit with only 1 or 2 binary qudits and arbitrary number of other qudits, can be constructed by hybrid Not and Controlled-Not gates. We present two construction-based algorithms to synthesize hybrid reversible circuits without ancilla qudits. The algorithms use hybrid Not and Multiple-Controlled-Not gates or hybrid Not and `1'-Controlled-Not gates, which are exponentially lower than breadth-first search based synthesis algorithms with respect to the input number.

This paper considers a cell mapping task of CMOL, a hybrid CMOS/molecular circuit architecture. To tackle the combinatorial hurdle arising from the structural connectivity domain constraint, a memetic computing algorithm is developed. The framework takes advantage of simulated annealing based local search strategy and appropriate population based encoding manipulation. Numerical results from ISCAS benchmarks and comparison with pure genetic approach illustrate the effectiveness of the modeling and solution methodology. In terms of CPU runtime, timing delay and circuit scale, the proposed method has better performance than previous methods.

Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We present an automated approach which combines compositional abstraction and counter-example guided abstraction refinement (CEGAR). The proposed approach exploits the semantics of a timed automaton to procure its over-approximative abstraction. Any safety property which holds on the abstraction is guaranteed to hold on the concrete model. In the case of a spurious counter-example, our proposed approach refines and strengthens the abstraction in a component-wise method. We implemented our method with the model checking tool Uppaal. Experimental results show promising improvements.

Model checking for large-scale systems is extremely difficult due to the state explosion problem. Creating useful abstractions for model checking task is a challenging problem, often involving many iterations of refinement. In this paper we consider techniques for model checking in the counter example-guided abstraction refinement. The state separation problem is one popular approach in counterexample-guided abstraction refinement, and it poses the main hurdle during the refinement process. To achieve effective minimization of the separation set, we present a novel probabilistic learning approach based on the sample learning technique, evolutionary algorithm, and effective heuristics. We integrate it with the abstraction refinement framework in the VIS model checker. We include experimental results on model checking to compare our new approach to recently published techniques. The benchmark results show that our approach has overall speedup of more than 56 percent against previous techniques. Our work is the first successful integration of evolutionary algorithm and abstraction refinement for model checking.

Automated compositional reasoning using assume-guarantee rules plays a key role in large system verification. A vexing problem is to discover fine decomposition of system contributing to appropriate assumptions. We present an automatic decomposition approach in compositional reasoning verification. The method is based on data mining algorithms. An association rule algorithm is harnessed to discover the hidden rules among system variables. A hypergraph partitioning algorithm is proposed to incorporate these rules as weight constraints for system variable clustering. The experiments demonstrate that our strategy leads to order-of-magnitude speedup over previous.

Device failure is an important consideration in nano-scale design. This paper presents a probabilistic logic model to compute the probability distribution of the nano gate states. The characterization is based on markov random field and statistical physics. The basic logic gates are probabilistically characterized. The effectiveness of the method is demonstrated by an inverter and the inverter casecade. Our analysis shows that the device probability distribution highly depends on the system structures and other performance parameters.

Reversible circuits play an important role in quantum computing, which is one of the most promising emerging technologies. In this paper, we investigate the problem of optimally synthesizing 4-bit reversible circuits. We present an enhanced bi-directional synthesis approach. Owing to the exponential nature of the memory and run-time complexity, all existing methods can only perform four steps for the Controlled-Not gate NOT gate, and Peres gate library. Our novel method can achieve 12 steps. As a result, we augment the number of circuits that can optimally be synthesized by over 5 × 106 times. We synthesized 1000 random 4-bit reversible circuits. The statistical analysis result supports our estimation. The quantum cost of our result is also better than the quantum cost of other approaches. The promising experimental results demonstrate the effectiveness of our approach.

This paper presents a constructive synthesis algorithm for any n-qubit reversible function. Given any n-qubit reversible function, there are N distinct input patterns different from their corresponding outputs, where N les 2n, and the other (2n- N) input patterns will be the same as their outputs. We show that this circuit can be synthesized by at most 2nldrN '(n - 1)'-CNOT gates and 4n2ldr N NOT gates. The time complexity of our algorithm has asymptotic upper bound O(n ldr 4n). The space complexity of our synthesis algorithm is also O(n ldr 2n). The computational complexity of our synthesis algorithm is exponentially lower than the complexity of breadth-first search based synthesis algorithm.

This paper proposes an approach to optimally synthesize quantum circuits by symbolic reachability analysis, where the primary inputs and outputs are basis binary and the internal signals can be nonbinary in a multiple-valued domain. The authors present an optimal synthesis method to minimize quantum cost and some speedup methods with nonoptimal quantum cost. The methods here are applicable to small reversible functions. Unlike previous works that use permutative reversible gates, a lower level library that includes nonpermutative quantum gates is used here. The proposed approach obtains the minimum cost quantum circuits for Miller gate, half adder, and full adder, which are better than previous results. This cost is minimum for any circuit using the set of quantum gates in this paper, where the control qubit of 2-qubit gates is always basis binary. In addition, the minimum quantum cost in the same manner for Fredkin, Peres, and Toffoli gates is proven. The method can also find the best conversion from an irreversible function to a reversible circuit as a byproduct of the generality of its formulation, thus synthesizing in principle arbitrary multi-output Boolean functions with quantum gate library. This paper constitutes the first successful experience of applying formal methods and satisfiability to quantum logic synthesis.

We present fast algorithms to synthesize exact minimal reversible circuits for various types of gates and costs. By reducing reversible logic synthesis problems to group theory problems, we use the powerful algebraic software GAP to solve such problems. Our algorithms are not only able to minimize for arbitrary cost functions of gates, but also orders of magnitude faster than the existing approaches to reversible logic synthesis. In addition, we show that the Peres gate is a better choice than the standard Toffoli gate in libraries of universal reversible gates.

We address the problem of implication of assertion graphs that occur in generalized symbolic trajectory evaluation (GSTE). GSTE has demonstrated its powerful capacity in formal verification of digital systems. Assertion graphs are used for property and model specifications. We present a novel implication technique for assertion graphs. It relies on direct Boolean reasoning on each edge (and vertex) of an assertion graph, thus avoiding the reachability computation in GSTE. We have successfully applied. both model-based and language-based implications on real industrial circuits. Experimental results demonstrate the promising performance of our approach.

We propose an approach to optimally synthesize quantum circuits from non-permutative quantum gates such as controlled-square-root-of-not (i.e., controlled-V). Our approach reduces the synthesis problem to multiple-valued optimization and uses group theory. We devise a novel technique that transforms the quantum logic synthesis problem from a multi-valued constrained optimization problem to a group permutation problem. The transformation enables us to utilize group theory to exploit the properties of the synthesis problem. Assuming a cost of one for each two-qubit gate, we find all reversible circuits with quantum costs of 4, 5, 6, etc, and give another algorithm to realize these reversible circuits with quantum gates.

Reversible quantum logic plays an important role in quantum computing. In this paper, we propose an approach to optimally synthesize quantum circuits by symbolic reachability analysis where the primary inputs are purely binary. we use symbolic reachability analysis, a technique most commonly used in model checking (a way of formal verification), to synthesize the optimum quantum circuits. We present an exact synthesis method with optimal quantum cost and a speedup method with non-optimal quantum cost. Both our methods guarantee the synthesizeability of all reversible circuits. Unlike previous works which use permutative reversible gates, we use a lower level library which includes non-permutative quantum gates. For the first time, problems in quantum logic synthesis have been reduced to those of multiple-valued logic synthesis thus reducing the search space and algorithm complexity. We synthesized quantum circuits for gate, half-adder, full-adder, etc. with the smallest cost.. Our approach obtains the minimum cost quantum circuits for Miller's gate, half-adder, and full-adder, which are better than previous results. In addition, we prove the minimum quantum cost (using our elementary quantum gates) for Fredkin, Peres, and Toffoli gates. Our work constitutes the first successful experience of applying satisfiability with formal methods to quantum logic synthesis.

Segmented channel routing is fundamental to the routing of row-based FPGAs. In this paper, we study segmented channel routability via satisfiability. Our method encodes the horizontal and vertical constraints of the routing problem as Boolean conditions. The routability constraint is satisfiable if and only if the net connections in the segmented channel are routable. Empirical results show that the method is time-efficient and applicable to large problem instances.

We present a novel symbolic routability checking approach for three-dimensional interconnect layout. The model considered is a general architecture that can fit into different applications, such as ASIC, multichip modules, field-programmable gate arrays, and reconfigurable computing architectures. The method can incrementally incorporate additional constraints driven by timing, performance, and design. We used the latest satisfiability solver to validate the effectiveness of our approach. The experimental results demonstrate the encouraging performance on difficult routing benchmarks.

This paper presents a satisfiability-based method for solving the board-level multiterminal net routing problem in the digital design of clos-folded field-programmable gate array (FPGA) based logic emulation systems. The approach transforms the FPGA board-level routing task into a Boolean equation. Any assignment of input variables that satisfies the equation specifies a valid routing. We use two of the fastest Boolean satisfiability (SAT) solvers: Chaff and DLMSAT to perform our experiments. Empirical results show that the method is time-efficient and applicable to large layout problem instances.

The paper presents a satisfiability-based method for solving the board-level multiterminal net routing problem in Clos-Folded FPGA based logic emulation systems. The approach transforms the FPGA board-level routing task into a single, large Boolean equation with the property that any assignment of input variables that satisfies the equation specifies a valid routing. The approach considers all nets simultaneously and the absence of a satisfying assignment implies that the layout is unroutable. We use two of the fastest SAT solvers: Chaff and DLM to perform our experiments. Empirical results show that the method is time-efficient and applicable to large layout problem instances.

Reduced-ordered binary decision diagrams (BDDs) are a data structure for representation and manipulation of Boolean functions. The variable ordering largely influences the size of the BDD, varying from linear to exponential. In this paper, the authors study the BDD minimization problem based on scatter search optimization. Scatter search offers a reasonable compromise between quality (BDD reduction) and time. On smaller benchmarks it delivers almost optimal BDD size with less time than the exact algorithm. For larger benchmarks it delivers smaller BDD sizes than genetic algorithm or simulated annealing at the expense of longer runtime.

Reduced ordered binary decision diagrams (BDDs) are a data structure for representation and manipulation of Boolean functions which are frequently used in VLSI design automation. The variable ordering largely influences the size of the BDD, varying from linear to exponential. In this paper we study BDD minimization problem based on scatter search optimization. The results we obtained are very encouraging in comparison with other heuristics (genetic and simulated annealing). This work is the first successful experience of using scatter search approach in design automation area. The approach can be applied to many design automation applications.