Approximate computing is an emerging design paradigm for error-tolerant applications, such as multimedia processing and neural network acceleration, which enables significant reductions in circuit area, delay, or power consumption through controlled accuracy trade-offs. This paper presents a novel deep reinforcement learning (DRL)-based framework for approximate logic synthesis (ALS) augmented with a backtracking mechanism, aimed at minimizing the area–delay product (ADP) while satisfying error rate constraints. The experimental results demonstrate that our approach can reduce the ADP by up to 92.83%, and 56.79% on average under a 5% error rate constraint.

Simulation-based approaches to detecting the nonequivalence of quantum circuits are efficient since they usually conclude the result of non-equivalence faster than traditional methods. However, proving the equivalence of two quantum circuits remains challenging. As a result, this paper aims at analyzing simulation-based approaches and uncovering their potential and limitations in equivalence checking.

This paper presents a novel approach to approximate logic synthesis (ALS) targeting at Dot-Inverter Graph (DIG), which is known for its superior expressive ability among all the 3-input gates and its potential in the future technology. We focus on minimizing the size of DIG circuits while maintaining acceptable error rates by introducing a Node Merging (NM)-enhanced Genetic Algorithm (GA)-based approach. The NM technique reduces the DIG size without altering its functionality, while the GA, incorporating Average Relative Hamming Distance (ARHD) and a self-adjusted mutation level, is used for ALS on DIGs. Our experimental results demonstrated that the proposed approach achieves a higher reduction rate and less CPU time on different sizes of circuits compared to the state-of-the-art ALS approach.

During the IR Engineering Change Order (ECO) stage, cell moving leads to uncertain IR-drop results, requiring designers to explore multiple ECO candidates in each iteration to find a solution that effectively mitigates IR-drop, resulting in a long evaluation time. Although machine learning (ML)-based predictors have been proposed to expedite IR-drop evaluation, partial simulations are still needed to update features after ECO, taking over an hour and delaying IR-drop results. In this work, we propose a real-time dynamic IR-drop estimation method based on an XGBoost model with a global view of a cell’s surroundings. After ECO, our method provides dynamic IR-drop results in minutes without running any simulations and thus achieves real-time estimation. This allows designers to evaluate multiple ECO candidates concurrently in a single iteration. We conducted the experiments on five ECO candidates of an industrial design with 3 nm technology. The results show that the proposed model can effectively predict the IR-drop variations of moved cells after ECO with over $93 \%$ of fixed cells detected and an average MAE of 8.75 mV achieved. Furthermore, our method achieves an $88 X$ speedup over Voltus (commercial tool) and a $64 X$ speedup over traditional ML predictors when evaluating a single ECO candidate. The speedup is expected to increase as the number of ECO candidates increases.

Dynamic IR drop analysis is a critical step in the design signoff stage for verifying the power integrity of a chip. Since the analysis is extremely time-consuming, it has led to the emergence of machine learning (ML)-based methods to expedite the procedure. While previous ML approaches have demonstrated the feasibility of IR drop prediction, they often neglect package effects and do not address diverse IR criteria for memory and standard cells. Thus, this paper introduces a novel ML-based approach designed for a fast and accurate prediction of multi-type IR drop, considering package effects. We develop new package-related features to account for the package impact on IR drop. The proposed model is based on a multitask U-net architecture that not only predicts two types of IR drops simultaneously but also increases prediction accuracy through comprehensive learning. To further enhance the model performance, we introduce the Input Fusion Block (IFB), which unifies units across channels within the input feature maps, leading to improved prediction accuracy. The experimental results show the across-pattern transferability of the proposed IR drop prediction method, demonstrating an RMSE of less than SmV and an MAE of less than 2mV on the unseen simulation patterns. Additionally, our proposed method achieves a 5X speedup compared to the commercial tool.

Cyclic logic locking is a cutting-edge hardware security method developed to defend against SAT Attack. It introduces cycles into the original circuit, which can cause the circuit to either get trapped in an endless loop or generate incorrect outputs if an incorrect key is used. Recently, a new cyclic logic locking method called LOOPLock 2.0 was proposed. Its primary feature is that the circuit retains its cyclic structure regardless of whether the correct key vector is applied or not. However, LOOPLock 2.0 can still be successfully attacked using locking structure analysis in the state-of-the-art. As a result, this paper presents a more robust cyclic logic locking approach LOOPLock 3.0 to counteract state-of-the-art attacks. The experimental results validate the effectiveness of the proposed approach.

Reverse engineering is a process that converts low-level description to high-level one. In this paper, we propose a hybrid approach consisting of structural analysis and black-box testing to reverse engineering on combinational circuits. Our approach is able to convert combinational circuits from gate-level netlist to Register-Transfer Level (RT-level) design accurately and efficiently. We developed our approach and participated in Problem A of the 2022 CAD Contest @ ICCAD. The revised version of our program successfully converted most cases and achieved higher scores than the 1stplace team in the contest.

With the advances in semiconductor technology, the sizes of transistors are getting smaller, which has led to an increasingly severe impact of IR drop. Consequently, this trend has amplified the significance of IR drop analysis within the realm of chip design. However, analyzing IR drop is resource-intensive and time-consuming, since numerous simulation patterns are required to verify the power integrity of circuits. Additionally, with every engineering change order (ECO) step, a reevaluation is necessary. In this paper, we propose a machine learning-based method to predict IR drop levels and present an algorithm for reducing simulation patterns, which could reduce the time and computing resources required for IR drop analysis within the ECO flow. Experimental results show that our approach can reduce the number of patterns by approximately 50%, thereby decreasing the analysis time while maintaining accuracy.

Identification of a Threshold Function (TF) is a significant task that determines whether a given Boolean function is a TF or not. The state-of-the-art only identifies all 8-input NP-class TFs. In this paper, we propose a new necessary condition for a function being a representative NP-class TF. With the proposed necessary condition, we design an effective approach to identify 9-input NP-class TFs. As a result, we reduce the candidate set of 9-input functions being TFs to an extremely tiny subset of all 9-input Boolean functions. Experimental results show that our approach successfully identifies at least 80% of 9-input NP-class TFs. This is the first attempt to deal with this challenging problem in the literature.

Approximate computing is an emerging design technique for error-tolerant applications, which may improve circuit area, delay, or power consumption by trading off a circuit's correctness. In this paper, we propose a novel approximate logic synthesis approach based on genetic algorithm targeting at depth minimization with an error rate guarantee. We conduct experiments on a set of IWLS 2005 and MCNC benchmarks. The experimental results demonstrate that the depth can be reduced by up to 50%, and 22% on average under a 5% error rate constraint. As compared with the state-of-the-art method, our approach can achieve an average of 159% more depth reduction under the same 5% error rate constraint.

As several compilation and optimization techniques have been proposed, equivalence checking for quantum circuits has become essential in design flows. The state-of-the-art to this problem observed that even small errors substantially affect the entire quantum system. As a result, it exploited random simulations to prove the non-equivalence of two quantum circuits. However, when errors occurred close to outputs, it was hard for the work to prove the non-equivalence of some non-equivalent quantum circuits under a limited number of simulations. In this work, we propose a novel simulation-based approach using a set of specially designed stimuli. The simulation runs of the proposed approach is linear rather than exponential to the number of quantum bits of a circuit. According to the experimental results, the success rate of our approach is 100% (100%) under a simulation run (execution time) constraint for a set of benchmarks, while that of the state-of-the-art is only 69% (74%) on average. Our approach also achieves a speedup of 26 on average.

The “CAD Contest at ICCAD” is a challenging, multi-month, research and development competition, focusing on advanced, real-world problems in the field of electronic design automation (EDA). Since 2012, the contest has been publishing many sophisticated circuit design problems, from system-level design to physical design, together with industrial benchmarks and solution evaluators. Contestants can participate in one or more problems provided by EDA/IC industry. The winners will be awarded at an ICCAD special session dedicated to this contest. Every year, the contest attracts more than a hundred teams, fosters productive industry-academia collaborations, and leads to hundreds of publications in top-tier conferences and journals. The 2023 CAD Contest has 210 teams from all over the world, which generates the highest participation record. Moreover, the problems of this year cover state-of-the-art EDA research trends such as circuit verification, hardware security, 3D-IC, and Machine Learning (ML) for EDA from well-known EDA/IC companies. We believe the contest keeps enhancing impact and boosting EDA researches.

Threshold Function (TF) is a subset of Boolean function that can be represented with a single linear threshold gate (LTG). In the research about threshold logic, the identification of TF is an important task that determines whether a given function is a TF or not. In this article, we propose a sufficient and necessary condition for a function being a TF. With the proposed sufficient and necessary condition, we devise a TF identification algorithm. The experimental results show that the proposed approach saves 80% CPU time for identifying all the 8-input NP-class TFs as compared with the state-of-the-art. Furthermore, the LTGs corresponding to the identified TFs obtained by the proposed approach have smaller weights and threshold values than the state-of-the-art.

The "CAD Contest at ICCAD" is a challenging, multi-month, research and development competition, focusing on advanced, real-world problems in the field of electronic design automation (EDA). Since 2012, the contest has been publishing many sophisticated circuit design problems, from system-level design to physical design, together with industrial benchmarks and solution evaluators. Contestants can participate in one or more problems provided by EDA/IC industry. The winners will be awarded at an ICCAD special session dedicated to this contest. Every year, the contest attracts more than a hundred teams, fosters productive industry-academia collaborations, and leads to hundreds of publications in top-tier conferences and journals. The 2022 CAD Contest has 166 teams from all over the world. Moreover, the problems of this year cover state-of-the-art EDA research trends such as circuit security, 3D-IC, and design space exploration from well-known EDA/IC companies. We believe the contest keeps enhancing impact and boosting EDA researches.

Cyclic logic locking is a new type of SAT-resistant techniques in hardware security. Recently, LOOPLock 2.0 was proposed, which is a cyclic logic locking method creating cycles deliberately in the locked circuit to resist SAT Attack, CycSAT, BeSAT, and Removal Attack simultaneously. The key idea of LOOPLock 2.0 is that the resultant circuit is still cyclic no matter the key vector is correct or not. This property refuses attackers and demonstrates its success on defending against attackers. In this paper, we propose an unlocking approach to LOOPLock 2.0 based on structure analysis and SAT solvers. Specifically, we identify and remove non-combinational cycles in the locked circuit before running SAT solvers. The experimental results show that the proposed unlocking approach is promising.

Quantum-dot cellular automata (QCA) is considered as a promising emerging technology due to its low power dissipation and high device density. Since the majority function is the main operation in QCA circuits, minimizing the number of majority gates in QCA circuits is crucial to the corresponding QCA circuit minimization. A previous work used the node-merging technique to replace one target node with an existing substitute node in majority circuits for optimization. However, this technique may fail when no substitute nodes exist for a target node. In this article, we propose an enhanced optimization technique for majority circuits by adding a new node into the circuits and removing the target node and its fanin nodes. The experimental results show that this technique improves the results of the node-merging technique on a set of EPFL logic synthesis benchmarks. Additionally, this enhanced technique can work together with other optimization techniques. The circuit size reduction in the integrated approach reaches 1.26 times as compared to the results using the node-merging technique.

Threshold logic has been attracting great attention from researchers due to the rapid development in nanotechnology-based devices. In the state-of-the-art approach to the threshold logic network (TLN) synthesis using don’t cares, we observed that not all the computed don’t cares contribute to the cost minimization of threshold logic gate (TLG). Therefore, in this work, we focus on computing the don’t cares that effectively provide the opportunities for cost minimization. Furthermore, De Morgan’s law for TLGs is applied such that global TLN optimization considering the cost and the number of inverters can be achieved. The experimental results show that the proposed approach is capable of obtaining efficiently a smaller cost and fewer inverters for a set of TLN benchmarks.

Reducing the number of AND gates in logic networks benefits the applications in cryptography, security, and quantum computing. This work proposes a don’t-care-based (DC-based) approach to reduce the number of AND gates further in the well-optimized network. Furthermore, this work also proposes an enhanced synthesis flow by integrating our approach with the state-of-the-art. The experimental results show that our approach can further reduce up to 25% of the number of AND gates in the network. For the experiments about the enhanced synthesis flow, we achieve a speedup of almost$10\times $on average for the cryptography benchmarks while having competitive results as compared to the flow in the state-of-the-art.

LOOPLock is the state-of-the-art cyclic logic locking method in hardware security. LOOPLock is able to invalidate SAT Attack, Removal Attack, and CycSAT simultaneously by introducing two types of cycle pairs in a circuit. In this work, we analyze LOOPLock’s locking mechanism and propose an attacking approach based on locking structure analysis. Furthermore, to defend the new attack, we propose LOOPLock 2.0, which strengthens the original cyclic logic locking method—LOOPLock. Experimental results show the efficiency and effectiveness of the proposed attacking approach to LOOPLock and the high defense capability of LOOPLock 2.0.

Logic equivalence checking is a critical task in the ASIC design flow. Due to the rapid development in nanotechnology-based devices, an efficient implementation of multivalued logic becomes practical. As a result, many synthesis algorithms for ternary logic were proposed. In this paper, we bring out an equivalence checking framework based on multivalued logic exploiting the modern SAT solvers. Furthermore, a structural conflict-driven clause learning (SCDCL) technique is also proposed to accelerate the SAT solving process. The SCDCL algorithm deploys some strategies to cut off the search space for SAT algorithms. The experimental results show that the proposed SCDCL technique saves 42% CPU time from SAT solvers on average over a set of industrial benchmarks.

Approximate computing is an emerging design paradigm for error-tolerant applications. e.g., signal processing and machine learning. In approximate computing, the area, delay, or power consumption of an approximate circuit can be improved by trading off its accuracy. In this paper, we propose an approximate logic synthesis approach based on a node-merging technique with an error rate guarantee. The ideas of our approach are to replace internal nodes by constant values and to merge two similar nodes in the circuit in terms of functionality. We conduct experiments on a set of IWLS 2005 and MCNC benchmarks. The experimental results show that our approach can reduce area by up to 80%, and 31% on average. As compared with the state-of-the-art method, our approach has a speedup of 51 under the same 5% error rate constraint.

The “CAD Contest at ICCAD” is a challenging, multi-month, research and development competition, focusing on advanced, real-world problems in the field of electronic design automation (EDA). Since 2012, the contest has been publishing many sophisticated circuit design problems, from system-level design to physical design, together with industrial benchmarks and solution evaluators. Contestants can participate in one or more problems provided by EDA/IC industry. The winners will be awarded at an ICCAD special session dedicated to this contest. Every year, the contest attracts more than a hundred teams, fosters productive industry-academia collaborations, and leads to hundreds of publications in top-tier conferences and journals. The 2021 CAD Contest has 137 teams from all over the world. The contest keeps enhancing impact and boosting EDA research.

Singe-Electron Transistor (SET) is considered as a promising candidate of low-power devices for replacement or co-existence with Complementary Metal-Oxide-Semiconductor (CMOS) transistors/circuits. In this work, we propose a diagnosis approach for SET array under a more generalized defect model. With the more generalized defect model, the diagnosis approach will become more practical but complicated. We conducted experiments on a set of SET arrays with different dimensions and defect rates. The experimental results show that our approach only has 3.8% false-negative rate and 0.7% misjudged-category rate on average without reporting any false-positive edge when the defect rate is 4%. Therefore, the proposed diagnosis approach can diagnose the defective SET arrays and elevate the reliability of the SET arrays in the synthesis flow.

The binary-weight-binary-input binarized neural network (BNN) allows a much more efficient way to implement convolutional neural networks (CNNs) on mobile platforms. During inference, the multiply-accumulate operations in BNNs can be reduced to XNOR-popcount operations. Thus, the XNOR-popcount operations dominate most of the computation in BNNs. To reduce the number of required operations in convolution layers of BNNs, we decompose 3-D filters into 2-D filters and exploit the repeated filters, inverse filters, and similar filters to share results. By sharing the results, the number of operations in convolution layers of BNNs can be reduced effectively. Experimental results show that the number of operations can be reduced by about 60% for CIFAR-10 on BNNs while keeping the accuracy loss within 1% of originally trained network.

SAT Attack, CycSAT, and Removal Attack have demonstrated their abilities to break most existing logic locking methods. In this article, we propose a new cyclic logic locking method to invalidate these attacks simultaneously. Our main intention is to create noncombinational cycles to lock a circuit. Specifically, the noncombinational behavior in the noncombinational cycles that is unobservable at the primary outputs (POs) needs to be preserved when the correct key-vector is fed to resist CycSAT, and the noncombinational behavior in the noncombinational cycles affecting POs needs to be preserved when the incorrect key-vector is fed to invalidate SAT Attack. Furthermore, some nodes will be removed when applying our locking method, which is able to defend Removal Attack. The experimental results show the effectiveness and low area overhead of the proposed method.

This article proposes a new necessary condition and the corresponding speedup strategies to the threshold function (TF) identification problem. The state-of-the-art to this identification problem could be very time-consuming when the function-under-identification is a non-TF with the unateness property. The proposed new necessary condition can be seamlessly integrated into this identification algorithm. As compared with the state-of-the-art, the improved identification algorithm with the proposed necessary condition can more effectively and efficiently detect non-TFs. Furthermore, according to the experimental results, the ratio of CPU time overhead in the process of checking the proposed necessary condition for identifying all the 8-input TF is only 0.1%.

The identification of threshold function (TF), which determines whether a Boolean function can be represented by an linear threshold logic gate (LTG) or not, is a fundamental but important task in the theories of threshold logic. In this paper, we propose a more efficient and effective algorithm of TF identification by constructing the system of irredundant inequalities and adjusting the weight assignment comprehensively. This is the first non-ILP-based approach that is able to identify all the eight-input TFs. The experimental results demonstrated that the proposed approach is more effective than all the existing non-ILP-based approaches and the LTGs obtained by the proposed approach are optimal for near 100% cases. For TFs with 9–15 inputs, the proposed approach can identify 100 000 randomly generated TFs as well in a reasonable CPU time.

Recently, Threshold logic attracts a lot of attention due to the advances of its physical implementation and the strong binding to neural networks. Approximate computing is a new design paradigm that focuses on error-tolerant applications, e.g., machine learning or pattern recognition. In this paper, we integrate threshold logic with approximate computing and propose a synthesis algorithm to obtain cost-efficient approximate threshold logic circuits with an error rate guarantee. We conduct experiments on IWLS 2005 benchmarks. The experimental results show that the proposed algorithm can efficiently explore the approximability of each benchmark. For a 5% error rate constraint, the circuit cost can be reduced by up to 65%, and 22.8% on average. Compared with a naive method, our approach has a speedup of 2.42 under a 5% error rate constraint.

Boolean Relation (BR) is a many-to-many mapping between two domains. Logic optimization considering BR can exploit the potential flexibility existed in logic networks to minimize the circuits. In this paper, we present a logic optimization approach considering BR. The approach identifies a proper sub-circuit and locally changes its functionality by solving the corresponding BR in the sub-circuit without altering the overall functionality of the circuit. We conducted experiments on a set of MCNC benchmarks that cannot be further optimized by resyn2 script in ABC. The experimental results show that the node counts of these benchmarks can be further reduced. Additionally, when we apply our approach followed by the resyn2 script repeatedly, we can obtain 6.11% improvements in average.

Fault-based verification technique is a method to qualify a verification environment. The better verification environment can detect output differences between the fault-free and fault-injected circuits with a higher probability. Since different injected faults could cause the same output response under all stimuli, which are called equivalent faults, maximally identifying these equivalent faults can improve the efficiency of verification environment qualification without sacrificing its quality. The 2016 CAD Contest at ICCAD posed the problem of identifying equivalent faults in the circuits. This paper presents our work in the Contest with some improvements.

Memristor, which is a two-terminal nanodevice, widely used in various fields, e.g., machine learning and neuromorphic systems, has attracted much attention these years. Memristor can also be used to realize an implication logic gate and thus logic circuits. However, the fanouts in a memristor-based logic circuit have some constraints and need to be processed with special care. On the other hand, in addition to the number of memristors, the number of operational pulses is another metric to measure the quality of a memristor-based logic circuit. Hence, in this paper, we propose a synthesis algorithm to deal with the fanout problems in memristor-based logic circuits using implication logic gates for having a minimal number of operational pulses. We conducted experiments on a set of MCNC benchmarks. The experimental results show that the proposed algorithm can reduce 29% operational pulses and 36% memristor count on average compared with the state-of-the-art.

Quantum-dot Cellular Automata (QCA) has emerged as a new design paradigm for nanotechnologies. Since the operational logic in QCA is the majority logic, much research about the synthesis and optimisation of majority logic has been proposed recently. In this paper, we propose an optimisation method by merging nodes in the Majority-Inverter-Graph, which is the representation of majority logic circuits. Instead of using satisfiability solvers, our approach can identify the node mergers by using logic implications for circuit size reduction. The experimental results show that for a set of EPFL benchmarks, our approach can minimise the node count by 21% when integrated with the state-of-the-art on average.

Single-electron transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore's law due to its ultralow-power consumption. Previous works proposed mapping approaches to implement Boolean functions on SET arrays. However, these approaches were based on an ideal assumption that the SET arrays are defect-free. Recently, a diagnosis method was proposed targeting at defective SET arrays. However, the approach was static, such that the performance is inefficient. As a result, in this paper, we propose a dynamic diagnosis approach that can efficiently identify the locations and the types of the defects in the SET arrays. The experimental results show that the proposed dynamic diagnosis approach can achieve the same results as the previous work with much less CPU time on a set of benchmarks. Furthermore, the proposed method spent a few seconds while the previous work exceeded the CPU time limit of 3600 s on some benchmarks.

A majority function can be represented as sum-of-product (SOP) form or product-of-sum (POS) form. However, a Boolean expression including majority functions could be more compact compared to SOP or POS forms. Hence, majority logic provides a new viewpoint for manipulating the Boolean logic. Recently, majority logic attracts more attentions than before and some synthesis algorithms and axiomatic system for majority logic have been proposed. On the other hand, solvers for satisfiability (SAT) problem have a tremendous progress in the past decades. The format of instances for the SAT solvers is the Conjunctive Normal Form (CNF). For the instances that are not expressed as CNF, we have to transform them into CNF before running the SAT-solving process. However, for the instances including majority functions, this transformation might be not scalable and time-consuming due to the exponential growth in the number of clauses in the resultant CNF. As a result, this paper presents a new SAT solver-MajorSat, which is for solving a SAT instance containing majority functions without any transformation. Some techniques for speeding up the solver are also proposed. Besides, we also propose a transformation method that can generate the characteristic function of a majority logic gate. The experimental results show that the MajorSat solver can efficiently solve random instances containing majority functions that CNF SAT solvers, like MiniSat or Lingeling, cannot.

Single-electron transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore’s law due to its ultra-low power consumption. Existing SET synthesis methods synthesize a Boolean network into a large reconfigurable SET array where the height of SET array equals the number of primary inputs. However, recent experiments on device level have shown that this height is restricted to a small number, say, 10, rather than arbitrary value due to the ultra-low driving strength of SET devices. On the other hand, the width of an SET array is also suggested to be a small value. Consequently, it is necessary to decompose a large SET array into a set of small SET arrays where each of them realizes a sub-function of the original circuit with no more than 10 inputs. Thus, this article presents two techniques for achieving area-efficient SET array decomposition: One is a width minimization algorithm for reducing the area of a single SET array; the other is a depth-bounded mapping algorithm, which decomposes a Boolean network into many sub-functions such that the widths of the corresponding SET arrays are balanced. The width minimization algorithm leads to a 25%--41% improvement compared to the state of the art, and the mapping algorithm achieves a 60% reduction in total area compared to a naïve approach.

Single-electron transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore's law due to its ultralow power consumption. However, early realizations of SET array lacked variability and reliability due to their fixed architectures and high defect rates of nanowire segments. Therefore, a reconfigurable version of SET was proposed to deal with these issues. Recently, several automated mapping approaches have been proposed for area minimization of reconfigurable SET arrays. However, to the best of our knowledge, seldom mapping algorithms that consider the existence of defective nanowire segments were proposed. Furthermore, before the defect-aware mapping, we have to know the locations of defects in SET arrays. Thus, this paper presents the first diagnosis approach to identify the locations of defects in SET arrays followed by two defect-aware algorithms for mapping SET arrays in different scenarios. The experimental results show that the proposed diagnosis method can detect 100% of defects under a defect rate and distribution in SET arrays. As for the mapping algorithms, the results show that our approach can successfully map the SET arrays with 11.13% and 7.69% width overhead on average in the baseline detour mapping algorithm and defect-reuse mapping algorithm, respectively, in the presence of 5000-ppm defects.

Single-Electron Transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore's law due to its ultra low power consumption. However, early realizations of SET array lacked variability and reliability due to their fixed architectures and high defect rates of nanowire segments. Therefore, a reconfigurable version of SET was proposed to deal with these issues. Recently, several automated mapping approaches were proposed for area minimization of reconfigurable SET arrays. However, to the best of our knowledge, no mapping approaches that consider the existence of defective nanowire segments were proposed. Thus, this paper presents the first defect-aware approach for mapping reconfigurable SET arrays. The experimental results show that our approach can successfully map the SET arrays with 20% width overhead on average in the presence of 5000 ppm defects.

Negative Bias Temperature Instability (NBTI) has become a major reliability concern in nanoscale designs. Although several previous studies have been proposed to address the NBTI effect during logic synthesis, their performance is limited because of focusing on a certain logic synthesis stage. Additionally, their complicated algorithms are not scalable to large designs. To tackle this, we propose a coordinated and scalable logic synthesis approach, which integrates techniques at different logic synthesis stages, ranging from subject graph to technology mapping and mapped netlist, to achieve an effective NBTI reduction. To our best knowledge, this is the first work that considers and mitigates NBTI impact in subject graphs, the earlier stage of logic synthesis. Experimental results on industry-strength benchmarks show that our approach can achieve 6.5% NBTI delay reduction with merely 2.5% area overhead on average, while a previous work barely gets NBTI delay reduction when the circuits are optimized beforehand, the circuit sizes are large, and standard cell libraries are richer.

Traditionally, we expect that circuit designs can be executed without errors. However, for error resilient applications such as image processing, 100% correctness is not necessary. By pursuing less than 100% correctness, power consumption can be significantly reduced. Recently, probabilistic CMOS and probabilistic Boolean circuits (PBCs) have been proposed to deal with power consumption issue. However, to the best of our knowledge, no correctness analysis and power optimization algorithms have been proposed for PBCs. Thus, in this paper, we first propose a statistical approach for evaluating the correctness of PBCs. Then, we propose strategies for power optimization of PBCs. Finally, we integrate these strategies with the correctness analysis as a power optimization algorithm for PBCs. The experimental results show that the proposed correctness analysis method is highly efficient and accurate, and that the power optimization algorithm saves 36% of total power-delay-product on average under a correctness constraint of 90% on a set of International Workshop on Logic and Synthesis (IWLS) 2005 benchmarks.

Power consumption has become one of the primary challenges to meetMoore's law. For reducing power consumption, single-electron transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore's law due to its ultralow power consumption in operation. Previous works have proposed automated mapping approaches for SET arrays that focused on minimizing the number of hexagons in the SET arrays. However, the area of an SET array is the product of the bounded height and the bounded width, and the height usually equals the number of inputs in the Boolean function. Consequently, in this paper, we focus on the width minimization to reduce the overall area in the mapping of the SET arrays. Our approach consists of techniques of product term minimization, branch-then-share (BTS)-aware variable reordering, SET array architecture relaxation, and BTS-aware product term reordering. The experimental results on a set of MCNC and IWLS 2005 benchmarks show that the proposed approach saves 45% of width compared with the work by Chiang et al., which focused on hexagon count minimization, and also saves 13% of width compared with the work by Chen et al., which focused on width minimization.

Recently, many works have been focused on synthesis, verification, and testing of threshold circuits due to the rapid development in efficient implementation of threshold logic circuits. To minimize the hardware cost of threshold circuit implementation, this paper proposes a heuristic that consists of rewiring operations and a simplification procedure. Additionally, a subset of input vectors of a gate, called critical-effect vectors, are proved to be complete for formally verifying the equivalence of two threshold logic gates, instead of the whole truth table in this paper. This achievement can accelerate the equivalence checking of two threshold logic gates. The experimental results show that the proposed heuristic can efficiently reduce the cost.

Power consumption has become one of the primary challenges to meet the Moore's law. For reducing power consumption, Single-Electron Transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore's law due to its ultra-low power consumption during operation. Prior work has proposed an automated mapping approach for SET arrays which focuses on minimizing the number of hexagons in an SET array. However, the area of an SET array is more related to the width. Consequently, in this work, we propose an approach for width minimization of the SET arrays. The experimental results show that the proposed approach saves 26% of width compared with the state-of-the-art for a set of MCNC and IWLS 2005 benchmarks while spending similar CPU time.

Single-electron transistor (SET) is an ultra-low power device, which has been demonstrated as a promising alternative for CMOS devices in reducing power consumption. A suitable structure for realizing logic function using SET is a binary decision diagram (BDD)-based SET array. Previous works proposed product term-based automated synthesis methods to map a given logic function onto an SET array. In this work, we propose a novel BDD-based synthesis method that exploits the structure similarity between an SET array and a BDD. Our method transforms a BDD of a Boolean function into a planar graph and further maps the graph onto an SET array. Experiment results showed that compared to the state-of-the-art synthesis method, our method saves 51% in area on average and is more than 16 times faster.

Alzheimer's disease (AD) is becoming one of the major diseases of the elderly. Traditionally, patients take questionnaires or do some balance tests for clinical evaluation. However, results with such evaluation are subjective. For more objective quantitative measurement, this paper uses an inertial-sensor-based device to measure the gait information while participants walking. In the experiment, the participants are asked to walk on a 40m strike line and take single-task and dual-task tests. In the dual-task test, the participants are asked to count down from 100. This paper presents a stride detection algorithm to automatically acquire gait information of each gait cycle from the acceleration and angular velocity signals. Features are calculated from those inertial signals. After feature generation, we do feature selection to select the significant feature. Then, a probabilistic neural networks (PNNs) is used to classify if the participants suffer from AD. In this paper, we provide an objective way to evaluate the situation of the participants. The experimental results successfully validate the effectiveness of the proposed device and the proposed algorithm with an overall classification accuracy rates are 63.33% and 70.00% in women and men group, respectively.

Despite patients with Alzheimer's disease (AD) were reported of revealing gait disorders and balance problems, there is still lack of objective quantitative measurement of gait patterns and balance capability of AD patients. Based on an inertial-sensor-based wearable device, this paper develops gait and balance analyzing algorithms to obtain quantitative measurements and explores the essential indicators from the measurements for AD diagnosis. The gait analyzing algorithm is composed of stride detection followed by gait cycle decomposition so that gait parameters are developed from the decomposed gait details. On the other hand, the balance is measured by the sway speed in anterior-posterior (AP) and medial-lateral (ML) directions of the projection path of body's center of mass (COM). These devised gait and balance parameters were explored on twenty-one AD patients and fifty healthy controls (HCs). Special evaluation procedure including single-task and dual-task walking experiments for observing the cognitive function and attention is also devised for the comparison of AD and HC groups. Experimental results show that the wearable instrument with the designed gait and balance analyzing system is a promising tool for automatically analyzing gait information and balance ability, serving as assistant indicators for early diagnosis of AD.

Power consumption has become one of the primary challenges in meeting Moore's law. Fortunately, Single-Electron Transistor (SET) at room temperature has been demonstrated as a promising device for extending Moore's law due to its ultra low power consumption during operation. An automated mapping approach for the SET architecture has been proposed recently for facilitating design realization. In this paper, we propose an enhanced approach consisting of variable reordering, product term reordering, and mapping constraint relaxation techniques to minimizing the area of mapped SET arrays. The experimental results show that our enhanced approach, on average, saves 40% in area and 17% in mapping time compared to the state-of-the-art approach for a set of MCNC and IWLS 2005 benchmarks.

Threshold logic has been known as an alternative representation of Boolean logic due to its compactness characteristic. Recently, the developments in advanced nanotechnologies have also promised efficient implementations of threshold logic gates. Thus, many synthesis methodologies for threshold logic circuits have been proposed. Since threshold logic has a different mechanism in functional evaluation compared to the traditional Boolean logic, a threshold logic gate can represent a more complex function. As a result, the sensitization criterion in threshold logic circuits is also different. In this work, we propose a sensitization criterion for threshold logic circuits, and show its application to the static timing analysis problem. The experimental results show the accuracy of the proposed criterion.

Mutation Analysis (MA) is a fault-based simulation technique that is used to measure the quality of testbenches for mutant detections where mutants are simple syntactical changes in the designs. A mutant is said living if its error effect cannot be observed at the primary outputs. Previous works mainly focused on the cost reduction in the process of MA, because the MA is a computation intensive process in the commercial tool. For the living mutants, to the best of our knowledge, the commercial tool has not addressed the pattern generation issue yet. Thus, this paper presents a Genetic Algorithm to generate patterns for detecting living mutants such that the quality of the verification environment is improved. The experimental results show that more living mutants can be detected after adding the generated patterns in the testbench.

Reducing power consumption has become one of the primary challenges in chip design, and therefore significant efforts are being devoted to find holistic solutions on power reduction from the device level up to the system level. Among a plethora of low power devices that are being explored, single-electron transistors (SETs) at room temperature are particularly attractive. Although prior work has proposed a binary decision diagram-based reconfigurable logic architecture using SETs, it lacks an automatic synthesis algorithm for the architecture. Consequently, in this work, we develop a product-term-based approach that synthesizes a logic circuit by mapping all its product terms into the SET architecture. The experimental results show the effectiveness and efficiency of the proposed approach on a set of MCNC benchmarks.

Recently, single-electron transistors (SETs) have been attracting substantial attention and are considered candidate devices for future integrated circuits due to their ultralow power consumption. To realize SETs, a binary decision diagram-based SET array is proposed as a suitable candidate for implementing Boolean circuits. Then, some works started developing computer-aided design techniques for this new architecture. However, most of them focused on the development of mapping techniques. How to verify the mapping results is still an open problem. Thus, in this paper, we address this problem and develop a satisfiability (SAT)-based verification method. We propose a transformation approach to model the functionality of a mapped SET array as a conjunctive normal form formula. Then, the problem that whether the SET array is functionally equivalent to its specification circuit can be solved with a SAT solver. The experimental results show that the proposed method can successfully verify correct and incorrect SET array implementations with reasonable verification time.

Mutation Analysis (MA) is a fault-based simulation technique that is used to measure the quality of testbenches in error (mutant) detection. Although MA effectively reports the living mutants to designers, it suffers from the high simulation cost. This paper presents a probabilistic MA preprocessing technique, Error Propagation Analysis (EPA), to speed up the MA process. EPA can statically estimate the probability of the error propagation with respect to each mutant for guiding the observation-point insertion. The inserted observation-points will reveal a mutant's status earlier during the simulation such that some useless testcases can be discarded later. We use the mutant model from an industrial EDA tool, Certitude, to conduct our experiments on the OpenCores' RT-level designs. The experimental results show that the EPA approach can save about 14% CPU time while obtaining the same mutant status report as the traditional MA approach.

This paper presents an inertial-sensor-based wearable device and its associated stride detection algorithm to analyze gait information for patients with Alzheimer's disease (AD). The wearable gait analysis device is composed of a triaxial accelerometer, a microcontroller, and an RF wireless transmission module. To validate the effectiveness of the proposed device and algorithm, nine AD patients and three healthy controls were recruited to participate a gait analysis experiment. They were asked to mount the device on their foot and walk along a straight line of 40 meters at normal speed. The stride detection algorithm, consisting of procedures of data collection, signal preprocessing, and stride detection, has been developed for acquiring gait feature information from acceleration signals. The advantages of this wearable gait analysis device include the following: 1) It can be used anywhere without any external device, and 2) the stride detection algorithm can acquire gait feature information from acceleration signals automatically and effectively. Experimental results show that the AD patients exhibited a significantly shorter mean stride length and slower mean gait speed than those of the healthy controls. No significant differences in mean stride frequency and mean cadence were observed in the two groups. The variability in the percentage of the stance phase of the AD patients was slightly greater than that of the healthy controls. Based on the above results and discussions with physicians, we conclude that the proposed wearable gait analysis device is a promising tool for automatically analyzing gait information which can serve as indicators for early diagnosis of AD.

This paper presents a logic restructuring technique named node addition and removal (NAR). It works by adding a node into a circuit to replace an existing node and then removing the replaced node. Previous node-merging techniques focus on replacing one node with an existing node in a circuit, but fail to replace a node that has no substitute node. To enhance the node-merging techniques on logic restructuring and optimization, we propose an NAR approach in this paper. We first present two sufficient conditions that state the requirements of added nodes for safely replacing a target node. Then, an NAR approach is proposed to quickly detect the added nodes by performing logic implications based on these conditions. We apply the NAR approach to circuit minimization together with two techniques: redundancy removal and mandatory assignment reuse. We also apply it to satisfiability (SAT)-based bounded sequential equivalence checking (BSEC) to reduce the computation complexity of SAT solving. The experimental results show that our approach can enhance our prior automatic test pattern generation-based node-merging approach. Additionally, our approach has a competitive capability of circuit minimization with 44 times speedup compared to a SAT-based node-merging approach. For BSEC, our approach can work together with other optimization technique to save a total of approximately 39-h verification time for all the benchmarks.

Reducing power consumption has become one of the primary challenges in chip design, and therefore significant efforts are being devoted to find holistic solutions on power reduction from the device level up to the system level. Among a plethora of low power devices that are being explored, single-electron transistors (SETs) at room temperature are particularly attractive. Although prior work has proposed a binary decision diagram-based reconfigurable logic architecture using SETs, it lacks an automated synthesis tool for the device. Consequently, in this work, we develop a product-term-based approach that synthesizes a logic circuit by mapping all its product terms into the SET architecture. The experimental results show the effectiveness and efficiency of the proposed approach on a set of MCNC benchmarks.

Rewiring is a well developed and widely used technique in the synthesis and optimization of traditional Boolean logic designs. The threshold logic is a new alternative logic representation to Boolean logic which poses a compactness characteristic of representation. Nowadays, with the advances in nanomaterials, research on multi-level synthesis, verification, and testing for threshold networks is flourishing. This paper presents an algorithm for rewiring in a threshold network. It works by removing a target wire, and then corrects circuit's functionality by adding a corresponding rectification network. It also proposes a simplification procedure for representing a threshold logic gate canonically. The experimental results show that our approach has 7.1 times speedup compared to the-state-of-the-art multi-level synthesis algorithm, in synthesizing a threshold network with a new fanin number constraint.

This paper presents a logic restructuring technique named node addition and removal (NAR). It works by adding a node into a circuit to replace an existing node and then removing the replaced node. Previous node-merging techniques focus on replacing one node with an existing node in a circuit, but fail to replace a node that has no substitute node. To enhance the node-merging techniques on logic restructuring and optimization, we propose an NAR approach in this work. We first present two sufficient conditions that state the requirements of added nodes for safely replacing a target node. Then, an NAR approach is proposed to fast detect the added nodes by performing logic implications based on these conditions. We also apply the NAR approach to circuit minimization together with two techniques: redundancy removal and mandatory assignment reuse. We conduct experiments on a set of IWLS 2005 benchmarks. The experimental results show that our approach can enhance the state-of-the-art ATPG-based node-merging approach. Additionally, our approach has a competitive capability of circuit minimization with 44 times speedup compared to a SAT-based node-merging approach.

Short term and long term transactions will become very important for both personal and cooperative work involving workflows that use ontologies of the Semantic Web. We describe a way to get around the CAP theorem (the impossibility of simultaneous consistency, availability, and the possibility of network partitioning) and the worst-case infinite delay for any distributed decision-making.

We describe the educational cloud layer of our Cadabia middleware. This layer will permit users to specify the machines which will be used for copies of the materials for various groups that they have joined. This kind of “personal cloud” will help to protect data for both individuals and institutions, while making other data searchable by those who have used similar ontologies.

Node merging is a popular and effective logic restructuring technique that has recently been applied to minimize logic circuits. However, in the previous satisfiability (SAT)-based methods, the search for node mergers required trial-and-error validity checking of a potentially large set of candidate mergers. Here, we propose a new method, which directly identifies node mergers using logic implications without any SAT solving calls. Although the efficiency benefits of the method come at the expense of quality, we further engage the redundancy removal and the wire replacement techniques to enhance its quality. The experimental results show that the proposed optimization method achieves approximately 46 times the speedup while possessing a competitive capability of circuit minimization compared to the state-of-the-art method.

The large number of latches in current designs increase the complexity of formal verification and logic synthesis, since the growth of latch number leads the state space to explode exponentially. One solution to this problem is to find the functional dependencies among these latches. Then, these latches can be identified as dependent latches or essential latches, where the state space can be constructed using only the essential latches. This paper proposes an approach to find the functional dependencies among latches in a sequential circuit by using SAT solvers with the Craig interpolation theorem. In addition, the proposed approach detects sequential functional dependencies existing in the reachable state space only. Experimental results show that our approach could deal with large sequential circuits with up to 1.5 K latches in a reasonable time and simultaneously identify the combinational and sequential dependent latches.

Redundancy Addition and Removal (RAR) is a restructuring technique used in the synthesis and optimization of logic designs. It can remove an existing target wire and add an alternative wire in the circuit such that the functionality of the circuit is intact. However, not every irredundant target wire can be successfully removed due to some limitations. Thus, this paper proposes a new restructuring technique, IRredundancy Removal and Addition (IRRA), which successfully removes any desired target wire by constructing a rectification network which exactly corrects the error caused by removing the target wire.

The sequential depth determines the completeness of bounded model checking in design verification. Recently, a SAT-based method is proposed to compute the sequential depth of a design by searching the state space. Unfortunately, it suffers from the search space explosion due to the exponential growth of design complexity. To alleviate the impact of state space explosion, we propose a search space reduction method. We collect the learned states and consider them constraints for further path searching. Furthermore, we propose a heuristic to guide the SAT-solver to efficiently find a shortest path. The experimental results show that as compared to another method which also enhances the previous SAT-based method using a branch-and-bound strategy, our approach obtains more improvements.

In this paper, we propose a new node merging algorithm using logic implications. The proposed algorithm only requires two logic implications to find the substitute nodes for a given target node, and thus can efficiently detect node mergers. Furthermore, we also apply the node merger identification algorithm for area optimization in VLSI circuits. We conduct experiments on a set of IWLS 2005 benchmarks. The experimental results show that our algorithm has a competitive capability on area optimization compared to a global observability don't care (ODC)-based node merging algorithm which is highly time-consuming. Our speedup is approximately 86 times for overall benchmarks.

The large number of latches in current digital designs increases the complexity of formal verification and logic synthesis, since an increase in latch numbers leads to an exponential expansion of the state space. One solution to this problem is to find the functional dependences among these latches. With the information of functional dependences, these latches can be identified as dependent or essential latches, and the state space can be constructed using only the essential latches. Although much research has been devoted to exploring the functional dependences among latches using binary-decision-diagram (BDD)-based symbolic algorithms, this issue is still unresolved for large sequential circuits. In this paper, we propose a heuristic to identify the dependent latches based on the state-of-the-art work. In addition, our proposed approach detects sequential functional dependences existing in the reachable state space only. The sequential functional dependences can identify additional dependent latches after a specific time frame in order to achieve additional reduction of the state space. Experimental results show that this approach can deal with large sequential circuits with up to 9000 latches in a reasonable time while simultaneously identifying their combinational and sequential dependent latches. For instance, with s13207 in ISCAS'89, 23% of the latches are identified as combinational dependent latches, and an additional 13% of the latches are identified as sequential dependent latches. For the reachability analysis of s13207, with the benefits of dependent-latch identification, 70.70% of the BDD size and 73.32% of the CPU time can be reduced within the same time frame. Furthermore, 2890.76% more states can be reached under the 600 000-s run-time limit.

To construct a reversible sequential circuit, reversible sequential elements are required. This work presents novel designs of reversible sequential elements such as the D latch, JK latch, and T latch. Based on these reversible latches, we construct the designs of the corresponding flip-flops. Then we further discuss the physical implementations of our designs based on electron waveguide Y-branch switch technology. Test costs, including test generation and test application, of reversible sequential circuits with these reversible flip-flops are also discussed. Compared with previous work, the implementation cost of our new designs, including the number of gates and the number of garbage outputs, is significantly reduced. The number of gates in our designs is 47.4% of the designs in previous work on average. The number of garbage outputs in our designs is 25% of the designs in previous work on average.

Simplifying a combinational circuit while preserving its range has a variety of applications, such as combinational equivalence checking and random simulation. Previous approaches use thebinarydecisiondiagram(BDD) technique to compute the range of one circuit and then reconstruct the circuit using the computed range. Although the size of the new circuit is significantly reduced due to the range rearrangement, this method suffers from the BDD blowup problems for large circuits since performing range computation using BDD is memory intensive. Thus, in this paper, we propose a new method for simplifying combinational circuits without explicit range computation. We first introduce a new concept of a stuck-at fault test for a circuit's range, showing that a range untestable stuck-at fault on a primary input (PI) indicates that this PI is range redundant, i.e., it can be removed without affecting the circuit's range. We then present a procedure to determine if a given range stuck-at fault on a PI is untestable. Our method iteratively identifies and removes range-redundant PIs to simplify a combinational circuit without performing range computation. Accordingly, large circuits that BDD-based methods cannot deal with can be handled using our method. We conduct experiments on a set of ISCAS'85 and MCNC benchmarks, and the experimental results show that our approach can minimize circuits such that fewer PIs are left. On average, our approach gets 37.06% reduction in terms of the number of PIs and 36.31% reduction in terms of the node counts.

Exact approaches to combinational equivalence checking, such as automatic test pattern generation-based, binary decision diagrams (BDD)-based, satisfiability-based, and hybrid approaches, have been proposed over the last two decades. Recently, we proposed another exact approach using signal probability. This probability-based approach assigns probability values to the primary inputs and compares the corresponding output probability of two networks via a probability calculation process to assert if they are equivalent. The shortcoming of all these exact approaches is that if two networks are too complex to be handled, their equivalence cannot be determined, even with tolerance. An approximate approach, named the probabilistic approach, is a suitable way to give such an answer for those large circuits. However, despite generally being more efficient than exact approaches, the probabilistic approach faces a major concern of a non zero aliasing rate, which is the possibility that two different networks have the same output probability/signatures. Thus, minimizing aliasing rate is substantial in this area. In this paper, we propose a novel probabilistic approach based on the exact probability-based approach. Our approach exploits proposed probabilistic equivalence checking architecture to efficiently calculate the signature of network with virtually zero aliasing rate. We conduct experiments on a set of benchmark circuits, including large and complex circuits, with our probabilistic approach. Experimental results show that the aliasing rate is virtually-zero, e.g., 10-6013. Also, to demonstrate the effectiveness of our approach on error detection, we randomly inject errors into networks for comparison. As a result, our approach more efficiently detects the error than a commercial tool, Cadence LEC, does. Although our approach is not exact, it is practically useful. Thus, it can effectively complement exact methods to improve the efficiency and effectiveness of combination equivalence checking algorithms.

To construct a reversible sequential circuit, reversible sequential elements are required. This work presents novel designs of reversible sequential elements such as D latch, JK latch, and T latch. Based on these reversible latches, we also construct the designs of the corresponding flip-flops. Comparing with previous work, the implementation cost of our new designs, including the number of gates and the number of garbage outputs is considerably reduced.

Factoring is a logic minimization technique to represent a Boolean function in an equivalent function with minimum literals. When realizing the circuit, a function represented in a more compact form has smaller area. Some Boolean functions even have equivalent forms where each variable appears exactly once, which are known as fanout-free functions. John P. Hayes (Hayes, 1975) had devised an algorithm to determine if a function can be fanout-free and construct the circuit if fanout-free realization exists. In this paper, we propose a property and an efficient technique to accelerate this algorithm. With our improvements, execution time of this algorithm is more competitive with the state-of-the-art method (Golumbic, 2001).

A crosstalk effect leads to increases in delay and power consumption and, in the worst-case scenario, to inaccurate results. With the scale down of technology to deep-submicrometer level, the crosstalk effect between adjacent wires becomes more and more serious, particularly between long on-chip buses. In this paper, we propose a deassembler/assembler technique to eliminate undesirable crosstalk effects on bus transmission. By taking advantage of the prefetch process, where the instruction/data fetch rate is always higher than the instruction/data commit rate, the proposed method incurs almost no penalty in terms of dynamic instruction count. In addition, when the bus width is 128 b, the required number of extra bus wires is only 7 as compared to the 85 extra bus wires needed in the work of Victor and Keutzer.

Symmetric input identification is an important technique in logic synthesis. Previous approaches deal with this problem by building BDDs and developing algorithms to determine symmetric inputs. For the design whose corresponding BDDs cannot be built, BDD-based approaches cannot be applied on this problem. To avoid the limitations of BDD-based approaches, simulation-based methods have been proposed. It is applicable to designs described in arbitrary level, especially to high-level and black box designs. Previous simulation-based approaches focus on determining the inputs of nonequivalence symmetry. In this paper, we propose a simulation-based approach to identify equivalence symmetric inputs. The experimental results on a set of ISCAS-85 and MCNC benchmarks are also presented.

This paper presents a probability based approach to logic equivalence checking. First, a general probability assignment procedure is proposed to uniquely characterize output probability of a network. Thus, the equivalence of two networks can be asserted by the equality of output probabilities. To improve the efficiency of probability calculation, a new encoding scheme and operations are proposed. These encoding scheme and operations also solve the signal correlation issue during the output probability evaluation. As a result, an exact output probability of a network is successfully derived in one pass. Finally, the equivalence of internal gates between two networks are exploited to reduce the number of required input assignments and improve the efficiency of our approach. In the experiments, our approach is compared with a BDD based approach in terms of CPU time and memory usage. The results disclose the potential and limitation of the probabilistic approach to logic equivalence checking

This paper describes an approximate approach for combinational equivalence checking. We propose an architecture such that a virtually-zero aliasing rate is obtained in a single-pass probability calculation. Furthermore, the aliasing rate can be easily configured in various precision by designers. We conduct experiments on a set of ISCAS'85 benchmarks. Experimental results show that with virtually-zero aliasing rate, for example, 10-74, our approach is more efficient than those exact approaches

Redundancy addition and removal (RAR) is a restructuring technique used in the synthesis and optimization of logic designs and physical designs. It finds alternative wires to replace a given target wire without changing the functionality of the circuit. Previous approaches apply two-stage algorithms for this problem. First, they build up a set of candidate wires for the target wire. Second, they perform redundancy test on each candidate wire to determine if it is an alternative wire. Recently, a one-stage algorithm RAM-FIRE (Chang et al., 2003) is proposed. It conducts three logic implications to identify backward alternative wires without trial-and-error redundancy tests. However, the number of alternative wires it can find is smaller than that obtained by the previous two-stage approaches. Here, we propose an improved one-stage algorithm, which only conducts two logic implications. The experimental results show that compared to RAMFIRE, our approach only requires 83% cpu time on average, while obtaining the same number of backward alternative wires. As extending to finding both backward and forward alternative wires, on average our approach gets 157% improvement with 32% cpu time overhead.

We propose a graph automorphism-based algorithm for computing maximal sets of symmetric inputs of circuits. It can be used to identify nonsymmetric inputs in a circuit and enhance the efficiency of input matching, library binding, as well as logic verification problems. We conduct the experiments on some benchmarks. The experimental results demonstrate that our approach distinguishes more non-symmetric inputs than that of previous work.

In a system-on-a-chip (SOC) design, several to hundreds of design blocks or intellectual properties (IPs) are integrated to form a complex function. Prior to verify the functionality of the integrated IPs, it is very important to ensure the correctness of the port connections among these IPs. This work addresses the problem of verification on port connections while IPs are integrated into a larger block or a system, and presents a new connection model and the corresponding error model for port connections. An algorithm providing the minimum pattern set and a general verification flow used to verify port connections are also proposed.

This paper describes the xml definition of class algebra which is available at http://xbean.cs.ccu.edu.tw/~dan/classAlgebra.xml . A sample user-defined ontology document and instance document are available at http://xbean.cs.ccu.edu.tw/~dan/userOntology.xml and http://xbean.cs.ccu.edu.tw/~dan/userInstances.xml . The class algebra ontology is very similar to the OWL ontology, but it uses its own definition of pointers for non-partOf relations. This simplifies the underlying theory as well as the syntax. The same syntax is used to define the ontology (i.e. the schema) as well as instance documents. The class algebra ontology has sufficient information to enable conversion between class algebra instance documents, SQL tables, and Java persistent objects, all of which can be queried by class algebra queries and updated by class algebra assignment operators, RMI calls, or SOAP method calls. The state-space graph of all possible orderings of class algebra operators is searchable by efficient constraint-based search techniques. Operators include guarded class algebra assignments as well as traditional SOAP or RMI method calls.

This paper presents an automatic interconnection rectification (AIR) technique to correct the misplaced interconnection occurred in the integration of a SoC design automatically. The experimental results show that the AIR can correct the misplaced interconnection and therefore accelerates the integration verification of a SoC design.

Embedded cores are being increasingly used in large system-on-a-chip (SoC) designs. The high complexity of SoC designs lead the design verification to be a challenge for system integrators. This paper presents an automatic interconnection rectification (AIR) technique based on the port order fault model to detect, diagnose, and correct the misplacements of interconnection that occurred in the integration of a SoC design automatically. The experiments are conducted on combinational and sequential benchmarks. Experimental results show that the AIR can correct the misplaced interconnection exactly within reasonable efforts and, therefore, accelerates the integration verification of SoC designs.

Embedded cores are being increasingly used in the design of large system-on-a-chip (SoC). Because of the high complexity of SoC, the design verification is a challenge for system integrators. To reduce the verification complexity, the port-order fault (POF) model has been used for verifying core-based designs (Tang and Jou, 1998). In this paper, we present an automatic-verification pattern generation (AVPG) for SoC design verification based on the POF model and perform experiments on combinational and sequential benchmarks. Experimental results show that our AVPG can efficiently generate verification patterns with high POF coverage.

Embedded cores are being increasingly used in the design of large system-on-a-chip (SoC). Because of the high complexity of SoC, the design verification is a challenge for system integrators. To reduce the verification complexity, the port-order fault (POF) model was proposed. It has been used for verifying core-based designs and the corresponding verification pattern generation has been developed. Here, the authors present an automorphic technique to improve the efficiency of the automatic verification pattern generation (AVPG) for SoC design verification based on the POF model. On average, the size of pattern sets obtained on the ISCAS-85 and MCNC benchmarks are 45% smaller and the run time decreases 16% as compared with the previous results of AVPG.

Embedded cores are being increasingly used in the design of large system-on-a-chip (SoC). Because of the high complexity of SoC the design verification is a challenge for the system integrator. To reduce the verification complexity, the port order fault (POF) model has been used for verifying core-based designs and the corresponding verification pattern generation has been developed. Here we present an automorphic technique to improve the efficiency of the automatic verification pattern generation (AVPG) for SoC design verification based on POF model. On average, the size, of pattern sets obtained on the ISCAS-85 and MCNC benchmarks are 45% smaller and the run time decreases 16% as compared with the results of AVPG.