This paper mathematically models a constant-function automated market maker (CFAMM) position as a portfolio of exotic options, known as perpetual American continuous-installment (CI) options. This model replicates an AMM position's delta at each point in time over an infinite time horizon, thus taking into account the perpetual nature and optionality to withdraw of liquidity provision. This framework yields two key theoretical results: (a) It proves that the AMM's adverse-selection cost, loss-versus-rebalancing (LVR), is analytically identical to the continuous funding fees (the time value decay or theta) earned by the at-the-money CI option embedded in the replicating portfolio. (b) A special case of this model derives an AMM liquidity position's delta profile and boundaries that suffer approximately constant LVR, up to a bounded residual error, over an arbitrarily long forward window. Finally, the paper describes how the constant volatility parameter required by the perpetual option can be calibrated from the term structure of implied volatilities and estimates the errors for both implied volatility calibration and LVR residual error. Thus, this work provides a practical framework enabling liquidity providers to choose an AMM liquidity profile and price boundaries for an arbitrarily long, forward-looking time window where they can expect an approximately constant, price-independent LVR. The results establish a rigorous option-theoretic interpretation of AMMs and their LVR, and provide actionable guidance for liquidity providers in estimating future adverse-selection costs and optimizing position parameters.

This paper introduces HEMVM, an innovative heterogeneous blockchain framework that seamlessly integrates diverse virtual machines (VMs), including the Ethereum Virtual Machine (EVM) and the Move Virtual Machine (MoveVM), into a unified system. This integration facilitates interoperability while retaining compatibility with existing Ethereum and Move toolchains by preserving high-level language constructs. HEMVM's unique cross-VM operations allow users to interact with contracts across various VMs using any wallet software, effectively resolving the fragmentation in user experience caused by differing VM designs. Our experimental results demonstrate that HEMVM is both fast and efficient, incurring minimal overhead (less than 4.4 %) for intra-VM transactions and achieving up to 9300 TPS for cross-VM transactions. Our results also show that the cross-VM operations in HEMVM are sufficiently expressive to support complex decentralized finance interactions across multiple VMs. Finally, the parallelized prototype of HEMVM shows performance improvements up to 44.8 % compared to the sequential version of HEMVM under workloads with mixed transaction types.

Many central banks are researching and piloting digital versions of fiat money, specifically retail central bank digital currencies (CBDCs). Core to many discussions revolving around these systems’ design is the ability to perform transactions even without network connectivity. While this approach is generally believed to provide additional degrees of freedom for user privacy, the lack of direct involvement of third parties in these offline transfers also interferes with key regulatory requirements that need to be accommodated in the financial space. This paper presents a compliance-by-design approach to evaluate technologies that can balance privacy with anti-money laundering and counter-terrorism financing (AML/CFT) measures. It classifies privacy design options and corresponding technical building blocks for offline CBDCs, along with their impact on AML/CFT measures, and outlines commonalities and differences between offline and online solutions. As such, it provides a conceptual framework for further techno-legal assessments and implementations.

Many central banks are researching and piloting digital versions of fiat money, specifically retail Central Bank Digital Currencies (CBDCs). Core to these systems’ design is the ability to perform transactions even without network connectivity. Due to the lack of direct involvement of third parties in these offline transfers, various regulatory requirements that are key in the financial space need to be accommodated. This paper deploys a compliance-by-design approach to evaluate technologies that can balance privacy with anti-money laundering and counterterrorism financing (AML/CFT) measures. It classifies privacy design options and corresponding technical building blocks for offline CBDCs, along with their impact on AML/CFT measures, and outlines commonalities and differences between offline and online solutions. As such, it provides a conceptual framework for further techno-legal assessments and implementations.

This paper investigates the current state of option trading platforms for cryptocurrencies, encompassing both centralized and decentralized exchanges. Option contracts in cryptocurrency markets offer functionalities akin to traditional markets, providing investors with tools to mitigate risks, particularly those arising from price volatility. The paper discusses these applications of option contracts in the context of decentralized finance, emphasizing their utility in managing market uncertainties. Despite a recent surge in the trading volume of option contracts on cryptocurrencies, decentralized platforms account for less than $1 \%$ of this total volume. Hence, this paper takes a closer look by examining the design choices of these platforms to understand the challenges hindering their growth and adoption. It identifies technical, financial, and adoption-related challenges faced by decentralized exchanges. Subsequently, the paper provides commentary on existing platform responses.

This paper introduces BAKUP, a smart contract design that insures decentralized finance users against the vulnerability risks in third-party platforms. Apart from providing an automated claim payout, the modular structure of BAKUP brings harmonization among three conflicting features: resilience against vulnerabilities, flexibility of the underwritten policies, and capital efficiency. An immutable core module performs basic accounting while ensuring robustness against external vulnerabilities; a customizable oracle module enables the underwriting of novel policies, and a peripheral (optional) yield module allows users to independently manage additional yield without interfering with the risk management of fellow participants. User payoff is implemented using binary conditional ERC20 tokens tradable on automated market maker (AMM)-based exchanges.

This paper presents OVer, a framework designed to automatically analyze the behavior of decentralized finance (DeFi) protocols when subjected to a "skewed" oracle input. OVer firstly performs symbolic analysis on the given contract and constructs a model of constraints. Then, the framework leverages an SMT solver to identify parameters that allow its secure operation. Furthermore, guard statements may be generated for smart contracts that may use the oracle values, thus effectively preventing oracle manipulation attacks. Empirical results show that OVer can successfully analyze all 10 benchmarks collected, which encompass a diverse range of DeFi protocols. Additionally, this paper illustrates that current parameters utilized in the majority of benchmarks are inadequate to ensure safety when confronted with significant oracle deviations. It shows that existing ad-hoc control mechanisms such as introducing delays are often in-sufficient or even detrimental to protect the DeFi protocols against the oracle deviation in the real-world.

We present the Layered Merkle Patricia Trie (LMPT), a performant storage data structure for processing transactions in high-throughput systems when compared to traditional Merkle Patricia Tries used in Ethereum clients. LMPTs keep smaller intermediary tries in memory to alleviate read and write amplification from high-latency disk storage. As an additional feat, they also allow for the I/O and transaction verifier threads to be scheduled in parallel and independently. LMPTs can ultimately reduce significant I/O traffic that happens on the critical path of transaction processing. Empirical results show that LMPTs can process up to$\times6$more transactions per second on real-life ERC20 smart contract workloads when compared to existing Ethereum clients.

This paper presents Mobius, the first cost-efficient state sharding design that remains consensus mechanism agnostic and guarantees atomicity for cross-shard smart contract transactions. In particular, to address the challenges posed by the growing blockchain state, Mobius enables its participants to verify all transactions while only storing a partial state. Unlike previous state sharding systems, the proposed protocol uses a novel vector commitment data structure to reduce the network bandwidth overhead via proof aggregation. Further, it utilizes a novel epoch-based multi-phase commitment technique for guaranteeing atomicity in cross-shard transactions. Experiments presented here show that Mobius reduces the disk requirement of each participant linearly with respect to the number of shards. Further, it presents a 4.7-7.3x lower network bandwidth overhead when compared to existing state-of-the-art state sharding systems. The outcomes also confirm that existing smart contracts can operate on Mobius in cross-shard scenarios without modifications.

This paper presents Deeper, a design for a decentralized exchange that enhances the average active liquidity via reserve sharing. By doing this, it addresses the problem of shallow liquidity in low trading volume token pairs. Deeper allows liquidity providers of multiple trading pairs against a common token to share liquidity. This is achieved by creating a common reserve pool for the shared token that is accessible by each trading pair. Independent from the shared liquidity, providers are free to add liquidity to individual token pairs without any restriction. The trading between one token pair does not affect the price of other token pairs even though the reserve of the shared token changes. The proposed design is an extension of concentrated liquidity market maker-based DEXs that is simple enough to be implemented on smart contracts. Experiments show that for a batch consisting of 8 trading pairs, Deeper enhances liquidity by over 2.6 − 5.9 ×. This enhancement in liquidity can be increased further by increasing participating tokens in the shared pool.

Blockchain-based smart contracts enable the creation of decentralized applications, which often handle assets of considerable value. While the underlying platforms guarantee the correctness of smart-contract execution, they cannot ensure that the code of a contract is correct. Today, as evidenced by a number of recent security breaches, developers still have a hard time making contracts that work properly.Even though these incidents often exploit contract interaction, prior work on smart-contract verification, vulnerability discovery, and secure development typically considers only individual contracts in isolation. To address this gap, we introduce theVeriSolidframework for the formal verification of contracts that are specified using a abstract state machine based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify the behavior of a set of interacting contracts at a high level of abstraction.VeriSolidallows the generation of Solidity code that is functionally and behaviorally equivalent to verified models, which enables the creation of correct-by-design smart contracts. We additionally introduce a graphical notation (calleddeployment diagrams) for specifying possible interactions between contract types. Based on this notation, we present a framework for the automated verification, generation, and deployment of contracts that conform to a deployment diagram. To demonstrate the applicability ofVeriSolid, we translate existing Ethereum Improvement Proposal (EIP) specifications to temporal properties for two of the most popular contract interfaces: ERC20 and ERC721. We also show you how to write code for the ERC20 and ERC721 interfaces in a way that is safe, and we do this by usingVeriSolid. We evaluate our framework on 726 contracts that are currently deployed on the Ethereum blockchain, which include 267 ERC20 and 459 ERC721 contracts. Our experiments indicate that 18% of ERC20 contracts and 4% of ERC721 contracts fail to satisfy the EIP specifications.

With the emergence of decentralized finance, smart contracts and their users become more and more susceptible to expensive exploitations. This paper investigates the price gouging transaction order dependency vulnerabilities in smart contracts. A static analysis based approach is proposed to automatically locate and rectify such vulnerabilities, and a prototype tool using Slither, a static analyzer for Solidity, is also developed. All in all, empirical results on a benchmark suite containing 51 Solidity smart contracts show that the proposed methodology can be used successfully to both detect such vulnerabilities and rectify them, or to certify that a Solidity smart contract under question does not contain such vulnerabilities.

We present the Layered Merkle Patricia Trie (LMPT), a performant storage data structure for processing transactions in high-throughput systems when com-pared to traditional Merkle Patricia Tries used in Ethereum clients. LMPTs keep smaller intermediary tries in memory to alleviate read and write amplification from high-latency disk storage. As an additional feat, they also allow for the I/O and transaction verifier threads to be scheduled in parallel and independently. LMPTs can ultimately reduce significant I/O traffic that happens on the critical path of transaction processing. Empirical results presented here confirm that LMPTs can process up to × 6 more transactions per second on real-life workloads when compared to existing Ethereum clients.

This paper presents SigVM, the first blockchain virtual machine that extends EVM to support an event-driven execution model, enabling developers to build truly decentralized smart contracts. Contracts in SigVM can emit signal events, on which other contracts can listen. Once an event is triggered, corresponding handler functions are automatically executed as signal transactions. We build an end-to-end blockchain platform SigChain and a contract language compiler SigSolid to realize the potential of SigVM. Experimental results show that our benchmark applications can be reimplemented with SigVM in a truly decentralized way, eliminating the dependency on centralized and unreliable mechanisms like off-chain relay servers. The development effort of reimplementing these contracts with SigVM is small, i.e., we modified on average 3.17% of the contract code. The runtime and the gas overhead of SigVM on these contracts is negligible.

With the rapid adoption of new technologies and applications, e.g., the Internet of Things, 5G/6G communication networks, big data analytics, and artificial intelligence, a deluge of devices are being connected to the network, thus generating a large amount of data. The collection, processing, and analysis of this vast amount of data are essential to help people and enterprises gain valuable information, make sensible decisions, and subsequently improve the quality of people’s lives. However, the underlying communication networks are thus facing a new number of unprecedented challenges. Managing these large numbers of devices in a scalable and secure manner is bringing significant challenges to the infrastructure construction, maintenance, and management of the communication networks. Recurring data privacy breaches and the lack of control make Internet users and enterprises less willing to provide valuable data for processing and analysis.

Central banks and governments all over the world are increasingly exploring digital versions of fiat money, known as retail Central Bank Digital Currencies (CBDCs). Most initiatives rely on Distributed Ledger Technologies and are presented as alternatives to physical cash. Consequently, anonymity-related regulatory questions have naturally started to arise in terms of Anti-Money Laundering and Counter-Terrorist Financing compliance. Against this backdrop, this paper provides a techno-legal taxonomy of approaches to balance privacy and transparency in CBDCs without thwarting accountability, but it also underlines cross-sectoral impacts. The contribution heeds regulation-by-design as its core methodological foundation, with Privacy-Enhancing Technologies as the relevant use case. Thus, it highlights that not only technology aids legal purposes, but also that some regulatory requirements ought to be designed into technology for one to reach agreed-upon results and/or standards.

Due to the excessive cost associated with manual RTL design debugging, automated tools are often employed to identify a set of suspect bug locations. To further accelerate the process, one observes that the anytime behavior of these tools allows partial results to be analyzed before the suspect search is complete. Thus, it is preferable for the tool to maximize the number of suspects that are found in the early stages of its search. Toward this end, this article proposes a new SAT-based debugging algorithm which predicts where solutions are most likely to be found and prioritize examining these locations. Two techniques are proposed to predict solution locations by learning from historical debug data. The first technique does so using belief propagation on a probabilistic graph, while the second trains a neural network to classify candidate suspects as solutions or nonsolutions. Intensive empirical evaluation demonstrates that these techniques can predict suspect sets with accuracies of 81% and 87%, respectively, but the second method requires more training data and careful hyperparameter tuning in order to do so. Furthermore, when guided by these suspect prediction models, the proposed debugging algorithm finds an average of 83% more suspects within a given amount of time.

Automated debugging tools based on Boolean Satisfiability (SAT) have greatly alleviated the time and effort required to diagnose and rectify a failing design. Practical experience shows that long-running debugging instances can often be resolved faster using partial results that are available before the SAT solver completes its search. In such cases it is preferable for the tool to maximize the number of suspects it returns during the early stages of its deployment. To capitalize on this observation, this paper proposes a directed SAT-based debugging algorithm which prioritizes examining design locations that are more likely to be suspects. This prioritization is determined by suspect2vec --- a model which learns from historical debug data to predict the suspect locations that will be found. Experiments show that this algorithm is expected to find 16% more suspects than the baseline algorithm if terminated prematurely, while still retaining the ability to find all suspects if executed to completion. Key to its performance and a contribution of this work is the accuracy of the suspect prediction model. This is because incorrect predictions introduce overhead in exploring parts of the search space where few or no solutions exist. Suspect2vec is experimentally demonstrated to outperform existing suspect prediction methods by an average accuracy of 5--20%.

Model checking of safety properties is fundamental in formal verification. When a safety property is found to hold, the model checker provides (at best) a machine-checkable certificate that gives limited insight to users and little confidence that the check passes for the “right” reasons, rather than due to e.g., vacuity or unjustified assumptions. Recently, inductive validity cores (IVCs) have been developed to address this issue. In this paper, we lift several algorithms from the field of UNSAT core extraction in order to compute minimal IVCs of hardware safety checking problems. The MARCO algorithm extracts all minimal cores of an UNSAT formula by efficiently exploring the formula's power set, and has already been applied to compute IVCs in software safety checking. The CAMUS algorithm for UNSAT core extraction exploits a duality between minimal correction subsets (MCSes) of a formula and minimal UNSAT cores. We adapt the algorithms to the hardware IVC context, construct a hybrid algorithm that subsumes both CAMUS and MARCO, and introduce novel domain-specific optimizations. Several instances of the hybrid algorithm are presented (including CAMUS and MARCO themselves, among other novel variants) and evaluated empirically on hardware model checking competition circuits, demonstrating the practicality of the proposed algorithm.

Knowledge graph embeddings are instrumental for representing and learning from multi-relational data, with recent embedding models showing high effectiveness for inferring new facts from existing databases. However, such precisely structured data is usually limited in quantity and in scope. Therefore, to fully optimize the embeddings it is important to also consider more widely available sources of information such as text. This paper describes an unsupervised approach to incorporate textual information by augmenting entity embeddings with embeddings of associated words. The approach does not modify the optimization objective for the knowledge graph embedding, which allows it to be integrated with existing embedding models. Two distinct forms of textual data are considered, with different embedding enhancements proposed for each case. In the first case, each entity has an associated text document that describes it. In the second case, a text document is not available, and instead entities occur as words or phrases in an unstructured corpus of text fragments. Experiments show that both methods can offer improvement on the link prediction task when applied to many different knowledge graph embedding models.

We propose a framework for predicting erroneous design components from partially observed solution sets that are found through automated debugging tools. The proposed method involves learning design component dependencies by using historical debugging data and representing these dependencies by means of a probabilistic graph. Using this representation, one can run a debugging tool non-exhaustively, obtain a partial set of potentially erroneous components and then predict the remaining by applying a cost-effective belief propagation pass. The method can reduce debugging runtime when it comes to multiple debugging sessions by 15x on the average while achieving a 91% average prediction accuracy.

In the modern design cycle, substantial manual effort is required to correct failed liveness properties due to the limited availability of automated tools. To address this limitation, this paper introduces two techniques to diagnose register transfer level errors that manifest in the form of erroneously unreachable states, which represent a common form of liveness property failure. The first uses steps of reachable state-space over-approximation and traditional debugging to compute a subset of the solutions that make a target state reachable. The second solves a series of unbounded model checking problems using an enhanced model of the circuit's transition relation to compute the complete solution set to the problem. The proposed techniques are complementary to each other and present the user with a configurable tradeoff between runtime and resolution of the returned solution set. Empirical results on OpenCores and HWMCC'15 circuits confirm the effectiveness of the approaches and demonstrate the tradeoffs between them.

We propose an automated failure triage framework for register transfer level debugging in functional verification regression flows which unifies three critical aspects of the problem: the approximation of the general location of root-cause(s) in the design under verification, the binning of all related failures generated by regression runs, and the distribution of these binned failures to the proper engineer(s) for detailed analysis. The proposed triage engine entails two novel methodologies. The first is a classification framework that mines information from SAT-based debugging and simulation to probabilistically reason about the relation of root-causes with their respective failing verification traces. This enables the construction of a priority ranking for these root-causes, and can effectively guide debugging by focusing resources on high-priority root-causes. Second, we propose a formulation of failure binning as exemplar-based clustering for grouping and distributing failing traces to the proper engineering team(s). Experiments on industrial designs show that the proposed methodology achieves 84% and 81% accuracy when it comes to failure grouping and distribution, respectively, with only a 6.5% runtime overhead over existing debugging state-of-the-art techniques.

Automated debugging techniques can significantly reduce the manual effort required to localize RTL errors. These techniques return to the user a set of RTL locations where a change can correct erroneous behavior. However, each location must be manually investigated. This problem is exacerbated by the increasing amount of failures in the modern regression verification cycle. Recent work in clustering-based revision debugging mitigates this cost by ranking revisions based on their likelihood of having introduced an error. This work presents a perceptron based approach to revision debugging that can be extended to leverage the revision history of a design directly. Perceptrons are trained using labeled revisions from the design history. They are then used to predict the probability that a revision has introduced an error. The proposed methodology performs competitively with the state-of-the-art, but can be extended to handle more features. This allows for an automated regression debug flow integrated with Version Control and Issue Tracking Systems.

In recent years, IC3 has enjoyed wide adoption by academia and industry as an unbounded model checking engine. The core algorithm works by learning lemmas that, given a safe property, eventually converge to an inductive proof. As such, its runtime performance is heavily dependent upon “pushing” (or “promoting”) important lemmas, possibly by discovering additional supporting lemmas. More recently, Quip has emerged to be a complementary extension behind the reasoning capabilities of IC3 as it allows it to target particular lemmas for pushing. This also raises the following question: which lemmas should be promoted? To that end, this paper extends the reasoning capabilities of IC3 and Quip using special SAT queries to find support sets that represent fine-grained information on which lemmas are required to push other lemmas. Further, this paper presents an IC3-based algorithm called Truss (Testing Reachability Using Support Sets) that uses support sets to identify sets of lemmas that may be close to forming an inductive proof. The set is targeted for promotion as a cohesive unit. If any of the lemmas cannot be promoted, the entire set is abandoned and a new set excluding that lemma is found. In the presented framework, there are two reasons why a lemma cannot be promoted: either because it blocks a known reachable state (in which case, the lemma is permanently marked as bad), or because lemma promotion exceeds a specified amount of effort (in which case the lemma is temporarily marked as ugly). Intuitively, the proposed approach allows the algorithm to construct a proof more quickly by focusing on the important yet easily-pushed lemmas. Experiments on the HWMCC'15 benchmark set show a significant improvement against existing practices. Compared to Quip, our algorithm solves 17 more problem instances and it offers an impressive 1.77× speedup.

In modern hardware design, substantial manual effort is required to fix a design when verification discovers a state unreachable. This paper addresses this growing pain where given an unreachable target state, a methodology is presented to return all design locations where a change can be implemented to make the target state reachable. In contrast to previous state reachability rectification techniques that use bounded model checking, our approach addresses the issue using unbounded model checking. It first enhances the circuit transition relation by inserting a novel error model construction at each suspect location. An unbounded model checking algorithm is then applied to the enhanced transition relation to find which of the suspect locations can be changed to make the target state reachable. The use of unbounded model checking allows it to identify the complete problem solution set. As an added benefit, it also returns a proof that no further solution(s) exist in the form of an inductive invariant. Empirical results on industrial designs confirm the theoretical and practical gains of this approach.

Modern digital systems are growing in size and complexity, introducing significant organizational and verification challenges in the design cycle. Verification today takes as much as 70% of the design time with debugging being responsible for half of this effort. Automation has mitigated part of the resource-intensive nature of rectifying erroneous designs. Nevertheless, most tools target failures in isolation. Since regression verification can discover myriads of failures in one run, automation is also required to guide an engineer to rank them and expedite debugging. To address this growing regression pain, this paper presents a framework that utilizes traditional machine learning techniques along with historical data in version control systems and the results of functional debugging. Its aim is to rank revisions based on their likelihood of being responsible for a particular failure. Ranking prioritizes revisions that ought to be targeted first, and therefore it speeds-up the localization of the error source. This effectively reduces the number of debug iterations. Experiments on industrial designs demonstrate a 68% improvement in the ranking of actual erroneous revisions versus the ranking obtained through existing industrial methodologies. This benefit arrives with negligible run-time overhead.

Design debugging poses a major bottleneck in modern VLSI CAD flows, consuming up to 60% of the verification cycle. The debug pain, however, worsens in regression verification flows at the pre-silicon stage where myriads of failures can be exposed. These failures need to be properly grouped and distributed among engineers for further analysis before the next regression run commences. This high-level and complex debug problem is referred to as failure triage and largely remains a manual task in the industry. In this paper, we propose an automated failure triage flow that mines information from both failing and passing tests during regression, and automatically performs a coarse-grain partitioning of the failures. The proposed framework combines formal tools and novel statistical metrics to quantify the likelihood of specific design components being the root-cause of the observed failures. These components are then used to represent failures as high-dimensional objects, which are grouped by applying data-mining clustering algorithms. Finally, the generated failure clusters are automatically prioritized and passed to the best suited engineers for detailed analysis. Experimental results show that the proposed approach groups related failures together with 90% accuracy on the average, and efficiently prioritizes the responsible design errors for 86% of the exposed failures.

Formal verification has increased efficiency by detecting corner case design bugs but it has also introduced new challenges when failures are detected. Once a counter-example is returned by a formal tool, the user typically does not know if the failure is caused by a design bug, an incorrectly written assertion, or a missing assumption. Previous work in debug automation has focused on the former two cases. This paper introduces a novel methodology to automatically debug missing assumptions. It begins by generating multiple formal counter-examples for the error. Next, a function is extracted from these counter-examples that encodes the input combinations that cause the assertion to fail. This function is later used to generate a list of fixed cycle assumptions that prevent failures similar to the generated counter-examples. These filtered assumptions can then be used as hints for the actual missing assumption. Further, if a missing assumption is not the cause of the failure, the method offers the additional benefit that the counter-examples it generates can be utilized to debug the RTL and/or the assertion. An extensive set of experimental results on OpenCores designs and assertions show that the number of generated assumptions can be reduced by an average of 38% using ten counter-examples, while an average of 28 assumptions is returned to the user.

Modern designs are growing in size and complexity, becoming increasingly harder to verify. Today, they are architected to include multiple clock domains as a measure to reduce power consumption. Verifying them proves to be a computationally intensive and challenging task as it requires their clocks to be synchronized. To achieve synchronization, existing Boolean satisfiability-based methodologies add hardware to combine the clock domains before transforming them into their iterative logic array representation (ILA). As a consequence, this results in the addition of redundant time-frames adding overhead during verification. This paper introduces a novel framework to verify designs with multiple clocks using Quantified Boolean Formula satisfiability (QBF). We first present a formulation that models an ILA representation with symbolic universal quantification to achieve synchronization. This is later extended with the use of a clock divider to overcome inefficiencies. The net effect is the reduction in the number of redundant time-frames. Furthermore, the usage of QBF results in significant memory savings when compared to traditional methods. Experiments on bounded model checking demonstrate memory reductions of 76% on average with competitive run-time performance.

Regression verification at the pre-silicon stage has experienced a dramatic boost in capabilities over the past years. With the aid of assertions, improved simulation coverage and formal verification tools, a vast amount of trace data and myriads of failures are often generated after each regression run. Along these lines, modern flows face an emerging need to appropriately categorize, prioritize and distribute these failures to the engineer(s) best-suited for detailed debugging of each failure. This task is known as failure triage. Despite its resource-intensive nature, triage remains a predominantly manual process. In this work, an automated data-mining failure triage framework is introduced that mines simulation and SAT-based design debugging data, uncovers relations among verification failures and automatically groups the related ones together. The core characteristic of the framework is a novel feature-based representation for verification failures and a new multiple-pass clustering strategy that surpass previous methodologies in accuracy, robustness and flexibility. The proposed triage engine achieves an 89% average accuracy in failure categorization and compared to existing solutions, it reduces the number of misplaced verification failures by 47% on the average.

Register-transfer level (RTL) debug has become a resource-intensive bottleneck in modern very large scale integration computer-aided design flows, consuming as much as 32% of the total verification effort. This paper aims to advance the state-of-the-art in automated RTL debuggers, which return all potential bugs in the RTL, called solutions, along with corresponding corrections. First, an iterative algorithm is presented to compute the dominance relationships between RTL blocks. These relationships are leveraged to discover implied solutions with every new solution, thus significantly reducing the number of formal engine calls. Furthermore, a modern Boolean satisfiability (SAT) solver is tailored to detect debugging nonsolutions, sets of RTL blocks guaranteed to be bug-free, and to imply other nonsolutions using the precomputed RTL dominance relationships. Extensive experiments on industrial designs show a three-fold reduction in the number of SAT calls due to solution implications, coupled with faster SAT run-times due to nonsolution implications, resulting in a 2.63x overall speedup in total SAT solving time, demonstrating the robustness and practicality of the proposed approach.

The conflicting yet increasing demand for high performance and low power in multi-functional chips has pushed techniques for power reduction to the forefront of VLSI design. Although recent developments have automated most of the low power implementations, designers often manually modify the circuit in order to achieve further power savings. This human intervention is often paved with many errors that are bound to typical logic functional failures. Debugging these errors can be a resource intensive process that requires considerable manual effort. This discourages engineers and achieving power savings at the micro level of the design sometimes remains unrealized. This paper proposes a novel debugging methodology to rectify erroneous clock-gating implementations. With the use of Partial Max-SAT, the method localizes and rectifies the design error introduced in the circuit during a clock-gating implementation. The net effect of the proposed methodology leads to shorter debug time ensuring additional power savings. Extensive experiments on benchmark circuits confirm the effectiveness of the approach.

With the growing complexity of current designs and shrinking time-to-market, traditional ATPG methods fail to detect all electrical faults in the design. Debug teams have to spend considerable amount of time and effort to identify these faults during post silicon debug. This work proposes off-chip analysis to speed-up the effort of identifying hard-to-find electrical faults that are not detected using conventional test methods, but cause the chip to crash during functional testing or silicon-bring-up. With the goal of reducing the search space for reconstructing the failure trace path, formal methodology is used to analyze the reachable states along the path. Isolating the root cause of failure is also accelerated. Moreover, we propose a forward traversal technique on selected few possible faults to generate a complete failure trace starting from the initial state to the crash state. Experimental results show that the proposed approach can lead to a 44% reduction in actual silicon run with a commensurate reduction in off-chip debug time.

The ever growing demand for functionally robust and error-free industrial electronics necessitates the development of techniques that will prohibit the propagation of functional errors to the final tape-out stage. This paramount requirement in the semiconductor world is imposed by the equivocal observation that functional errors slipping to silicon production introduce immense amounts of cost and jeopardize chip release dates. Functional verification and debugging are burdened with the tedious task of guaranteeing logic functionality early in the design cycle. In this paper, we present an automated method for the very first stage of functional debugging, called failure triage. Failure triage is the task of analyzing large sets of failures, grouping together those that are likely to be caused by the same design error, and then allocating those groups to the appropriate engineers for fixing. The introduced framework instruments techniques from the machine learning domain combined with the root cause analysis power of modern SAT-based debugging tools, in order to exploit information from error traces and bin the corresponding failures using clustering algorithms. Preliminary experimental results indicate an average accuracy of 93 % for the proposed failure triage engine, which corresponds to a 43 % improvement over conventional automated methods.

With the growing popularity of hand-held battery-powered devices, leakage power is a major concern in the nanometer CMOS era. Power gating technique is an effective and widely adopted solution to this problem. The challenge of implementing power gating is the sizing and placement of the sleep transistors that are used to gate the power supply. In a placed design, due to non-uniform current demand of logic cells, some regions of the chip can have sleep transistors with very high current demand, causing power grid noise violations. Identifying these regions early in the design cycle is critical to the success of power gating implementation. This paper presents a novel methodology to calculate the current demand of each sleep transistor and locate regions in the chip where multiple sleep transistors experience very high current demand. In this paper, we model the spatial locality of the current drawn by each logic cells in the form of a bounding box. We explore techniques to identify the appropriate size of the bounding boxes. Furthermore, we extend the current distribution technique to handle placement blockages that do not share the sleep transistor network of the chip. Experimental results on industrial circuits show that the proposed algorithm can identify over 90% of such regions with a 20× run-time reduction compared to state-of-the-art commercial CAD tool.

Functional verification has become one of the most time-consuming tasks in the very large scale integration design flow accounting for up to 57% of the total project time. The largest component of this task is that of design debugging due to its resource-intensive manual nature. With the ever growing size of modern designs and their error traces, the complexity of the debugging problem poses a great challenge to automated debugging techniques. To overcome this challenge, this paper introduces a novel path-directed abstraction and refinement algorithm for design debugging to manage excessive error trace lengths. A sliding window of the error trace is iteratively analyzed in a time-windowing framework, which is made possible by the use of the path-directed abstraction. This abstraction forms a concise approximation of nonmodeled parts of the error trace while simultaneously providing an efficient representation for refinement. The result is an algorithm that dramatically reduces the memory requirements of debugging while mitigating the incomplete results of past techniques. Experimental results on industrial designs with long error traces show that the proposed approach can analyze traces that are 64.6% longer while simultaneously decreasing peak memory usage compared to previous work.

The growing size, density and complexity of modern VLSI chips are contributing to an increase in hardware faults and design errors in the silicon, decreasing manufacturing yield and increasing the design cycle. The use of Partially Programmable Circuits (PPCs) has been recently proposed for yield enhancement with very small overhead. This new circuit structure is obtained from conventional logic by replacing some subcircuits with programmable LUTs. The present paper lays the theoretical groundwork for evaluating PPCs with Quantified Boolean Formula (QBF) satisfiability. First, QBF models are constructed to calculate the fault tolerance and design error tolerance of a PPC, namely the percentages of faults and design errors that can be masked using LUT reconfigurations. Next, zero-cost Engineering Change Order (ECO) in PPCs is investigated. QBF formulations are given for performing ECOs, and for quantifying the ECO coverage of a PPC architecture. Experimental results are presented evaluating PPCs from [1], demonstrating the applicability and accuracy of the proposed formulations.

With the growing size of modern designs and more strict time-to-market constraints, design errors unavoidably escape pre-silicon verification and reside in silicon prototypes. As a result, silicon debug has become a necessary step in the digital integrated circuit design flow. Although embedded hardware blocks, such as scan chains and trace buffers, provide a means to acquire data of internal signals in real time for debugging, there is a relative shortage in methodologies to efficiently analyze this vast data to identify root-causes. This paper presents an automated software solution that attempts to fill-in the gap. The presented techniques automate the configuration process for trace-buffer based hardware in order to acquire helpful information for debugging the failure, and detect suspects of the failure in both the spatial and temporal domain.

The past decade has seen a disproportionate amount of resources dedicated towards verification as compared to actual design. It is reported that one third of this overhead is due to the resource-intensive task of manual debugging. To relieve this burden, this work introduces the novel concept of path directed debugging within a window-based abstraction/refinement framework. The algorithm divides the error trace into non-overlapping time-windows where each window is analyzed separately. Subsequent windows are replaced with abstracted over-approximations derived from failing paths in the time domain. Using this abstracted model, each solution found is processed through an additional verification step that removes spurious solutions and simultaneously refines the problem. This paper also develops the theory that shows that the proposed approach is complete, a fact that mitigates the incompleteness inherent in past time-window based debugging methods. Experimental results on industrial designs with long error traces show a 55% decrease in peak memory usage resulting in 78% more instances being solved when compared to previous work.

With the growing complexity of VLSI designs, functional debugging has become a bottleneck in modern CAD flows. To alleviate this cost, various SAT-based techniques have been developed to automate bug localization in the RTL. In this context, dominance relationships between circuit blocks have been recently shown to reduce the number of SAT solver calls, using the concept of solution implications. This paper first introduces the dual concepts of reverse domination and non-solution implications. A SAT solver is tailored to leverage reverse dominators for the early on-the-fly detection of bug-free components. These are non-solution areas and their early pruning significantly reduces the the debugging search-space. This process is expedited by branching on error-select variables first. Extensive experiments on tough real-life industrial debugging cases show an average speedup of 1.7x in SAT solving time over the state-of-the-art, a testimony of the practicality and effectiveness of the proposed approach.

We propose new hardware and software techniques for FPGA functional debug that leverage the inherent reconfigurability of the FPGA fabric to reduce functional debugging time. The functionality of an FPGA circuit is represented by a programming bitstream that specifies the configuration of the FPGA's internal logic and routing. The proposed methodology allows different sets of design internal signals to be traced solely by changes to the programming bitstream followed by device reconfiguration and hardware execution. Evidently, the advantage of this new methodology vs. existing debug techniques is that it operates without the need of iterative executions of the computationally-intensive design re-synthesis, placement and routing tools. In essence, with a single execution of the synthesis flow, the new approach permits a large number of internal signals to be traced for an arbitrary number of clock cycles using a limited number of external pins. Experimental results using commercial FPGA vendor tools demonstrate productivity (i.e. run-time) improvements of up to 30× vs. a conventional approach to FPGA functional debugging. These results demonstrate the practicality and effectiveness of the proposed approach.

Current silicon test methods are highly effective at sensitizing and propagating most electrical faults. Unfortunately, with ever increasing chip complexity and shorter time-to-market windows, an increasing number of faults escape undetected. To address this problem, we propose a novel technique to help identify hard-to-find electrical faults that are not detected using conventional test methods, but manifest themselves as observable functional errors during functional test, system test, or during actual use in the field. These faults are too sequentially deep to be diagnosed using simulation, ATPG, or formal tools. Our technique relies on repeated full-speed chip runs that witness the functional bug, combined with some additional on-chip functional debug support and off-line analysis, to compute a possible set of suspected faults. The technique quickly prunes the suspect set, and for each suspect, it can provide a short test vector for further analysis. Experiments on the ITC'99 benchmarks demonstrate the effectiveness of our approach.

With lower supply voltages, increased integration densities and higher operating frequencies, power grid verification has become a crucial step in the very large-scale integration design cycle. The accurate estimation of maximum instantaneous power dissipation aims at finding the worst-case scenario where excessive simultaneous switching could impose extreme current demands on the power grid. This problem is highly input-pattern dependent and is proven to be NP-hard. In this paper, we capitalize on the compelling advancements in satisfiability (SAT) solvers to propose a pseudo-Boolean SAT-based framework that reports the input patterns maximizing circuit activity, and consequently peak dynamic power, in combinational and sequential circuits. The proposed framework is enhanced to handle unit gate delays and output glitches. In order to disallow unrealistic input transitions, we show how to integrate input constraints in the formulation. Finally, a number of optimization techniques, such as the use of gate switching equivalence classes, are described to improve the scalability of the proposed method. An extensive suite of experiments on ISCAS85 and ISCAS89 circuits confirms the robustness of the approach compared to simulation-based techniques and encourages further research for low-power solutions using Boolean SAT.

With the growing size of modern designs and more strict time-to-market constraints, design errors can unavoidably escape pre-silicon verification and reside in silicon prototypes. Due to those errors and faults in the fabrication process, silicon debug has become a necessary step in the digital integrated circuit design flow. Embedded hardware blocks, such as scan chains and trace buffers, provide a means to acquire data of internal signals in real time for debugging. However, the amount of the data is limited compared to pre-silicon debugging. This paper presents an automated software solution to analyze this sparse data to detect suspects of the failure in both the spatial and temporal domain. It also introduces a technique to automate the configuration process for trace-buffer-based hardware in order to acquire helpful information for debugging the failure. The technique takes the hardware constraints into account and identifies alternatives for signals not part of the traceable set so that their values can be restored by implications. The experiments demonstrate the effectiveness of the proposed software solution in terms of run-time and resolution.

Design debugging is becoming an increasingly difficult task in the VLSI design flow with the growing size of modern designs and their error traces. In this work, a novel abstraction and refinement technique for design debugging is presented that addresses two key components of the debugging complexity, the design size and the error trace length. The abstraction technique works by under-approximating the debugging problem by removing modules of the original design and replacing them with simulated values of the erroneous circuit. After each abstract problem is solved, the refinement strategy uses the resulting UNSAT core to direct which modules should be refined. This refinement strategy is extended by allowing refinement of across time-frames in addition to modules. Experimental results show that the proposed algorithm is able to return solutions for all instances compared to only 41% without the technique demonstrating the viability of this approach in tackling real-world debugging problems.

Computer-aided design tools are continuously improving their scalability and efficiency to mitigate the high cost associated with designing and fabricating modern VLSI systems. A key step in the design process is the root-cause analysis of detected errors. Debugging may take months to close, introduce high cost and uncertainty ultimately jeopardizing the chip release date. This study makes the case for debug automation in each part of the design flow (RTL to silicon) to bridge the gap. Contemporary research, challenges and future directions motivate for the urgent need in automation to relieve the pain from this highly manual task.

In the last decade, functional verification has become a major bottleneck in the design flow. To relieve this growing burden, assertion-based verification has gained popularity as a means to increase the quality and efficiency of verification. Although robust, the adoption of assertion-based verification poses new challenges to debugging due to presence of errors in the assertions. These unique challenges necessitate a departure from past automated circuit debugging techniques which are shown to be ineffective. In this work, we present a methodology, mutation model and additional techniques to debug errors in SystemVerilog assertions. The methodology uses the failing assertion, counterexample and mutation model to produce alternative properties that are verified against the design. These properties serve as a basis for possible corrections. They also provide insight into the design behavior and the failing assertion. Experimental results show that this process is effective in finding high quality alternative assertions for all empirical instances.

Design debugging has become a resource-intensive bottleneck in modern VLSI CAD flows, consuming as much as 60% of the total verification effort. With typical design sizes exceeding the half-million synthesized gates mark, the growing number of blocks to be examined dramatically slows down the debugging process. The aim of this work is to prune the number of debugging iterations for finding all potential bugs, without affecting the debugging resolution. This is achieved by using structural dominance relationships between circuit components. More specifically, an iterative fixpoint algorithm is presented for finding dominance relationships between multiple-output blocks of the design. These relationships are then leveraged for the early discovery of potential bugs, along with their corrections, resulting in significant debugging speed-ups. Extensive experiments on real industrial designs show that 66% of solutions are discovered early due to dominator implications. This results in consistent performance gains in all cases and a 1.7× overall speed-up for finding all potential bugs, demonstrating the robustness and practicality of the proposed approach.

During the very large scale integration design process, a synthesized design is often required to be modified in order to accommodate different goals. To preserve the engineering effort already invested, designers seek small logic structural transformations to achieve these logic restructuring goals. This paper proposes a systematic methodology to devise such transformations automatically. It first presents a simulation-based formulation to approximate sets of pairs of functions to be distinguished and avoid the memory/time explosion issue inherent with the original representation. Then, it uses this new data structure to devise the required transformations dynamically without the need of a static dictionary model. The methodology is applied to both combinational and sequential designs with transformations at a single or multiple locations. An extensive suite of experiments documents the benefits of the proposed methodology when compared to existing practices.

Register renaming is a performance-critical component of modern, dynamically-scheduled processors. Register renaming latency increases as a function of several architectural parameters (e.g., processor issue width, processor window size, and processor checkpoint count). Pipelining of the register renaming logic can help avoid restricting the processor clock frequency. This work presents a full-custom, two-stage register renaming implementation in a 130-nm fabrication technology. The latency of non-pipelined and two-stage, pipelined renaming is compared, and the underlying performance and complexity tradeoffs are discussed. The two-stage pipelined design reduces the renaming logic depth from 23 fan-out-of-four (FO4) down to 9.5 FO4.

Managing long verification error traces is one of the key challenges of automated debugging engines. Today, debuggers rely on the iterative logic array to model sequential behavior which drastically limits their application. This work presents bounded model debugging, an iterative, systematic and practical methodology to allow debuggers to tackle larger problems than previously possible. Based on the empirical observation that errors are excited in temporal proximity of the observed failures, we present a framework that improves performance by up to two orders of magnitude and solve 2.7x more problems than a conventional debugger.

Many CAD for VLSI problems can be naturally encoded as Quantified Boolean Formulas (QBFs) and solved with QBF solvers. Furthermore, such problems often contain circuit-based information that is lost during the translation to Conjunctive Normal Form (CNF), the format accepted by most modern solvers. In this work, a novel preprocessing framework for circuit-based QBF problems is presented. It leverages structural circuit dominators to reduce the problem size and expedite the solving process. Our circuit-based QBF preprocessor PReDom recursively reduces dominated subcircuits to return a simpler but equisatisfiable QBF instance. A rigorous proof is given for eliminating subcircuits dominated by single outputs, irrespective of input quantifiers. Experimental results are presented for circuit diameter computation problems. With preprocessing times of at most five seconds using PReDom, three state-of-the-art QBF solvers can solve 27% to 45% of our problem instances, compared to none without preprocessing.

Formal CAD tools operate on mathematical models describing the sequential behavior of a VLSI design. With the growing size and state-space of modern digital hardware designs, the conciseness of this mathematical model is of paramount importance in extending the scalability of those tools, provided that the compression does not come at the cost of reduced performance. Quantified Boolean Formula satisfiability (QBF) is a powerful generalization of Boolean satisfiability (SAT). It also belongs to the same complexity class as many CAD problems dealing with sequential circuits, which makes it a natural candidate for encoding such problems. This work proposes a succinct QBF encoding for modeling sequential circuit behavior. The encoding is parametrized and further compression is achieved using time-frame windowing. Comprehensive hardware constructions are used to illustrate the proposed encodings. Three notable CAD problems, namely bounded model checking, design debugging and sequential test pattern generation, are encoded as QBF instances to demonstrate the robustness and practicality of the proposed approach. Extensive experiments on OpenCore circuits show memory reductions in the order of 90 percent and demonstrate competitive runtimes compared to state-of-the-art SAT techniques. Furthermore, the number of solved instances is increased by 16 percent. Admittedly, this work encourages further research in the use of QBF in CAD for VLSI.

As contemporary very large scale integration designs grow in complexity, design debugging has rapidly established itself as one of the largest bottlenecks in the design cycle today. Automated debug solutions such as those based on Boolean satisfiability (SAT) enable engineers to reduce the debug effort by localizing possible error sources in the design. Unfortunately, adaptation of these techniques to industrial designs is still limited by the performance and capacity of the underlying engines. This paper presents a novel formulation of the debugging problem using MaxSAT to improve the performance and applicability of automated debuggers. Our technique not only identifies errors in the design but also indicates when the bug is excited in the error trace. MaxSAT allows for a simpler formulation of the debugging problem, reducing the problem size by 80% compared to a conventional SAT-based technique. Empirical results demonstrate the effectiveness of the proposed formulation as run-time improvements of 4.5 × are observed on average. This paper introduces two performance improvements to further reduce the time required to find all error sources within the design by an order of magnitude.

Design debugging is a major bottleneck in modern very large scale integration design flows as both the design size and the length of the error trace contribute to its inherent complexity. With typical design blocks exceeding half a million synthesized logic gates and error traces in the thousands of clock cycles, the complexity of the debugging problem poses a great challenge to automated debugging techniques. This paper aims to address this daunting challenge by introducing the bounded model debugging methodology that iteratively analyzes bounded sequences of the error trace. Two techniques are introduced in this methodology to solve this growing problem. The first technique iteratively analyzes bounded subsequences of the error trace of increasing size until the error is found or the entire trace is analyzed. The second technique partitions the error trace into non-overlapping bounded sequences of clock cycles which are each separately analyzed. A discussion of these two techniques is presented and a unified methodology that leverages the strengths of both techniques is developed. Empirical results on real industrial designs show that for large designs and long error traces the proposed methodology can find the actual error in 79% of cases with the first technique and 100% of cases with the second technique. In cases where the methodology is not used only 21% of cases are able to find the actual error. These numbers confirm the benefits of the proposed methodology to allow conventional automated debuggers to handle much larger real-life circuits.

This paper investigates how the latency and energy of register alias tables (RATs) vary as a function of the number of global checkpoints (GCs), processor issue width, and window size. It improves upon previous RAT checkpointing work that ignored the actual latency and energy tradeoffs and focused solely on evaluating performance in terms of instructions per cycle (IPC). This work utilizes measurements from the full-custom checkpointed RAT implementations developed in a commercial 130-nm fabrication technology. Using physical- and architectural-level evaluations together, this paper demonstrates the tradeoffs among the aggressiveness of the RAT checkpointing, performance, and energy. This paper also shows that, as expected, focusing on IPC alone incorrectly predicts performance. The results of this study justify checkpointing techniques that use very few GCs (e.g., four). Additionally, based on full-custom implementations for the checkpointed RATs, this paper presents analytical latency and energy models. These models can be useful in the early stages of architectural exploration where actual physical implementations are unavailable or are hard to develop. For a variety of RAT organizations, our model estimations are within 6.4% and 11.6% of circuit simulation results for latency and energy, respectively. This range of accuracy is acceptable for architectural-level studies.

Semiconductor design companies are in a continuous search for design tools that address the ever increasing chip design complexity coupled with strict time-to-market schedules and budgetary constraints. A fundamental aspect of the design process that remains primitive is that of debugging. It takes months to close, it introduces costs and it may jeopardize the release date of the chip. This paper reviews the debugging problem and the research behind it over the past 20 years. The case for automated RTL debug tools and methodologies is also made to help ease the manual burden and complement current industrial verification practices.

Since pre-silicon functional verification is insufficient to detect all design errors, re-spins are often needed due to malfunctions that escape into the silicon. This paper presents an automated software solution to analyze the data collected during silicon debug. The proposed methodology analyzes the test sequences to detect suspects in both the spatial and the temporal domain. A set of software debug techniques are proposed to analyze the acquired data from the hardware testing and provide suggestions for the setup of the test environment in the next debug session. A comprehensive set of experiments demonstrate its effectiveness in terms of run-time and resolution.

In the digital VLSI cycle, logic transformations are often required to modify the design to meet different synthesis and optimization goals. Logic transformations on sequential circuits are hard to perform due to the vast underlying solution space. This paper proposes an SPFD-based sequential logic transformation methodology to tackle the problem with no sacrifice on performance. It first presents an efficient approach to construct approximate SPFDs (aSPFDs) for sequential circuits. Then, it demonstrates an algorithm using aSPFDs to perform the desirable sequential logic transformations using both combinational and sequential don't cares. Experimental results show the effectiveness and robustness of the approach.

Given an erroneous design, functional verification returns an error trace exhibiting a mismatch between the specification and the implementation of a design. Automated design debugging uses these error traces to identify potentially erroneous modules causing the error. With the increasing size and complexity of modern VLSI designs, error traces have become longer and harder to analyze. At the same time, design debugging has become one of the most resource-intensive steps in the chip design cycle. This work proposes a scalable SAT-based design debugging algorithm that uses interpolants to over-approximate sets of constraints that model the erroneous behavior. The algorithm partitions the original problem into a sequence of smaller subproblems by using subsections of the error trace that are examined iteratively. This is made possible by using interpolants to properly constrain the erroneous behavior for each subproblem, significantly reducing the number of simultaneous time-frames examined in the error trace. The described method is shown to be complete and an additional technique is presented to improve the quality of the debugging results using multiple interpolants. Experiments on real designs show a 57% reduction in memory and 23% decrease in run-time compared to previous work.

Design debug remains one of the major bottlenecks in the VLSI design cycle today. Existing automated solutions strive to aid engineers in reducing the debug effort by identifying possible error sources in the design. Unfortunately, these techniques do not provide any information regarding the time at which the bug is active during an error trace or counter-example. This work introduces an automated debug technique that provides the user with both spatial and temporal information about the source of error. The proposed method is based on a Partial MaxSAT formulation which models errors at the CNF clause level instead of the traditional gate or module level. Thus, error sites are identified based on erroneous implications that correspond to locations both in the design and in the error trace. Experiments demonstrate that we can provide this additional information at no extra cost in run time and are able to prune about 61% of all simulation time frames from the debugging process. When compared to a trivial formulation we observe a performance improvement of up to two orders of magnitude and 5× on average when using the proposed formulation.

Design debugging is one of the major remaining manual processes in the semiconductor design cycle. Despite recent advances in the area of automated design debugging, more effort is required to cope with the size and complexity of today's designs. This paper introduces an abstraction and refinement methodology to enable current debuggers to operate on designs that are orders of magnitude larger than otherwise possible. Two abstraction techniques are developed with the goals of improving debugger performance for different circuit structures: State abstraction is aimed at reducing the problem size for circuits consisting purely of primitive gates, while function abstraction focuses on designs that also contain modular and hierarchical information. In both methods, after an initial abstracted model is created, the problem can be solved by an existing automated debugger. If an error site is abstracted, refinement is necessary to reintroduce some of the abstracted components back into the design. This paper also presents the underlying theory to guarantee correctness and completeness of a debugging tool that operates using the proposed methodology. Empirical results demonstrate improvements in run time and memory capacity of two orders of magnitude over a state-of-the-art debugger on a wide range of benchmark and industrial designs.

In todaypsilas complex SoC designs, verification and debugging are becoming ever more crucial and increasingly time-consuming tasks. The prevalence of embedded memories adds to the difficulty of the problem by exponentially increasing the state-space of the design. In this work, a novel memory model for design debugging is presented. It models memory succinctly by avoiding an explicit representation for each memory bit. The method uses the simulation of the erroneous design to guide the debugging process. This results in a parameterizable formal encoding that grows linearly with the erroneous trace length, significantly reducing the memory requirements of the debugging problem. In addition, the proposed model is extended to handle an arbitrary initial memory configuration, as well as non-cycle accurate output traces where only a final expected memory state is available for comparison. Experiments on industrial designs show a 96% average reduction in memory usage along with a noticeable performance improvement compared to previous work.

Sets of Pairs of Functions to be Distinguished (SPFD) is a functional flexibility representation method that was recently introduced in the logic synthesis domain, and promises superiority in exploring the flexibility offered by a design over all previous representation methods. In this work, we illustrate how the SPFD of a particular wire reveals information regarding the number of potential transient errors that may occur on that wire and may affect the output of the circuit. Using an SPFD-based rewiring method, we then demonstrate how to evolve a logic circuit in order to minimize the total number of potential transient errors in the circuit and, consequently, reduce its Soft Error Rate (SER) while controlling the effect on the rest of the design parameters, such as area, power, delay, and testability. Experimental results on ISCAS'89 and ITC'99 benchmark circuits indicate that the SER can be reduced at no additional overhead to any of the design parameters.

Using full-custom layouts in 130 nm technology, this work studies how the latency and energy of a checkpointed, CAM-based Register Alias Table (cRAT) vary as a function of the window size, the issue width, and the number of embedded global checkpoints (GCs). These results are compared to those of the SRAM-based RAT (sRAT). Understanding these variations is useful during the early stages of architectural exploration where physical level information is not yet available. It is found that compared to sRAT, cRAT is more sensitive to the number of physical registers and issue width, however, it is less sensitive to the number of GCs. In addition, beyond a certain number of GCs, cRAT becomes faster than its equivalent sRAT. For instance, this is true when a RAT for 64 architectural and 128 physical registers has at least 20 GCs. This work also proposes an energy optimization for the cRAT; this optimization selectively disables cRAT entries that do not result in a match during lookup. The energy savings are, for the most part, a function of the number of physical registers. For instance, for a cRAT with 128 entries energy is reduced by 40%.

An increasing number of architectural techniques have relied on hardware counting bloom filters (CBFs) to improve upon the energy, delay, and complexity of various processor structures. CBFs improve the energy and speed of membership tests by maintaining an imprecise and compact representation of a large set to be searched. This paper studies the energy, delay, and area characteristics of two implementations for CBFs using full custom layouts in a commercial 0.13-mum fabrication technology. One implementation, S-CBF, uses an SRAM array of counts and a shared up/down counter. Our proposed implementation, L-CBF, utilizes an array of up/down linear feedback shift registers and local zero detectors. Circuit simulations show that for a 1 K-entry CBF with a 15-bit count per entry, L-CBF compared to S-CBF is 3.7times or 1.6times faster and requires 2.3times or 1.4times less energy depending on the operation. Additionally, this paper presents analytical energy and delay models for L-CBF. These models can estimate energy and delay of various CBF organizations during architectural level explorations when a physical level implementation is not available. Our results demonstrate that for a variety of L-CBF organizations, the estimations by analytical models are within 5% and 10% of Spectre simulation results for delay and energy, respectively.

In today's designs, when functional verification fails, engineers perform debugging using the provided error traces. Reducing the length of error traces can help the debugging task by decreasing the number of variables and clock cycles that must be considered. We propose a novel trace length compaction approach based on SAT-based reachability analysis. We develop procedures and algorithms using pre-image computation to efficiently traverse the state space and reduce the trace lengths. We further introduce a data structure used to store the visited states which is critical to the performance of the proposed approach. Experiments demonstrate the effectiveness of the reachability approach as approximately 75% of the traces are reduced by one or two orders of magnitudes.

In the digital VLSI cycle, a netlist is often modified to correct design errors, perform small specification changes or implement incremental rewiring-based optimization operations. Most existing automated logic rectification tools use a small set of predefined logic transformations when they perform such modifications. This paper first shows that a small set of predefined transformations may not allow rectification to exploit the full potential of the design. Then, it proposes an automated simulation-based methodology to "approximate" sets of pairs of functions to be distinguished (SPFDs) and avoid the memory/time explosion problem. This representation is used by a SAT-based algorithm that devises appropriate logic transformations to fix a design. The SAT method is later complemented by a greedy one that improves on runtime performance. An extensive suite of experiments documents the added potential of the proposed rectification methodology.

In today's SoC design cycles, debugging is one of the most time consuming manual tasks. CAD solutions strive to reduce the inefficiency of debugging by identifying error sources in designs automatically. Unfortunately, the capacity and performance of such automated techniques must be considerably extended for industrial applicability. This work aims to improve the performance of current state-of-the-art debugging techniques, thus making them more practical. More specifically, this work proposes a novel design debugging formulation based on maximum satisfiability (max-sat) and approximate max-sat. The developed technique can quickly discard many potential error sources in designs, thus drastically reducing the size of the problem passed to an existing debugger. The max-sat formulation is used as a pre-processing step to construct a highly optimized debugging framework. Empirical results demonstrate the effectiveness of the proposed framework as run-time improvements of orders of magnitude are consistently realized over a state-of-the-art debugger.

Many CAD for VLSI techniques use time-frame expansion, also known as the Iterative Logic Array representation, to model the sequential behavior of a system. Replicating industrial- size designs for many time-frames may impose impractically ex- cessive memory requirements. This work proposes a performance- driven, succinct and parametrizable Quantified Boolean Formula (QBF) satisfiability encoding and its hardware implementation for modeling sequential circuit behavior. This encoding is then applied to three notable CAD problems, namely Bounded Model Checking (BMC), sequential test generation and design debugging. Extensive experiments on industrial circuits confirm outstanding run-time and memory gains compared to state-of-the-art techniques, pro- moting the use of QBF in CAD for VLSI.

We present two full-custom implementations of the Register Alias Table (RAT) for a 4-way superscalar dynamically-scheduled processor in a commercial 130nm CMOS technology. The implementations differ in the way they organize the embedded global checkpoints (GCs) which support speculative execution. In the first implementation, representative of early designs, the GCs are organized as shift registers. In the second implementation, representative of more recent proposals, the GCs are organized as random access buffers. We measure the impact of increasing thenumber of GCs on the latency, energy, and area of the RAT. The results support the importance of recent techniques that reduce the number of GCs while maintaining performance.

Most FPGA technology mapping approaches either target Lookup Tables (LUTs) or relatively simple Programmable Logic Blocks (PLBs). Considering networks of PLBs during technology mapping has the potential of providing unique optimizations unavailable through other techniques. This paper proposes a Boolean matching approach for FPGA technology mapping targeting networks of PLBs. To overcome the demanding memory requirements of previous approaches, the Boolean matching problem is formulated as a Boolean Satisfiability (SAT) problem. Since the SAT formulation provides a trade-off between space and time, the primary objective is to increase the efficiency of the SAT-based approach. To do this, the original SAT problem is decomposed into two easier SAT problems. To reduce the problem search space, a theorem is introduced to allow conflict clauses to be shared across problems and extra constraints are generated. Experiments demonstrate a 340% run time improvement and 27% more success in mapping than previous SAT-based approaches.

The problem of diagnosis - or locating the source of an error or fault $occurs in several areas of computer aided design, such as dynamic verification, property checking, equivalence checking and production test. Manually locating errors can be a time consuming and resource-intensive process. Several automated approaches for diagnosis have been presented, among them are simulation-based and SAT-based techniques. These two approaches are found to be robust even for large circuits as well as being applicable to a broad range of diagnosis problems. An in-depth comparison of both approaches necessary to augment our knowledge of diagnosis procedures has not been addressed by previous work. This paper provides a thorough analysis of the similarities and differences between simulation-based and SAT-based procedures for diagnosis. The relation between the basic approaches is theoretically analyzed. Issues regarding performance and diagnosis quality (resolution) are discussed. Experimental data strengthens the theoretical results. This detailed understanding of the relations between the techniques is necessary to provide further improvements to the field of diagnosis. The initial steps towards building a hybrid technique are also presented

All-solution Boolean satisfiability (SAT) solvers are engines employed to find all the possible solutions to a SAT problem. Their applications are found throughout the EDA industry in fields such as formal verification, circuit synthesis and automatic test pattern generation. Typically, these engines iteratively find each solution by calling a standard SAT solving procedure. Each solution is minimized using different post processing techniques and the problem is constrained to prevent recurring solutions. In this work, instead of applying post processing techniques, the objective is to minimize the size of the solution "on the fly" during the all-solution SAT solving process. This is achieved by allowing the solver to exploit the structural circuit observability don't cares (ODC) arising from the problem. The solver makes decisions such that the number of ODCs is maximized in each solution thus leading to an overall smaller number of iterations. Through extensive experiments, it is demonstrated that integrating ODC techniques within an all-solution SAT solver results in increased performance and more compact solutions

We study the energy, latency and area characteristics of two Counting Bloom Filter implementations using full custom layouts in a commercial 0.13μm technology. The first implementation, S-CBF, uses an SRAM array of counts and a shared counter. The second, L-CBF, utilizes an array of up/down linear feedback shift registers. Circuit level simulations demonstrate that for a 1K-entry CBF with a 15-bit count per entry, L-CBF is 3.7 or 1.6 times faster than the S-CBF depending on the operation. The L-CBF requires 2.3 or 1.4 times less energy per operation compared to the S-CBF. However, the L-CBF requires 3.2 times more area. We demonstrate that for one application of CBFs (early hit/miss detection for L1 caches [12] for an aggressive dynamically-scheduled superscalar processor) the energy consumed by the L-CBF is 60% of the energy consumed by the S-CBF for most of the SPEC CPU 2000 benchmarks.

Rewiring has been used extensively for optimizing the area, the power consumption, the delay, and the testability of a circuit. In this work, we demonstrate how rewiring can also be used for reducing the soft error rate (SER). We employ an ATPG-based rewiring method to generate functionally-equivalent yet structurally-different implementations of a logic circuit based on simple transformation rules. This rewiring capability, along with an off-the-shelf method for assessing the SER of a circuit, enable the integration of the SER in a unified search algorithm that iteratively evolves the design in order to satisfy a given set of objectives. Experimental results on ISCAS'89 and ITC'99 benchmark circuits verify that rewiring can indeed be successfully used to reduce the SER of a circuit and, thus, it facilitates a design-space exploration framework for trading off area, power consumption, delay, testability, and SER

The aim of the TTTC Doctoral Thesis Award is to promote and strengthen the interaction between doctoral students who are about to graduate and the industrial community. It also serves as a process that allows their work to be exposed to and tested under real life industrial needs by experts in the field. This is achieved with student presentations in a dedicated VTS session in front of an industrial panel that evaluates, comments and contributes to their work in terms of novelty and advance of industrial practice and this of theoretical methodology.

In the design cycle of high-performance integrated circuits, it is common that certain components are designed directly at the transistor level. This level of design representation may not be appropriate for test generation tools that usually require a model expressed at the gate level. Logic extraction is a key step in test model generation to produce a gate-level netlist from the transistor-level representation. This is a semi-automated process which is error-prone. Once a test model is found to be erroneous, manual debugging is required, which is a resource-intensive and time-consuming process. This paper presents an in-depth analysis of typical sets of extraction errors found in the test model representations of the pipelines in high-performance designs today. It also develops an automated debugging solution for single extraction errors for pipelines with no state equivalence information. A suite of experiments on circuits with similar architecture to that found in the industry confirms the fitness and practicality of the solution.

Test model generation is common in the design cycle of custom made high performance low power designs targeted for high volume production. Logic extraction is a key step in test model generation to produce a logic level netlist from the transistor level representation. This is a semi-automated process which is error prone. The paper analyzes typical extraction errors applicable to clocking schemes seen in high-performance designs today. An automated debugging solution for these errors in designs with no state equivalence information is also presented. A suite of experiments on circuits with similar architectures to those found in the industry confirm the fitness and practicality of the solution.

As timing requirements in today's advanced VLSI designs become more aggressive, the need for automated tools to diagnose timing failures increases. This work presents two such algorithms capable of diagnosing multiple delay faults. One method uses multiple transition fault models and the other reasons with ternary logic values, thus achieving model independent diagnosis. Experiments are conducted on IS-CAS'85 combinational and full-scan version of ISCAS'89 se-quential circuits corrupted with multiple transition faults. The performance of both algorithms are evaluated and compared. The results show good efficiency and diagnostic resolution.

Boolean Satisfiability (SAT) solvers are popular engines used throughout the verification world. Bounded sequential problems such as bounded model checking and bounded sequential equivalence checking rely on fast and robust SAT solvers. In this work, we introduce a technique that improves the performance of the underlying SAT solver for bounded sequential problems by taking advantage of a design's don't care states. We develop cost effective methods of filtering, replicating and applying the don't care states to the original problem thus reducing the search space. Experiments demonstrate the effectiveness of the proposed method on ISCAS'89 benchmarks.

As VLSI designs grow in complexity and size, errors become more frequent and difficult to track. Recent developments have automated most of the verification tasks but debugging still remains a resource-intensive, manually conducted procedure. This paper bridges this gap as it develops robust automated debugging methodologies that complement verification processes. Unlike prior debugging techniques, the proposed one exploits the hierarchical nature of modern designs to improve the performance and quality of debugging. It also formulates the problem in terms of Quantified Boolean Formula Satisfiability to obtain dramatic reduction in memory requirements, which allows for debugging of large designs. Extensive experiments conducted on industrial and benchmark designs confirm the efficiency and practicality of the proposed approach.

Fault diagnosis is important in improving the circuit-design process and the manufacturing yield. Diagnosis of today's complex defects is a challenging problem due to the explosion of the underlying solution space with the increasing number of fault locations and fault models. To tackle this complexity, an incremental diagnosis method is proposed. This method captures faulty lines one at a time using the novel linear-time single-fault diagnosis algorithms. To capture complex fault effects, a model-free incremental diagnosis algorithm is outlined, which alleviates the need for an explicit fault model. To demonstrate the applicability of the proposed method, experiments on multiple stuck-at faults, open-interconnects and bridging faults are performed. Extensive results on combinational and full-scan sequential benchmark circuits confirm its resolution and performance.

Recent advances in Boolean satisfiability have made it an attractive engine for solving many digital very-large-scale-integration design problems. Although useful in many stages of the design cycle, fault diagnosis and logic debugging have not been addressed within a satisfiability-based framework. This work proposes a novel Boolean satisfiability-based method for multiple-fault diagnosis and multiple-design-error diagnosis in combinational and sequential circuits. A number of heuristics are presented that keep the method memory and run-time efficient. An extensive suite of experiments on large circuits corrupted with different types of faults and errors confirm its robustness and practicality. They also suggest that satisfiability captures significant characteristics of the problem of diagnosis and encourage novel research in satisfiability-based diagnosis as a complementary process to design verification.

Advances in Boolean satisfiability solvers have popularized their use in many of today's CAD VLSI challenges. Existing satisfiability solvers operate on a circuit representation that does not capture all of the structural circuit characteristics and properties. This work proposes algorithms that take into account the circuit don't care conditions thus enhancing the performance of these tools. Don't care sets are addressed in this work both statically and dynamically to reduce the search space and guide the decision making process. Experiments demonstrate performance gains.

Logic debugging of today's complex sequential circuits is an important problem. In this paper, a logic debugging methodology for multiple errors in sequential circuits with no state equivalence is developed. The proposed approach reduces the problem of debugging to an instance of Boolean satisfiability. This formulation takes advantage of modern Boolean satisfiability solvers that handle large circuits in a computationally efficient manner. An extensive suite of experiments with large sequential circuits confirm the robustness and efficiency of the proposed approach. The results further suggest that Boolean satisfiability provides an effective platform for sequential logic debugging.

We present a formal logic verification methodology for combinational circuits. The method uses simulation, logic diagnosis and ATPG to identify circuit lines that implement equivalent logic functions efficiently. One advantage of the proposed technique is that it identifies line equivalences under controllability and observability don't care conditions, while not suffering from false negatives. The method is easy to implement, and, due to its general nature, existing techniques can benefit from ideas described here. We also give implementation details and present experiments to confirm its potential.

Test model generation is crucial in the test generation process of a high-performance design targeted for large volume production. A key process in test model generation requires the extraction of a gate-level (logic) model from the transistor level representation of the circuit under test. Logic extraction is an error prone process due to extraction tool limitations and due to the human interference. Errors introduced by extraction require manual debugging, a resource intensive and time consuming task. This paper presents a set of extraction errors typical in an industrial environment. It also proposes an automated solution to extraction error diagnosis and correction. Experiments on circuits with similar architecture to that of high speed custom-made industrial blocks are conducted to confirm the fitness of the approach. 1

An incremental simulation-based approach to fault diagnosis and logic debugging is presented. During each iteration of the algorithm, a single suspicious location is identified and fault modeled such that the functionality of the new design becomes "closer" to its specification. The method is based on a simple and, at a first glance, counter-intuitive theoretical result along with a number of heuristics which help avoid the exponential complexity inherent to the problems. Experiments on multiple design errors and multiple stuck-at faults confirm its effectiveness and accuracy, which scales well with increasing number of errors.

With increasing chip interconnect distances, open-interconnect is becoming an important defect. The main challenge with open-interconnects stems from its non-deterministic real-life behavior In this work, we present an efficient diagnostic technique for multiple open-interconnects. The algorithm proceeds in two phases. During the first phase, potential solution sets are identified following a model-free incremental diagnosis methodology. Heuristics are devised to speed up this step and screen the solution space efficiently. In the second phase, a generalized fault simulation scheme enumerates all possible faulty behaviors for each solution from the first phase. We conduct experiments on combinational and full-scan sequential circuits with one, two and three open faults. The results are very encouraging.

Technology dependent logic optimization is usually carried through a sequence of design rewiring operations. In Veneris et al (Proc. Asian-South-Pacific Design Automation Conf., pp. 479-484, 2001), a new design rewiring method is proposed that combines error diagnosis and correction techniques with ATPG. In this work, we examine its complexity and we arrive to a new set of results with interesting theoretical and practical applications. We also present experiments that confirm the competitiveness of the approach and motivate future work in the field.

Logic optimization is the step of the very large scale integration (VLSI) design cycle where the designer performs modifications on a design to satisfy different constraints such as area, power, or delay. Recently, automated test pattern generation (ATPG)-based design rewiring techniques for technology-dependent logic optimization have gained increasing popularity. In this paper, the authors propose a new operational framework to design rewiring that uses ATPG and diagnosis algorithms. They also examine its complexity requirements and discuss different implementation tradeoffs. To perform this study, the authors reduce the problem of design rewiring to the process of injecting a redundant set of multiple pattern faults. This formulation arrives at a new set of results with theoretical and practical applications. Experiments demonstrate the competitiveness of the approach and motivate future work in the area.

Logic optimization is the step of the VLSI design cycle where the designer performs modifications on a design to satisfy di#erent constraints such as area, power or delay. Recently, ATPG-based design rewiring techniques for logic optimization have gained increasing popularity. In this paper we propose a novel ATPG-based design rewiring methodology that borrows from previous design error diagnosis and correction techniques. We also present examples and experiments that indicate the added potential of our approach which is expected to provide a "powerful" route to design optimization. 1 Introduction Logic optimization is the step of the VLSI design cycle where the designer modifies the netlist obtained by synthesis tools to achieve di#erent constraints such as minimize the area, reduce power consumption, satisfy timing constraints, reduce switching noise or improve the testability of the final circuit. Recently, ATPG-based optimization techniques [6] [7] [8] [9] [10] [12] have gained i...

With the increase in the complexity of VLSI circuit design, logic design errors can occur during synthesis. In this work, we present a method for multiple design error diagnosis and correction. Our approach uses the results of test vector simulation for both error detection and error correction. This makes it applicable to circuits with no global BDD representation. In addition, diagnosis is performed through an implicit enumeration of potentially erroneous lines in an effort to avoid the exponential explosion of the error space. Experimental results on ISCAS'85 benchmark circuits show that our approach can typically detect and correct 1, 2 and 3 errors within seconds of CPU time.

With the increase in the complexity of digital VLSI circuit design, logic design errors can occur during synthesis. In this paper, we present a test vector simulation-based approach for multiple design error diagnosis and correction. Diagnosis is performed through an implicit enumeration of the erroneous lines in an effort to avoid the exponential explosion of the error space as the number of errors increases. Resynthesis during correction is as little as possible so that most of the engineering effort invested in the design is preserved. Since both steps are based on test vector simulation, the proposed approach is applicable to circuits with no global binary decision diagram representation. Experiments on ISCAS'85 benchmark circuits exhibit the robustness and error resolution of the proposed methodology. Experiments also indicate that test vector simulation is indeed an attractive technique for multiple design error diagnosis and correction in digital VLSI circuits.

With the increase in the complexity of VLSI circuit design and the corresponding increase in the number of logic gates on a chip, logic design errors can frequently occur. In this paper we present an efficient approach to Design Error Detection and Correction when a small number of modifications can rectify the design. Our method is based on test vector simulation and Boolean function manipulation techniques. The proposed approach guarantees to return a solution, if such a solution exists in our modification model, in a short computational time. Experimental results show the robustness of our approach.