Hardware information flow tracking (IFT) using taint analysis provides a methodology to check whether a hardware design satisfies certain security properties. Previous work has shown a broad trade-off space between precision and complexity when using different taint analysis schemes. A careful investigation of this space has led to the insight that applying different taint schemes to different components of a hardware design can improve overall efficiency.

Recent years have seen significant advances in using formal verification to check hardware security properties. Of particular practical interest are checking confidentiality and integrity of secrets, by checking that there is no information flow between the secrets and observable outputs. A standard method for checking information flow is to translate the corresponding non-interference hyperproperty into a safety property on a self-composition of the design, which has two copies of the design composed together. Although prior efforts have aimed to reduce the size of the self-composed design, there are no state-of-the-art model checkers that exploit their special structure for hardware security verification. In this paper, we propose SecIC3, a hardware model checking algorithm based on IC3 that is customized to exploit this self-composition structure. SecIC3 utilizes this structure in two complementary techniques: symmetric state exploration and adding equivalence predicates. We implement SecIC3 on top of two open-source IC3 implementations and evaluate it on a non-interference checking benchmark consisting of 10 designs. The experiment results show that SecIC3 significantly reduces the time for finding security proofs, with up to 49.3x proof speedup compared to baseline implementations.

Reasoning about the correctness of distributed systems is a significant challenge, with precise correctness specifications serving as an essential prerequisite to verification. However, identifying and formulating specifications remains a major hurdle for developers in practice. Specy addresses this challenge by automatically learning specifications from observable event traces generated by message exchanges in distributed systems. The system employs a specialized grammar tailored for event-based specifications, incorporating support for quantifiers over events - a capability essential for capturing the complex behavioral patterns inherent in distributed protocols. Specy utilizes a novel learning procedure that combines grammar-based enumerative search with dynamic learning from event traces, providing effective control over the specification search. We evaluated Specy on established distributed protocols and industrial case studies, demonstrating its ability to successfully learn important protocol specifications. Specy can discover previously unidentified specifications overlooked by developers, automatically derive inductive invariants that were previously constructed manually for verification purposes, and, through run-time monitoring in production systems, reveal gaps in testing coverage - highlighting opportunities to leverage specifications in practice.

Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus, a formal and rigorous evaluation of the ability of hardware designs to deal with speculative execution attacks is urgently desired.

Scaling hardware formal verification (FV) has been an ongoing challenge due to the state space explosion problem. In this article, we introduce a bottom-up verification methodology that leverages design hierarchy by using sound abstractions at each level in the hierarchy to decompose the overall FV problem into a set of smaller, more manageable FV tasks.We use the recently proposed instruction-level abstraction (ILA) as a complete specification at each level of the design hierarchy. We then utilize ILA-based verification methods to check correctness of modules composed at that level. The ILA specification includes an interface specification for each module and interface checks for verifying correct intermodule communication. This approach enables compositional verification with the following guarantee: if each hardware component refines its ILA specification and passes the interface checks, then the register-transfer level composition refines the ILA composition. We then show how this compositional verification methodology facilitates a bottom-up hierarchical verification approach, where the specification at one level serves as the implementation at the next higher level. We demonstrate the increased scalability of our methodology through several case studies, including complex modules in two deep learning accelerators (FlexASR and NVDLA), where verification fails to complete on the flat designs.

Specialized hardware accelerators are increasingly utilized to provide performance/power efficiency for Deep Neural Network (DNN) applications. However their benefits are limited by expensive off-chip data movement between host memory and the accelerator’s on-chip scratchpad, which can consume significantly more energy than accelerator computation [13]. While application-level DNN operators can have arbitrary sizes, accelerators typically support fixed-sized operations due to constrained on-chip memory and micro-architectures. Consequently, mapping an application-level operator to an accelerator involves decomposing it into loops of smaller tiles. Different choices of tile sizes, loop orders and memory partition across tensors result in a vast design space with huge differences in off-chip data movement volume. To address this challenge, we introduce Shoehorn, a schedule optimization framework that jointly optimizes loop tiling, loop ordering, and memory partitioning for mapping application-level DNN operators to hardware accelerators. Shoehorn can generate optimal schedules in subseconds and outperforms state-of-the-art approaches, reducing up to 51% total off-chip memory traffic relative to competing schedulers for several widely-used DNN applications on three distinct hardware accelerator targets.

Today's low-power designs switch between active and standby modes depending on their activity. While the design is in standby mode, its power supply can be turned off to prevent static power consumption. Retention registers are used in these low-power designs to maintain design state even when power is turned off. However, replacing all normal registers with retention registers results in significant area and power overhead. As a consequence, designers often go through the tedious and error-prone process of identifying a partial set of retention registers required to maintain correct design functionality. Further, checking for the correctness of this partial retention set is limited to simulation-based validation. In this paper, we develop model-checking based techniques to formally verify the correctness of a partial retention set for a low-power design. Further, we propose automatic algorithms to help designers identify compact partial retention sets. These algorithms can leverage designers' knowledge to reduce the overall search space and improve scalability. Experiments on open-source designs demonstrate the efficiency and effectiveness of the proposed algorithms. We also show how utilizing design knowledge can help scale our method up to handling designs with about 400K flip-flops.

Simulation is widely used during different stages of hardware development. This paper focuses on one specific type of simulation - cycle-accurate timing simulation, which measures the number of cycles for a given computation. We propose a pioneering approach for automatically generating cycle-accurate timing models of hardware accelerators from their RTL designs based on dependency analysis and constraint solving, making this the first technique of its kind in this domain. We demonstrate the applicability of our approach for six non-trivial designs. We show that our method achieves a 1.5x-6.9x speedup for cycle-accurate simulation over RTL models for computation-intensive accelerators, demonstrating its effectiveness. Our approach provides a cost-effective way to quickly determine the execution time of accelerators.

Ideally, accelerator development should be as easy as software development. Several recent design languages/tools are working toward this goal, but actually testing early designs on real applications end-to-end remains prohibitively difficult due to the costs of building specialized compiler and simulator support. We propose a new first-in-class, mostly automated methodology termed “3LA” to enable end-to-end testing of prototype accelerator designs on unmodified source applications. A key contribution of 3LA is the use of a formal software/hardware interface that specifies an accelerator’s operations and their semantics. Specifically, we leverage the Instruction-level Abstraction (ILA) formal specification for accelerators that has been successfully used thus far for accelerator implementation verification. We show how the ILA for accelerators serves as a software/hardware interface, similar to the Instruction Set Architecture for processors, that can be used for automated development of compilers and instruction-level simulators. Another key contribution of this work is to show how ILA-based accelerator semantics enables extending recent work on equality saturation to auto-generate basic compiler support for prototype accelerators in a technique we term “flexible matching.” By combining flexible matching with simulators auto-generated from ILA specifications, our approach enables end-to-end evaluation with modest engineering effort. We detail several case studies of 3LA, which uncovered an unknown flaw in a recently published accelerator and facilitated its fix.

Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.

This paper presents the Instruction-Level Abstraction (ILA) as a formal software/hardware interface for accelerator-rich platforms. The ILA provides a common framework for formal functional specification of processors and accelerator behavior, verifying their implementations, and reasoning about software-hardware interactions of programs with accelerators. The ILA-MCM specification extends the ILA to enable reasoning about interactions of accelerators with other compute engines through shared memory. The 3LA compilation flow for accelerators uses the ILA model to bridge the gap between fine-grain compiler intrinsics and coarse-grain accelerator operations.

In modern systems-on-chips, several hardware protocols are used for communication and interaction among different modules. These protocols are complex and need to be implemented correctly for correct operation of the system-on-chip. Therefore, protocol verification has received significant attention. However, this verification is often limited to checking high-level properties on a protocol specification or an implementation. Verifying these properties directly on an implementation faces scalability challenges due to its size and design complexity. Further, even after some high-level properties are verified, there is no guarantee that an implementation fully complies with a given specification, even if the same properties have also been checked on the specification. We address these challenges and gaps by adding a layer of component specifications, one for each component in the protocol implementation, and specifying and verifying the interactions at the interfaces between each pair of communicating components. We use the recently proposed formal model termed Instruction-Level Abstraction (ILA) as a component specification, which includes an interface specification for the interactions in composing different components. The use of ILA models as component specifications allows us to decompose the complete verification task into two sub-tasks: checking that the composition of ILAs is sequentially equivalent to a verified formal protocol specification, and checking that the protocol implementation is a refinement of the ILA composition. This check requires that each component implementation is a refinement of its ILA specification and includes interface checks guaranteeing that components interact with each other as specified. We have applied the proposed ILA-based methodology for protocol verification to several third-party design case studies. These include an AXI on-chip communication protocol, an off-chip communication protocol, and a cache coherence protocol. For each system, we successfully detected bugs in the implementation, and show that the full formal verification can be completed in reasonable time and effort.

Convolution Neural Networks (CNNs) are widely deployed in computer vision applications. The datasets are large, and the data reuse across different parts is heavily interleaved. Given that memory access (SRAM and especially DRAM) is more expensive in both performance and energy than computation, maximizing data reuse to reduce data movement across the memory hierarchy is critical to improving execution efficiency. This is even more important for the common use case of CNNs on mobile devices where computing/memory resources are limited. We propose CNNFlow, a memory-driven dataflow optimization framework to automatically schedule CNN computation on a given CNN architecture to maximize data reuse at each level of the memory hierarchy. We provide a mathematical calculation for data reuses in terms of parameters including loop ordering, blocking, and memory-bank allocation for tensors in CNN. We then present a series of techniques that help prune the large search space and reduce the cost of the exploration. This provides, for the first time, an exact and practical search algorithm for optimal solutions to minimize memory access cost for CNN. The efficacy is demonstrated for two widely used CNN algorithms: AlexNet and VGG16 with 5 and 13 convolution layers, respectively. CNNFlow finds the optimal solution for each layer within tens of minutes of compute time. Its solution requires about 20% fewer DRAM accesses and 40%–80% fewer SRAM accesses compared to state-of-the-art algorithms in the literature.

Simulation-based testing has been the workhorse of hardware implementation validation. For processors, tandem simulation improves test and debug efficiency by cross-level simulating the Instruction Set Architecture (ISA) and RTL models, and comparing architectural-state variables at the end of each instruction rather than at the end of the whole trace. Further, the simulation may start with the ISA model and switch to the RTL model at some point by transferring the values of the architectural variables, thus speeding up the “warm-up” phase. However, thus far tandem simulation has been limited to processor designs as other SoC components lack high-level ISA models and thus the notion of instructions. Even for processors, significant manual effort is required in connecting the two models and constructing the necessary controller to synchronize/check/swap between them. This paper leverages the recently proposed Instruction-level Abstractions (ILAs) for generalizing tandem simulation to accelerators. Further, we use the refinement-map that is part of the ILA verification methodology to automate the connection between the ILA and the RTL simulation models for both processors and accelerators. We provide seven case studies to demonstrate the practical applicability of our methodology.

Hardware platforms comprise general-purpose processors and application-specific accelerators. Unlike processors, application-specific accelerators often do not have clearly specified architecture-level models/specifications (the instruction set architecture or ISA). This poses challenges to the development and verification/validation of firmware/software for these accelerators. Manually writing architecture-level models takes great effort and is error-prone. When Register-Transfer Level (RTL) designs are available, they can be a source from which to automatically derive the architecture-level models. In this work, we propose an approach for automatically generating architecture-level models for processors as well as accelerators from their RTL designs. In previous work we showed how to automatically extract the architectural state variables (ASVs) from RTL designs. (These are the state variables that are persistent across instructions.) In this work we present an algorithm for generating the update functions of the model: how the ASVs and outputs are updated by each instruction. Experiments on several processors and accelerators demonstrate that our approach can cover a wide range of hardware features and generate high-quality architecture-level models within reasonable time.

Recent years have witnessed increasing use of domain-specific accelerators in computing platforms to provide power-performance efficiency for emerging applications. To increase their applicability within the domain, these accelerators tend to support a large set of functions, e.g. Nvidia's open-source Deep Learning Accelerator, NVDLA, supports five distinct groups of functions [17]. However, an individual use case of an accelerator may utilize only a subset of these functions. The unused functions lead to unnecessary overhead of silicon area, power, and hardware verification/hardware-software co-verification complexity. This motivates our research question: Given an RTL design for an accelerator and a subset of functions of interest, can we automatically extract a subset of the RTL that is sufficient for these functions and sequentially equivalent to the original RTL? We call this the Usage-based RTL Subsetting problem, referred to as the RTL subsetting problem in short. We first formally define this problem and show that it can be formulated as a program synthesis problem, which can be solved by performing expensive hyperproperty checks. To overcome the high cost, we propose multiple levels of sound over-approximations to construct an effective algorithm based on relatively less expensive temporal property checking and taint analysis for information flow checking. We demonstrate the acceptable computation cost and the quality of the results of our algorithm through several case studies of accelerators from different domains. The applicability of our proposed algorithm can be seen in its ability to subset the large NVDLA accelerator (with over 50,000 registers and 1,600,000 gates) for the group of convolution functions, where the subset reduces the total number of registers by 18.6% and the total number of gates by 37.1%.

Property-based specification s uch a s SystemVerilog Assertions (SVA) uses mathematical logic to specify the temporal behavior of RTL designs which can then be formally verified using model checking algorithms. These properties are specified for a single component (which may contain other components in the design hierarchy). Composing design components that have already been verified requires additional verification since incorrect communication at their interface may invalidate the properties that have been checked for the individual components. This paper focuses on a specification for their interface which can be checked individually for each component, and which guarantees that refinement-based properties checked for each component continue to hold after their composition. We do this in the setting of the Instruction-level Abstraction (ILA) specification and verification methodology. The ILA methodology provides a uniform specification for processors, accelerators and general modules at the instruction-level, and the automatic generation of a complete set of correctness properties for checking that the RTL model is a refinement of the ILA specification. We add an interface specification to model the inter-ILA communication. Further, we use our interface specification to generate a set of interface checking properties that check that the communication between the RTL components is correct. This provides the following guarantee: if each RTL component is a refinement of its ILA specification and the interface checks pass, then the RTL composition is a refinement of the ILA composition. We have applied the proposed methodology to six case studies including parts of large-scale designs such as parts of the FlexASR and NVDLA machine learning accelerators, demonstrating the practical applicability of our method.

For processors, an instruction-set-architecture (ISA) provides a complete functional specification that can be used to formally verify an implementation. There has been recent work in specifying accelerators using formal instruction sets, referred to as Instruction-Level Abstractions (ILAs), and using them to formally verify their implementations by leveraging processor verification techniques. In this paper, we generalize ILAs for specification of general hardware modules and formal verification of their RTL implementations. This includes automated generation of a complete set of functional (not including timing) specification properties using the ILA instructions. We address the challenges posed by this generalization and provide several case studies to demonstrate the applicability of this technique, including all the modules in an open-source 8051 micro-controller. This verification identified three bugs and completed in reasonable time.

Today's Systems-on-Chips (SoCs) comprise general/special purpose programmable processors and specialized hardware modules referred to as accelerators. These accelerators serve as co-processors and are invoked through software or firmware. Thus, verifying SoCs requires co-verification of hardware with software/firmware. Co-verification using cycle-accurate hardware models is often not scalable, and requires hardware abstractions. Among various abstractions, architecture-level abstractions are very effective as they retain only the software visible state. An Instruction-Set Architecture (ISA) serves this role for processors and such ISA-like abstractions are also desirable for accelerators. Manually creating such abstractions for accelerators is tedious and error-prone, and there is a growing need for automation in deriving them from existing Register-Transfer Level (RTL) implementations. An important part of this automation is determining which state variables to retain in the abstract model. For processors and accelerators, this set of variables is naturally the Architectural State Variables (ASVs) - variables that are persistent across instructions. This paper presents the first work to automatically determine ASVs of processors and accelerators from their RTL implementations. We propose three novel algorithms based on different characteristics of ASVs. Each algorithm provides a sound abstraction, i.e., an over-approximate set of ASVs. The quality of the abstraction is measured by the size of the set of ASVs computed. Experiments on several processors and accelerators demonstrate that these algorithms perform best in different cases, and by combining them a high quality set of ASVs can be found in reasonable time.

There is an increasing body of work in the area of hardware defenses for software-driven security attacks. A significant challenge in developing these defenses is that the space of security vulnerabilities and exploits is large and not fully understood. This results in specific point defenses that aim to patch particular vulnerabilities. While these defenses are valuable, they are often blindsided by fresh attacks that exploit new vulnerabilities. This article aims to address this issue by suggesting ways to make future defenses more durable based on an organization of security vulnerabilities as they arise throughout the program life cycle. We classify these vulnerability sources through programming, compilation, and hardware realization, and we show how each source introduces unintended states and transitions into the implementation. Further, we show how security exploits gain control by moving the implementation to an unintended state using knowledge of these sources and how defenses work to prevent these transitions. This framework of analyzing vulnerability sources, exploits, and defenses provides insights into developing durable defenses that could defend against broader categories of exploits. We present illustrative case studies of four important attack genealogies—showing how they fit into the presented framework and how the sophistication of the exploits and defenses have evolved over time, providing us insights for the future.

The increasing importance of inference algorithms, such as neural networks (NNs), principle component analysis (PCA), and singular value decomposition (SVD), etc., has led to the emergence of hardware accelerators to address power-performance tradeoffs in their implementation. Their large data sets make DRAM access the bottleneck for power and performance. Private SRAM scratch-pad memory is used to mitigate the DRAM access penalty but it is a limited resource in size and bandwidth. Thus, accelerator design is not just about computation, but also how data flow is scheduled across the memory hierarchy, including DRAM, scratch-pad SRAM, and datapath registers. Current accelerator design tools automate the generation of customized datapaths to improve performance, but have limited support for reducing DRAM/SRAM accesses during the computation. In this paper, we propose a memory-driven accelerator design methodology for large-scale inference applications, to maximize data access in the datapath and SRAM. We demonstrate its efficacy using several key kernels from large-scale inference applications.

Accelerators for sparse matrix multiplication are important components in emerging systems. In this paper, we study the main challenges of accelerating Sparse Matrix Multiplication (SpMM). For the situations that data is not stored in the desired order (row/column order), we propose a compact high performance sparse format, which allows for random access to a dataset with low memory access overhead. We show that using this format results in a 14-49 times speedup for SpMM. Next, we propose a high performance systolic architecture for SpMM, which uses a mesh of comparators to locate the useful (non-zero) computation. This design maximizes data reuse by sharing the input data among a row/column of the mesh. We also show that, with similar memory access assumptions, the proposed architecture results in a 9-30 times speedup in comparison with the state of the art.

Attacks often succeed by abusing the gap between program and machine-level semantics-- for example, by locating a sensitive pointer, exploiting a bug to overwrite this sensitive data, and hijacking the victim program's execution. In this work, we take secure system design on the offensive by continuously obfuscating information that attackers need but normal programs do not use, such as representation of code and pointers or the exact location of code and data. Our secure hardware architecture, Morpheus, combines two powerful protections: ensembles of moving target defenses and churn. Ensembles of moving target defenses randomize key program values (e.g., relocating pointers and encrypting code and pointers) which forces attackers to extensively probe the system prior to an attack. To ensure attack probes fail, the architecture incorporates churn to transparently re-randomize program values underneath the running system. With frequent churn, systems quickly become impractically difficult to penetrate. We demonstrate Morpheus through a RISC-V-based prototype designed to stop control-flow attacks. Each moving target defense in Morpheus uses hardware support to individually offer more randomness at a lower cost than previous techniques. When ensembled with churn, Morpheus defenses offer strong protection against control-flow attacks, with our security testing and performance studies revealing: i) high-coverage protection for a broad array of control-flow attacks, including protections for advanced attacks and an attack disclosed after the design of Morpheus, and ii) negligible performance impacts (1%) with churn periods up to 50 ms, which our study estimates to be at least 5000x faster than the time necessary to possibly penetrate Morpheus.

To improve the performance of sparse matrix-matrix multiplication (SpMM) running on a specialized architecture, orchestrating a data flow that maximizes data reuse in local memory is critical but challenging due to the irregular non-zero element locations and the wide range of sparsity. In this work, we proposed SpFlow, a memory-driven data flow optimization framework for SpMM. SpFlow can realize 54X fewer DRAM accesses and 97X fewer SRAM accesses on average than a GPU running the cuSPARSE kernel. And in comparison with a state-of-the-art accelerator, the performance can be improved by 3X, and SRAM accesses reduced by 5X on average.

We present ILAng, a platform for modeling and verification of systems-on-chip (SoCs) using Instruction-Level Abstractions (ILA). The ILA formal model targeting the hardware-software interface enables a clean separation of concerns between software and hardware through a unified model for heterogeneous processors and accelerators. Top-down it provides a specification for functional verification of hardware, and bottom-up it provides an abstraction for software/hardware co-verification. ILAng provides a programming interface for (i) constructing ILA models (ii) synthesizing ILA models from templates using program synthesis techniques (iii) verifying properties on ILA models (iv) behavioral equivalence checking between different ILA models, and between an ILA specification and an implementation. It also provides for translating models and properties into various languages (e.g., Verilog and SMT LIB2) for different verification settings and use of third-party verification tools. This paper demonstrates selected capabilities of the platform through case studies. Data or code related to this paper is available at: [ 9 ].

Contemporary integrated circuits (ICs) are increasingly being constructed using intellectual property blocks (IPs) obtained from third parties in a globalized supply chain. The increased vulnerability to adversarial changes during this untrusted supply chain raises concerns about the integrity of the end product. The difference in the levels of abstraction between the initial specification and the final available circuit design poses a challenge for analyzing the final circuit for malicious insertions. Reverse engineering presents one way to help reduce the difficulty of circuit analysis and inspection. In this work, we provide a framework that given (i) a gate-level netlist of a design and (ii) a block diagram for the design with relative sizes of the blocks, outputs a matching between the partitions of the circuit and blocks in the block diagram. We first compute a geometric embedding for each node in the circuit and then apply a clustering algorithm on the embedding features to obtain circuit partitions. Each partition is then mapped to the high-level blocks in the block diagram. These partitions can then be further analyzed for malicious insertions with much reduced complexity in comparison with the full chip. We tested our algorithm on different designs with varying sizes to evaluate the efficacy of algorithm, including the open-source processor OpenSparc T1, and showed that we can successfully match over 90% of gates to their corresponding blocks.

Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to the pre-accelerator era, when the ISA played an important role in verification by enabling a clean separation of concerns between software and hardware, verification of these “accelerator-rich” SoCs presents new challenges. From the perspective of hardware designers, there is a lack of a common framework for formal functional specification of accelerator behavior. From the perspective of software developers, there exists no unified framework for reasoning about software/hardware interactions of programs that interact with accelerators. This article addresses these challenges by providing a formal specification and high-level abstraction for accelerator functional behavior. It formalizes the concept of an Instruction Level Abstraction (ILA), developed informally in our previous work, and shows its application in modeling and verification of accelerators. This formal ILA extends the familiar notion of instructions to accelerators and provides a uniform, modular, and hierarchical abstraction for modeling software-visible behavior of both accelerators and programmable processors. We demonstrate the applicability of the ILA through several case studies of accelerators (for image processing, machine learning, and cryptography), and a general-purpose processor (RISC-V). We show how the ILA model facilitates equivalence checking between two ILAs, and between an ILA and its hardware finite-state machine (FSM) implementation. Further, this equivalence checking supports accelerator upgrades using the notion of ILA compatibility, similar to processor upgrades using ISA compatibility.

SRAM scratch-pad memory in accelerators is limited in size and bandwidth. Besides computation, accelerator design is about how data flow is scheduled across the memory hierarchy, from DRAM to datapath registers. There is limited support for this in current tools. Thus, we propose MemFlow, memory-driven data scheduling with datapath co-design in accelerators, to improve computing performance and reduce higher-level memory accesses. We demonstrate its efficacy using several key kernels from large-scale inference applications.

The secure information flow problem, which checks whether low-security outputs of a program are influenced by high-security inputs, has many applications in verifying security properties in programs. In this paper we present lazy self-composition, an approach for verifying secure information flow. It is based on self-composition, where two copies of a program are created on which a safety property is checked. However, rather than an eager duplication of the given program, it uses duplication lazily to reduce the cost of verification. This lazy self-composition is guided by an interplay between symbolic taint analysis on an abstract (single copy) model and safety verification on a refined (two copy) model. We propose two verification methods based on lazy self-composition. The first is a CEGAR-style procedure, where the abstract model associated with taint analysis is refined, on demand, by using a model generated by lazy self-composition. The second is a method based on bounded model checking, where taint queries are generated dynamically during program unrolling to guide lazy self-composition and to conclude an adequate bound for correctness. We have implemented these methods on top of the SeaHorn verification platform and our evaluations show the effectiveness of lazy self-composition.

Formal security verification of firmware interacting with hardware in modern Systems-on-Chip (SoCs) is a critical research problem. This faces the following challenges: (1) design complexity and heterogeneity, (2) semantics gaps between software and hardware, (3) concurrency between firmware/hardware and between Intellectual Property Blocks (IPs), and (4) expensive bit-precise reasoning. In this paper, we present a co-verification methodology to address these challenges. We model hardware using the Instruction-Level Abstraction (ILA), capturing firmware-visible behavior at the architecture level. This enables integrating hardware behavior with firmware in each IP into a single thread. The co-verification with multiple firmware across IPs is formulated as a multi-threaded program verification problem, for which we leverage software verification techniques. We also propose an optimization using abstraction to prevent expensive bit-precise reasoning. The evaluation of our methodology on an industry SoC Secure Boot design demonstrates its applicability in SoC security verification.

Modern Systems-on-Chip (SoCs) integrate heterogeneous compute elements ranging from non-programmable specialized accelerators to programmable CPUs and GPUs. To ensure correct system behavior, SoC verification techniques must account for inter-component interactions through shared memory, which necessitates reasoning about memory consistency models (MCMs) This paper presents ILA-MCM, a symbolic reasoning framework for automated SoC verification, where MCMs are integrated with Instruction-Level Abstractions (ILAs) that have been recently proposed to model architecture-level program-visible states and state updates in heterogeneous SoC components. ILA-MCM enables reasoning about system-wide properties that depend on functional state updates as well as ordering relations between them. Central to our approach is a novel facet abstraction, where a single program-visible variable is associated with potentially multiple facets that act as auxiliary state variables. Facets are updated by ILA "instructions," and the required orderings between these updates are captured by MCM axioms. Thus, facets provide a symbolic constraint-based integration between operational ILA models and axiomatic MCM specifications. We have implemented a prototype ILA-MCM framework and use it to demonstrate two verification applications in this paper: (a) finding a known bug in an accelerator-based SoC, plus a new potential bug under a weaker MCM, and (b) checking that a recently proposed low-level GPU hardware implementation is correct with respect to a high-level ILA-MCM specification.

Today, secure systems are built by identifying potential vulnerabilities and then adding protections to thwart the associated attacks. Unfortunately, the complexity of today's systems makes it impossible to prove that all attacks are stopped, so clever attackers find a way around even the most carefully designed protections. In this article, we take a sobering look at the state of secure system design, and ask ourselves why the "security arms race" never ends? The answer lies in our inability to develop adequate security verification technologies. We then examine an advanced defensive system in nature - the human immune system - and we discover that it does not remove vulnerabilities, rather it adds offensive measures to protect the body when its vulnerabilities are penetrated We close the article with brief speculation on how the human immune system could inspire more capable secure system designs.

GPUs have been widely used to accelerate big-data inference applications and scientific computing through their parallelized hardware resources and programming model. Their extreme parallelism increases the possibility of bugs such as data races and un-coalesced memory accesses, and thus verifying program correctness is critical. State-of-the-art GPU program verification efforts mainly focus on analyzing application-level programs, e.g., in C, and suffer from the following limitations: (1) high false-positive rate due to coarse-grained abstraction of synchronization primitives, (2) high complexity of reasoning about pointer arithmetic, and (3) keeping up with an evolving API for developing application-level programs. In this paper, we address these limitations by modeling GPUs and reasoning about programs at the instruction level. We formally model the Nvidia GPU at the parallel execution thread (PTX) level using the recently proposed Instruction-Level Abstraction (ILA) model for accelerators. PTX is analogous to the Instruction-Set Architecture (ISA) of a general-purpose processor. Our formal ILA model of the GPU includes non-synchronization instructions as well as all synchronization primitives, enabling us to verify multithreaded programs. We demonstrate the applicability of our ILA model in scalable GPU program verification of data-race checking. The evaluation shows that our checker outperforms state-of-the-art GPU data race checkers with fewer false-positives and improved scalability.

Modern system-on-chip (SoC) designs comprise programmable cores, application-specific accelerators, and I/O devices. Accelerators are controlled by software/firmware and functionality is implemented by this combination of programmable cores, firmware, and accelerators. Verification of such SoCs is challenging, especially for system-level properties maintained by a combination of firmware and hardware. Attempting to formally verify the full SoC design with both firmware and hardware is not scalable, while separate verification can miss bugs. A general technique for scalable system-level verification is to construct an abstraction of SoC hardware and verify firmware/software using it. There are two challenges in applying this technique in practice. Constructing the abstraction to capture required details and interactions is error-prone and time-consuming. The second is ensuring abstraction correctness so that properties proven with it are valid. This paper introduces a methodology for SoC design and verification based on the synthesis of instruction-level abstractions (ILAs). The ILA is an abstraction of SoC hardware which models updates to firmware-visible state at the granularity of instructions. For hardware accelerators, the ILA is analogous to the instruction-set architecture definition for programmable processors and enables scalable verification of firmware interacting with hardware accelerators. To alleviate the disadvantages of manual construction of abstractions, we introduce two algorithms for synthesis of ILAs from partial description called templates. We then show how the ILA can be verified to be correct. We evaluate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 15 bugs.

Outsourcing of design and manufacturing processes makes integrated circuits (ICs) vulnerable to adversarial changes and raises concerns about their integrity. Reverse engineering the manufactured netlist helps identify malicious insertions. In this article, we present an automated approach that, given a reference design description with high-level blocks, infers these blocks in an untrusted gate-level (test) implementation. Using the graph connectivity of the netlists, we compute a geometric embedding for each wire in the circuits, which, then, is used to compute a bipartite matching between the nodes of the two designs and identify high-level blocks in the test circuit. Experiments to evaluate the efficacy of the proposed technique on various-sized designs, including the multi-core processor OpenSparc T1, show that it can correctly match over 90% of gates in the test circuit to their corresponding block in the reference model.

We propose a methodology to determine the suitability of different data representations in terms of their error-tolerance for a given application with accelerator-based computing. This methodology helps match the characteristics of a representation to the data access patterns in an application. For this, we first identify a benchmark of key kernels from linear algebra that can be used to construct applications of interest using any of several widely used data representations. This is then used in an experimental framework for studying the error tolerance of a specific data format for an application. As case studies, we evaluate the error-tolerance of seven dataformats on sparse matrix to vector multiplication, diagonal add, and two machine learning applications i) principal component analysis (PCA), which is a statistical technique widely used in data analysis and ii) movie recommendation system with Restricted Boltzmann Machine (RBM) as the core. We observe that the Dense format behaves well for complicated data accesses such as diagonal accessing but is poor in utilizing local memory. Sparse formats with simpler addressing methods and a careful selection of stored information, e.g., CRS and ELLPACK, demonstrate a better error-tolerance for most of our target applications.

Malicious software, referred to as malware, continues to grow in sophistication. Past proposals for malware detection have primarily focused on software-based detectors which are vulnerable to being compromised. Thus, recent work has proposed hardware-assisted malware detection. In this paper, we introduce a new framework for hardware-assisted malware detection based on monitoring and classifying memory access patterns using machine learning. This provides for increased automation and coverage through reducing user input on specific malware signatures. The key insight underlying our work is that malware must change control flow and/or data structures, which leaves fingerprints on program memory accesses. Building on this, we propose an online framework for detecting malware that uses machine learning to classify malicious behavior based on virtual memory access patterns. Novel aspects of the framework include techniques for collecting and summarizing per-function/system-call memory access patterns, and a two-level classification architecture. Our experimental evaluation focuses on two important classes of malware (i) kernel rootkits and (ii) memory corruption attacks on user programs. The framework has a detection rate of 99.0% with less than 5% false positives and outperforms previous proposals for hardware-assisted malware detection.

We present LIAMC, a novel decision procedure for (quantifier-free) linear arithmetic over both integers modulo 2N(LIAn) and integers (LIA). There is no need to explain our motivation to design a new efficient decision procedure for the widely used LIA logic. A LIAndecision procedure can be extremely useful in the context of software (SW) verification. SW verification usually requires to reason about arithmetic constraints over finite integers. To that end, modern SW verification tools commonly use fixed-width bit-vector (BV) solvers. However, BV solvers' efficiency drops dramatically as the width increases. To solve the performance problem, LIA solvers are applied, but they are imprecise as they cannot handle integer overflow. An efficient LIANsolver would be the ideal solution in this context. Our decision procedure LIAMC is based on a transformation of linear arithmetic into safety verification. We treat integers as unbounded streams of bits over time. More precisely, for each input integer, the least significant bit (LSB) corresponds to time 0 in the corresponding stream, and the k-th bit corresponds to the bit received at time k. LIAMC then uses SAT-based model checking (SATMC) to solve the resulting problem. In order to achieve efficiency, LIAMC uses two forms of generalization. First, if it finds a formula to be unsatisfiable for width N, it tries to generalize this result for all the widths. Second, if LIAMC finds a formula to be satisfiable for width N, it tries to “extend” and thus generalize the assignment to a wider target width. To evaluate LIAMC we used the QF_LIA subset of SMT-COMP'16, and ran two sets of experiments. First, we reinterpreted the QF_LIA over fixed-width bit-vectors of varying widths and compared LIAMC in LIAn mode to both Boolector and Z3. LIAMC solved the most satisfiable instances out of the three even for the shortest width 32. Second, we compared LIAMC to CVC4 and Z3 on the original QF_LIA benchmarks. LIAMC was able to solve many instances that had not been solved by the other solvers.

With increasing technology scaling and design complexity there are increasing threats from device and circuit failures. This is expected to worsen with post-CMOS devices. Current error-resilient solutions ensure reliability of circuits through protection mechanisms such as redundancy, error correction, and recovery. However, the costs of these solutions may be high, rendering them impractical. In contrast, error-tolerant solutions allow errors in the computation and are positioned to be suitable for error-tolerant applications such as media applications. For such programmable error-tolerant processors, the Instruction-Set-Architecture (ISA) no longer serves as a specification since it is acceptable for the processor to allow for errors during the execution of instructions. In this work, we address this specification gap by defining the basic requirements needed for an error-tolerant processor to provide acceptable results. Furthermore, we formally define properties that capture these requirements. Based on this, we propose the Partially Protected Uniprocessor (PPU), an error-tolerant processor that aims to meet these requirements with low-cost microarchitectural support. These protection mechanisms convert potentially fatal control errors to potentially tolerable data errors instead of ensuring instruction-level or byte-level correctness. The protection mechanisms in PPU protect the system against crashes, unresponsiveness, and external device corruption. In addition, they also provide support for achieving acceptable result quality. Additionally, we provide a methodology that formally proves the specification properties on PPU using model checking. This methodology uses models for the hardware and software that are integrated with the fault and recovery models. Finally, we experimentally demonstrate the results of model checking and the application-level quality of results for PPU.

This paper describes a methodology for system-level security verification of modern Systems-on-Chip (SoC) designs. These designs comprise interacting firmware and hardware modules which makes verification particularly challenging. These challenges relate to (i) specifying security verification properties, and (ii) verifying these properties across firmware and hardware. We address the latter through raising the level of abstraction of the hardware modules to be similar to that of instructions in software/firmware. This abstraction, referred to as an instruction-level abstraction (ILA), plays a similar role to the instruction set architecture (ISA) definition for general purpose processors and enables high-level analysis of SoC firmware. In particular, the ILA can be used instead of the cycle-accurate bit-precise hardware implementation for scalable verification of system-level security properties in SoCs.

As semiconductor technology scales towards ever-smaller transistor sizes, hardware fault rates are increasing. Since important application classes (e.g., multimedia, streaming workloads) are data-error-tolerant, recent research has proposed techniques that seek to save energy or improve yield by exploiting error tolerance at the architecture/microarchitecture level. Even seemingly error-tolerant applications, however, will crash or hang due to control-flow/memory addressing errors. In parallel computation, errors involving inter-thread communication can have equally catastrophic effects. Our work explores techniques that mitigate the impact of potentially catastrophic errors in parallel computation, while still garnering power, cost, or yield benefits from data error tolerance. Our proposed CommGuard solution uses FSM-based checkers to pad and discard data in order to maintain semantic alignment between program control flow and the data communicated between processors. CommGuard techniques are low overhead and they exploit application information already provided by some parallel programming languages (e.g. StreamIt). By converting potentially catastrophic communication errors into potentially tolerable data errors, CommGuard allows important streaming applications like JPEG and MP3 decoding to execute without crashing and to sustain good output quality, even for errors as frequent as every 500μs.

Integrated Circuits (ICs) are designed and fabricated in a globalized multi-vendor environment making them vulnerable to malicious design changes and the insertion of hardware Trojans/malware. In this talk I will cover two distinct techniques to address the problem of detecting hardware Trojans. The first uses SAT and BDD-based functional analysis to reverse engineer ICs. The goal here is to derive the higher-level function of IC through algorithmic analysis of its netlist to help expose the Trojan logic. The second uses statistical analysis of chip simulation data in a clustering algorithm to isolate the Trojan logic. I will discuss these techniques, their practical application on benchmark circuits and their complementary strengths. This is joint work with Burcin Cakir and Pramod Subramanyan.

Contemporary integrated circuits are complex system-on-chip (SoC) designs consisting of programmable cores along with accelerators and peripherals controlled by firmware running on the cores. The functionality of the SoC is implemented by a combination of firmware and hardware components. As a result, verifying these two components separately can miss bugs while attempting to formally verify the full SoC design considering both firmware and hardware is not scalable. An abstraction that can be used instead of the cycle-accurate and bit-precise hardware implementation can be helpful in scalably verifying system-level properties of SoCs. However, constructing such an abstraction to capture all the required details and interactions is error-prone, tedious and time-consuming. Another challenge is ensuring correctness of the abstraction so that properties proven using it are valid. In this paper, we introduce a methodology for SoC verification. We synthesize an instruction-level abstraction (ILA) that precisely captures updates to all firmware-accessible states spanning the cores, accelerators and peripherals. The synthesis algorithm uses a blackbox simulator to synthesize the ILA from a template specification. A "golden-model" generated from the ILA is used to verify whether the hardware implementation matches the ILA. We demonstrate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 14 bugs.

There has been significant recent research in reliable architectures. This is in response to the perceived hardware failure threats faced by late- and post-CMOS devices, e.g., energized particle hits, increasing variability of device parameters and aging-related failures. This body of research proposes specific micro-architecture mechanisms to defend against these threats. Each proposed mechanism makes some assumptions about the underlying fault model and addresses some set of errors. Of particular interest are error-tolerant processors which do not guarantee that the processor will execute each instruction strictly as per the ISA, but rather provide a best-effort response to these faults. These processors are suited for application classes which are error-tolerant, e.g. media processing, and thus provide useful output even without strictly implementing their ISA. What is left unsaid is the minimum guarantees that they must provide to result in useful computation. This paper addresses this question. It makes the following contributions (i) It provides a minimum set of properties that such processors must satisfy, e.g., progress and non-accumulating errors, and states these formally using temporal logic for a model of the processor. This model captures not just the error-free function, but also the faults and the error response mechanisms. (ii) We have developed such full-system models for two case studies of recently proposed fault-tolerant processors, YMM [16] and ERSA [5]. (iii) Further, we present the result of model checking these properties for both case-studies and show that they do not fully satisfy these properties.

Boolean satisfiability (SAT)-the problem of determining whether there exists an assignment satisfying a given Boolean formula-is a fundamental intractable problem in computer science. SAT has many applications in electronic design automation (EDA), notably in synthesis and verification. Consequently, SAT has received much attention from the EDA community, who developed algorithms that have had a significant impact on the performance of SAT solvers. EDA researchers introduced techniques such as conflict-driven clause learning, novel branching heuristics, and efficient unit propagation. These techniques form the basis of all modern SAT solvers. Using these ideas, contemporary SAT solvers can often handle practical instances with millions of variables and constraints. The continuing advances of SAT solvers are the driving force of modern model checking tools, which are used to check the correctness of hardware designs. Contemporary automated verification techniques such as bounded model checking, proof-based abstraction, interpolation-based model checking, and IC3 have in common that they are all based on SAT solvers and their extensions. In this paper, we trace the most important contributions made to modern SAT solvers by the EDA community, and discuss applications of SAT in hardware model checking.

There is a strong trend in networking to move towards Software-Defined Networks (SDN). SDNs enable easier network configuration through a separation between a centralized controller and a distributed data plane comprising a network of switches. The controller implements network policies through installing rules on switches. Recently the "Big Switch" abstraction [1] was proposed as a specification mechanism for high-level network behavior, i.e., the network policies. The network operating system or compiler can use his specification for placing rules on individual switches. However, this is constrained by the limited capacity of the Ternary Content Addressable Memories (TCAMs) used for rules in each switch. We propose an Integer Linear Programming (ILP) based solution for placing rules on switches for a given firewall policy while optimizing for the total number of rules and meeting the switch capacity constraints. Experimental results demonstrate that our approach is scalable to practical sized networks.

When verifying or reverse-engineering digital circuits, one often wants to identify and understand small components in a larger system. A possible approach is to show that the sub-circuit under investigation is functionally equivalent to a reference implementation. In many cases, this task is difficult as one may not have full information about the mapping between input and output of the two circuits, or because the equivalence depends on settings of control inputs. We propose a template-based approach that automates this process. It extracts a functional description for a low-level combinational circuit by showing it to be equivalent to a reference implementation, while synthesizing an appropriate mapping of input and output signals and setting of control signals. The method relies on solving an exists/forall problem using an SMT solver, and on a pruning technique based on signature computation.

Silicon fault diagnosis, the process of locating faults in a chip prototype, becomes more challenging and time-consuming with increasing design complexity. Consistency-based fault diagnosis aims at identifying fault candidates for an erroneous execution trace by symbolically checking the consistency between the golden gate-level model and the faulty behavior of the prototype chip. The scalability of this technique is limited to short executions due to the underlying decision procedure. This problem has previously been addressed by restricting the analysis to a window of fixed size and moving it along the execution trace. In this setting, limited observability results in a loss of precision and potentially missed fault candidates. We present a novel interpolation-based framework which formalizes the propagation of state information across sliding windows as a satisfiability problem. Our approach provides both spatial and temporal localization for general faults and is not restricted to a specific fault model. Further, our approach can be used to provide more accurate localization for a single permanent fault model. We experimentally demonstrate the efficacy and scalability of this approach by applying it to a variety of benchmarks from multiple suites (OpenCores, ITC99 and HWMCC).

Network operators often need to change their routing policy in response to network failures, new load balancing strategies, or stricter security requirements. While several recent works have aimed at solving this problem, they all assume that a fast and conveniently dimensioned out-of band network is available to communicate with any device. Unfortunately, such a parallel network is often not practical. This paper presents a technique for performing such updates in-band: it enables reconfiguration control messages to be sent directly within the fast production network. Performing such updates is hard because intermediate configurations can lock out the controller from devices before they are updated. Thus, updates have to be carefully sequenced. Our technique also minimizes the total update time by updating the network in parallel, whenever possible. Our technique takes into account in-band middle boxes, such as firewalls. We have implemented our framework using Integer Linear Programming, and experimentally validated it on problems of realistic scale.

We present a satisfiability backbone-based formulation for ranking structure discovery and thereby present an alternative scalable proof technique for the response properties. Our algorithm offers enhanced automation by reducing the need for user supplied input information compared to the known technique for ranking structure discovery [1]. We demonstrate that backbone based response verification algorithm scales up or attains comparable scalability without user supplied safety invariants.

Integrated circuits (ICs) are now designed and fabricated in a globalized multi-vendor environment making them vulnerable to malicious design changes, the insertion of hardware trojans/malware and intellectual property (IP) theft. Algorithmic reverse engineering of digital circuits can mitigate these concerns by enabling analysts to detect malicious hardware, verify the integrity of ICs and detect IP violations. In this paper, we present a set of algorithms for the reverse engineering of digital circuits starting from an unstructured netlist and resulting in a high-level netlist with components such as register files, counters, adders and subtracters. Our techniques require no manual intervention and experiments show that they determine the functionality of more than 51% and up to 93% of the gates in each of the practical test circuits that we examine.

As semiconductor fabrics scale closer to fundamental physical limits, their reliability is decreasing due to process variation, noise margin effects, aging effects, and increased susceptibility to soft errors. Reliability can be regained through redundancy, error checking with recovery, voltage scaling and other means, but these techniques impose area/energy costs. Since some applications (e.g. media) can tolerate limited computation errors and still provide useful results, error-tolerant computation models have been explored, with both the application and computation fabric having stochastic characteristics. Stochastic computation has, however, largely focused on application-specific hardware solutions, and is not general enough to handle arbitrary bit errors that impact memory addressing or control in processors. In response, this paper addresses requirements for error-tolerant execution by proposing and evaluating techniques for running error-tolerant software on a general-purpose processor built from an unreliable fabric. We study the minimum error-protection required, from a microarchitecture perspective, to still produce useful results at the application output. Even with random errors as frequent as every 250µs, our proposed design allows JPEG and MP3 benchmarks to sustain good output quality—14dB and 7dB respectively. Overall, this work establishes the potential for error-tolerant single-threaded execution, and details its required hardware/system support.

Computer systems face increasing challenges in simultaneously meeting an application's energy, performance, and reliability goals. While energy and performance tradeoffs have been studied through different dynamic voltage and frequency scaling (DVFS) policies and power management schemes, tradeoffs of energy and performance with reliability have not been studied for general purpose computing. This is particularly relevant for application domains such as multimedia, where some limited application error tolerance can be exploited to reduce energy [7]. In this paper, we present EPROF, an optimization framework based on Mixed-Integer Linear Programming (MILP) that selects possible schedules for running tasks on multiprocessors in order to minimize energy while meeting constraints on application performance and reliability. We consider parallel applications that express (on task graphs) the performance and reliability goals they need to achieve, and that run on chip multiprocessors made up of heterogeneous processor cores that offer different energy/performance/reliability tradeoffs. For the StreamIt benchmarks [16], EPROF can identify schedules that offer up to 34% energy reduction over a baseline method while achieving the targeted performance and reliability. More broadly, EPROF demonstrates how these three degrees of freedom (energy, performance and reliability) can be flexibly exploited as needed for different applications.

The increasing pressure to make hardware resilient to runtime failures has prompted development of design techniques for specific classes of systems, e.g. processors and routers. However, these techniques come at increased design and verification costs, thus limiting their broader application. In this work we describe a methodology for general RTL designs based on the widely usable checkpointing and rollback resiliency mechanism. We take a modeling and language approach that provides an appropriate set of abstractions for the resiliency logic. This cleanly separates the main design behavior from the resiliency behavior, leading to ease of design. Further, as the language abstractions can be automatically synthesized into resiliency logic, our methodology can merge with existing design flows. The concerns of verifying this additional resiliency logic can be addressed by synthesizing behavioral assertions capturing correct behavior. We demonstrate the use of this methodology on four examples, with synthesis for performance and area to estimate the overhead of the additional synthesis logic.

Firewalls are widely deployed to safeguard the security of networks and it is critical for enterprise networks to have firewalls to prevent malicious attacks and to guarantee the normal functioning of the network. Firewalls prevent dangerous packets from entering the inner network by looking up the Access Control List (ACL) to permit or drop certain packets. However, ACLs often suffer from redundancy problems, which can degrade the performance of firewalls and the network. The contribution of this paper is threefold: 1) we present a Boolean Satisfiability (SAT) based technique that can compare the equivalence and inclusion relationship between two firewalls, which is very valuable for the testing between a given firewall and an optimized one, 2) we present a technique to discover redundancies within a firewall, and 3) we formulate the ACL optimization problem as a Quantified Boolean Formula problem (QBF) and explore its practical application using a QBF solver.

A parallel program must execute correctly even in the presence of unpredictable thread interleavings. This interleaving makes it hard to write correct parallel programs, and also makes it hard to find bugs in incorrect parallel programs. A range of tools have been developed to help debug parallel programs, ranging from atomicity-violation and data-race detectors to model-checkers and theorem provers. One technique that has been successful for debugging sequential programs, but less effective for parallel programs, is running the program using assertion predicates provided by the developer. These assertions allow programmers to specify and check their assumptions. In a multi-threaded program, the programmer's assumptions include both the current state, and any actions (e.g. access to shared memory) that other, parallel executing threads might take. We introduce parallel assertions which allow programmers to express these assumptions for parallel programs using simple and intuitive syntax and semantics. We present a proof-of-concept implementation, and demonstrate its value by testing a number of benchmark programs using parallel assertions.

We address the problem of detecting serializability violations in a concurrent program using predictive analysis, where a violation is detected either in an observed trace or in an alternate interleaving of events in that trace. Under the widely used notion of conflict-serializability, checking whether a given execution is serializable can be done in polynomial time. However, when all possible interleavings are considered, the problem becomes intractable. We address this in practice through a graph-based method, which for a given atomic block and trace, derives a smaller segment of the trace, referred to as the Trace Atomicity Segment (TAS), for further systematic exploration. We use the observed write-read pairs of events in the given trace to consider a set of events that guarantee feasibility, i.e., each interleaving of these events corresponds to some real execution of the program. We call this set of interleavings the almost view-preserving (AVP) interleavings. We show that the TAS is sufficient for finding serializability violations among all AVP interleavings. Further, the TAS enables a simple static check that can prove the absence of a violation. This check often succeeds in practice. If it fails, we perform a systematic exploration over events in the TAS, where we use dynamic partial order reduction with additional pruning to reduce the number of interleavings considered. Unlike previous efforts that are less precise, when our method reports a serializability violation, the reported interleaving is guaranteed to correspond to an actual execution of the program. We report experimental results that demonstrate the effectiveness of our method in detecting serializability violations for Java and C/C++ benchmark programs.

Ensuring the correctness of complex implementations of software transactional memory (STM) is a daunting task. Attempts have been made to formally verify STMs, but these are limited in the scale of systems they can handle and generally verify only a model of the system, and not the actual system. In this paper we present an alternate attack on checking the correctness of an STM implementation by verifying the execution runs of an STM using a checker that runs in parallel with the transaction memory system. With future many-core systems predicted to have hundreds and even thousands of cores, it is reasonable to utilize some of these cores for ensuring the correctness of the rest of the system. This will be needed anyway given the increasing likelihood of dynamic errors due to particle hits (soft errors) and increasing fragility of nanoscale devices. These errors can only be detected at runtime. An important correctness criterion that is the subject of verification is the serializability of transactions. While checking transaction serializability is NP-complete, practically useful subclasses such as interchange-serializability (DSR) are efficiently computable. Checking DSR reduces to checking for cycles in a transaction ordering graph which captures the access order of objects shared between transaction instances. Doing this concurrent to the main transaction execution requires minimizing the overhead of capturing object accesses, and managing the size of the graph, which can be as large as the total number of dynamic transactions and object accesses. We discuss techniques for minimizing the overhead of access logging which includes time-stamping, and present techniques for on-the-fly graph compaction that drastically reduce the size of the graph that needs to be maintained, to be no larger than the number of threads. We have implemented concurrent serializability checking in the Rochester Software Transactional Memory (RSTM) system. We present our practical experiences with this including results for the RSTM, STAMP and synthetic benchmarks. The overhead of concurrent checking is a strong function of the transaction length. For long transactions this is negligible. Thus the use of the proposed method for continuous runtime checking is acceptable. For very short transactions this can be significant. In this case we see the applicability of the proposed method for debugging.

An important correctness issue for emerging multi/many-core shared memory systems is to ensure that the inter-processor communication through shared memory conforms to the memory ordering rules, as specified by the architecturepsilas memory consistency model. This presents a significant validation challenge. Growing system complexity makes it increasingly hard to identify all deep-state logic bugs in pre-silicon verification. Further, aggressive technology scaling makes hardware more vulnerable to dynamic errors that can only be detected at runtime. In this paper, we propose an approach for runtime validation of memory ordering. This allows us to survive bugs that escape pre-silicon verification, as well as deal with emerging dynamic errors. Our solution consists of two parts: 1) at the microarchitecture level, we add efficient hardware support to capture the observed ordering among shared-memory operations; 2) we perform online verification of the observed memory ordering by checking for cycles in the constraint graph. We combine these to achieve end-to-end correctness validation of the system execution with respect to the memory ordering specification. There are several challenges that need to be addressed to make this approach practical. We describe these, as well as optimization techniques for reducing the hardware overhead. Estimates obtained from preliminary chip multiprocessor simulation experiments show that the proposed techniques are very effective in achieving acceptable hardware overhead and minimal performance impact.

Traditional hardware modeling using RTL presents a time-stationary view of the design state space which can be used to specify temporal properties for model checking. However, highlevel information in terms of computation being performed on units of data (transactions) is not directly available. In contrast, transaction-level microarchitecture models view the computation as sequences of (data-stationary) transactions. This makes it easy to specify properties which involve both transaction sequencing and temporal ordering (e.g. data hazards). In RTL models, additional book-keeping state must be manually introduced in order to specify and check these properties. We show here that a transaction-level microarchitecture model can help automate checks for such properties via the automated creation of the book-keeping structures, and illustrate this for a simple pipeline using SMV. A key challenge in model-checking the transactionlevel microarchitecture is representing the dynamic transaction state space. We describe an encoding as well as a fixed point computation for this.

Our ability to verify complex hardware lags far behind our capacity to design and fabricate it. We argue that this gap is partly due to the limitations of RTL models when used for verification. Higher level models such as SystemC and SystemVerilog aim to raise the level of abstraction to enhance designer productivity; however, they largely provide for executable but not analyzable descriptions. We propose the use of formally analyzable design models at two distinct levels above RTL: the architecture and the microarchitecture level. At both these levels, we describe concurrent units of data computation termed transactions. The architecture level describes the computation/state updates in the transactions and their interaction through shared data. The microarchitecture level adds to this the resource usage in the transactions as well as their interaction based on shared resources. We then illustrate the applicability of these models in a top-down verification methodology which addresses several concerns of current methodologies.

In multiprocessor-based SoCs, optimizing the communication architecture is often as important, if not more important, than optimizing the computation architecture. While there are mature platforms and techniques for the modeling and evaluation of architectures of processing elements, the same is not true for the communication architectures. This article presents an application-driven retargetable prototyping platform that fills this gap. This environment aims to facilitate the design exploration of the communication subsystem through application-level execution-driven simulations and quantitative analysis. Based on an analysis of a wide range of on-chip communication architectures, we describe how a specific hierarchical class library can be used to develop new on-chip communication architectures, or variants of existing ones with relatively little incremental effort. We demonstrate this through three case studies including two commercial on-chip bus systems and an on-chip packet switching network. Here we show that, through careful analysis and construction, it is possible for the modeling environment to support the common features of these architectures as part of the library and permit instantiation of the individual architectures as variants of the library design. Consequently, system-level design choices regarding the communication architecture can be made with high confidence in the early stages of design. In addition to improving design quality, this methodology also results in significantly shortening design-time.

Despite the many improvements in the speed and robustness of DPLL-based SAT solvers, we still lack a thorough understanding of the working mechanisms and dynamic behaviour of these solvers at run-time. In this paper, we present TIGERDISP, a tool designed to allow researchers to visualize the dynamic behaviour of modern DPLL solvers in terms of time-dependent metrics such as decision depth, implications and learned conflict clauses. It is our belief that inferences about dynamic behaviour can be drawn more easily by visual analysis than by purely aggregate post-execution metrics such as total number of decisions/implications/conflicts. These inferences can then be validated through detailed quantitative analysis on larger sets of data. To this end, we have used TIGERDISP with the HAIFASAT and MINISAT solvers and have generated a few specific inferences about their relatively efficient and inefficient solving runs. We have then tested one of these inferences through quantitative analysis on a larger data set and have presented our findings in this paper. An important application of TIGERDISP would be in the development of a solver that employs adaptive algorithms. This is an area that has intrigued researchers in the past, but has not seen significant results for lack of a clear understanding as to what constitutes good progress during the run of a SAT solver. With better knowledge of dynamic behaviour, it is conceivable that an adaptive solver could be designed such that it switches between several competitive heuristics at runtime based on a quantitative analysis of its own dynamic behaviour

Boolean Satisfiability (SAT) has seen many successful applications in various fields, such as Electronic Design Automation (EDA) and Artificial Intelligence (AI). However, in some cases it may be required/preferable to use variations of the general SAT problem. In this paper we consider one important variation, the Minimum-Cost Satisfiability Problem (MinCostSAT). MinCostSAT is a SAT problem which minimizes the cost of the satisfying assignment. MinCostSAT has various applications, e.g. Automatic Test Pattern Generation (ATPG), FPGA Routing, AI Planning, etc. This problem has been tackled before - first by covering algorithms, e.g. scherzo [3], and more recently by SAT based algorithms, e.g. bsolo [16]. However the SAT algorithms they are based on are not the current generation of highly efficient solvers. The solvers in this generation, e.g. Chaff [20], MiniSat [5] etc., incorporate several new advances, e.g. two literal watching based Boolean Constraint Propagation, that have delivered order of magnitude speedups. We first point out the challenges in using this class of solvers for the MinCostSAT problem and then present techniques to overcome these challenges. The resulting solver MinCostChaff shows order of magnitude improvement over several current best known branch-and-bound solvers for a large class of problems, ranging from Minimum Test Pattern Generation, Bounded Model Checking in EDA to Graph Coloring and Planning in AI.

Modern processors face growing verification and reliability challenges posed by increasing micro-architecture complexity and aggressive technology scaling. While viable approaches have been proposed to address these challenges in the context of uniprocessors, little work has been done for emerging multithreaded processors. Multithreading raises new issues for validation due to inter-thread interactions and inherent complexity of the underlying hardware. We propose an extension of the DIVA approach, which employs a simple checker processor to effectively validate the complex superscalar processor, to perform instruction-level runtime validation for both intra-thread and inter-thread correctness properties for multithreaded execution. We present the validation methodology using a representative simultaneous-multithreaded (SMT) architecture, and briefly discuss its general applicability to other forms of multithreading. Detailed timing simulation shows this solution has low performance penalty, while providing general robustness against both operational and functional errors with relatively small hardware overhead

In digital hardware system design, the quality of the product is directly related to the number of meaningful design alternatives properly considered. Unfortunately, existing modeling methodologies and tools have properties which make them less than ideal for rapid and accurate design-space exploration. This article identifies and evaluates the shortcomings of existing methods to motivate the Liberty Simulation Environment (LSE). LSE is a high-level modeling tool engineered to address these limitations, allowing for the rapid construction of accurate high-level simulation models. LSE simplifies model specification with low-overhead component-based reuse techniques and an abstraction for timing control. As part of a detailed description of LSE, this article presents these features, their impact on model specification effort, their implementation, and optimizations created to mitigate their otherwise deleterious impact on simulator execution performance.

In multiprocessor-based system-on-chips (SOCs), optimizing the communication architecture is often as important as, if not more than, optimizing the computation architecture. While there are mature platforms and techniques for the modeling and evaluation of computation architectures, the same is not true for the communication architectures. A major challenge in modeling the communication architecture is managing the concurrency at multiple levels: at the operation level, multiple communication operations may be active at any time; at the microarchitecture level, several microarchitectural components may be operating in parallel. Further, it is important to be able to clearly specify how the operation-level concurrency maps to the microarchitectural-level concurrency. This paper presents a modeling methodology and a retargetable simulation framework which fill this gap. This framework seeks to facilitate the design space exploration of the communication subsystem through a rigorous modeling approach based on a formal concurrency model, the operation state machine (OSM). Our OSM-based modeling methodology enables the entire system including both the computation and communication architectures to be modeled in a single OSM framework. This allows us to develop a tool set that can synthesize cycle-accurate system simulators for multiprocessing-element SOC prototypes. We show that, by simulation, critical system information such as timing and communication patterns can be obtained and evaluated. Consequently, system-level design choices regarding the communication architecture can be made with high confidence in early stages of design.

Despite the increasing use of QBF solvers, current QBF solvers do not provide for any mechanism to verify their results. This paper demonstrates a methodology for independently validating the results of a DLL based QBF solver using the traces generated during the solving process. It also presents a mechanism to extract small unsatisfiable subformulas, called cores, from unsatisfiable QBF instances.

Boolean satisfiability (SAT) has seen significant use in various tasks in circuit verification. A key contributor to the efficiency of contemporary SAT solvers is fast deduction using Boolean constraint propagation (BCP). This can be efficiently implemented with a conjunctive normal form (CNF) representation of a circuit. However, most circuit verification tasks start from a logic circuit description of the problem instance. A simple conversion from a logic circuit to a CNF (Tseitin, G.S., 1968), that enables the use of the CNF representation even for circuit verification tasks, loses some information regarding the structure of the circuit. One example of such structural information is circuit observability don't cares. Several recent papers have addressed the issue of handling circuit unobservability in CNF-based SAT, but none of them accurately captures the conditions for use of this information in all stages of a CNF-based SAT solver. To take such don't care information into consideration in a CNF-based SAT solver, we propose a broader approach that adds certain don't care literals to clauses in the CNF representation. These literals are treated differently at different times during the solution process, much like don't cares in logic synthesis. The major merit of this scheme is that the solver can continue to use this don't care information during the learning process, which is an important part of contemporary SAT solvers. We have implemented this approach in the zChaff SAT solver and experiments show that significant performance gain can be obtained.

As packet-switching interconnection networks replace buses and dedicated wires to become the standard on-chip interconnection fabric, reducing their power consumption has been identified to be a major design challenge. Network topologies have high impact on network power consumption. Technology scaling is another important factor that affects network power, since each new technology changes semiconductor physical properties. These two aspects need to be considered synergistically. We characterize the impact of process technologies on network energy for a range of topologies, starting from 2-dimensional meshes/tori, to variants of meshes/tori that incorporate higher dimensions, multiple hierarchies and express channels. We present a method which uses an analytical model to predict the most energy-efficient topology based on network size and architecture parameters for future technologies. Our model is validated against cycle-accurate network power simulation and shown to arrive at the same predictions. We also show how our method can be applied to actual parallel benchmarks with a case study. We see this work as a starting point for defining a roadmap of future on-chip networks.

The increasing gap between design complexity and compute power for verification necessitates radically new solutions to meet the verification challenges for future generations of hardware designs. Increasingly it will not be possible to completely validate hardware prior to fabrication. We will need to reconcile ourselves to the fact that hardware, like software, will be shipped with bugs. However, this can be acceptable with appropriate mechanisms for runtime validation that detect bugs and recover from them when needed. This paper takes a significant step in examining runtime validation as part of the verification methodology. It examines the strengths and weaknesses of runtime validation and how it may be used to complement model checking in a hybrid methodology. We consider the use of on-chip hardware for detecting bugs using hardware assertions. These assertions may be used for validating abstractions and assumptions for use in offline model checking. Hardware based assertions monitor properties at runtime and do not suffer from the state explosion problem. Offline model checking is used to validate globally distributed properties where runtime error detection has limitations in monitoring and responding to signals separated by many clock cycles. In this case the hardware based runtime validated abstractions and assumptions help in reducing the state space for model checking. Our ideas are demonstrated on a highly concurrent, yet simple to understand token sharing protocol, as well as a fairly complex cache coherence system.

Dynamic voltage/frequency scaling (DVFS) has been shown to be an efficient power/energy reduction technique. Various runtime DVFS policies have been proposed to utilize runtime DVFS opportunities. However, it is hard to know if runtime DVFS opportunities have been fully exploited by a DVFS policy without knowing the upper bounds of possible energy savings. We propose an exact but exponential algorithm to determine the upper bound of energy savings. The algorithm takes into consideration the switching costs, discrete voltage/frequency voltage levels and different program states. We then show a fast linear time heuristic can provide a very close approximate to this bound

In multiprocessor based SoCs, optimizing the communication architecture is often as important, if not more important, than optimizing the computation architecture. While there are mature platforms and techniques for the modeling and evaluation of architectures of processing elements, the same is not true for the communication architectures. This paper presents an application-driven retargetable prototyping platform which fills this gap. This environment aims to facilitate the design exploration of the communication sub-system through application-level execution-driven simulations and quantitative analysis. First, we introduce an expressive communication architecture specification which gives the designers the freedom to choose and configure their custom interconnection schemes over a wide range of communication architectures, covering the spectrum from buses to packet switching networks. This, combined with a distributed application model, drives a modular modeling and simulation environment that permits detailed simulation of the communication (and computation) architectures at the application level. Through the case studies motivated by an embedded system application, we show that through simulations, critical system information such as timings and communication patterns can be obtained and evaluated. Consequently, system-level design choices regarding the communication architecture can be made with high confidence in the early stages of design. In addition to improving design quality, this methodology also results in significantly shortening design-time.

Rapidly increasing design and manufacturing non-recurring engineering (NRE) costs are prompting a shift in electronic design from hardwired application specific integrated circuits (ASICs) to the use of software on programmable platforms. However, in order to minimize the power and performance overhead of such processors, we are seeing the introduction of domain or application specific processors such as network and communication processors. The design of such specialized processors requires software development tools such as simulators and compilers. In order to quickly develop these tools for multiple design points under consideration, it is highly desirable to have them synthesized from formal processor descriptions written in Architecture Description Languages (ADLs). In this paper, we present the Mescal Architecture Description Language (MADL). MADL features a two-layer structure, a core layer and an annotation layer. The core layer is based on a formal and flexible microprocessor model -- the operation state machine (OSM), which enables MADL to express the concurrency at the operation execution level for a wide range of architectures. We address the challenges faced in designing the core layer to combine the OSM model with techniques for achieving compact processor descriptions. The annotation layer features a generic syntax that allows creating annotation schemes to specify implementation dependent or tool specific information. To show the effectiveness of MADL, we present an MADL-based simulator synthesis framework that has been used to generate efficient cycle accurate simulators and instruction set simulators with very low development effort. We also describe our annotation schemes that enable the extraction of architecture properties for use in instruction scheduling and integer-linear-programming based register allocation. Our experimental results demonstrate the efficacy of MADL as a practical and promising language for the development of programmable platforms.

Dynamic voltage scaling (DVS) has become an important dynamic power-management technique to save energy. DVS tunes the power-performance tradeoff to the needs of the application. The goal is to minimize energy consumption while meeting performance needs. Since CPU power consumption is strongly dependent on the supply voltage, DVS exploits the ability to control the power consumption by varying a processor's supply voltage and clock frequency. However, because of the energy and time overhead associated with switching DVS modes, DVS control has been used mainly at the interprogram level.In this paper, we explore the opportunities and limits of intraprogram DVS scheduling. An analytical model is derived to predict the maximum energy savings that can be obtained using intraprogram DVS given a few known program and processor parameters. This model gives insights into scenarios where energy consumption benefits from intraprogram DVS and those where there is no benefit. The model helps us extrapolate the benefits of intraprogram DVS into the future as processor parameters change. We then examine how much of these predicted benefits can actually be achieved through compile-time optimal settings of DVS modes. We extend an existing mixed-integer linear program formulation for this scheduling problem by accurately accounting for DVS energy switching overhead, by providing finer-grained control on settings and by considering multiple data categories in the optimization. Overall, this research provides a comprehensive view of intraprogram compile-time DVS management, providing both practical techniques for its immediate deployment as well theoretical bounds for use into the future.

Increasing nonrecurring engineering and mask costs are making it harder to turn to hardwired application specific integrated circuit (ASIC) solutions for high-performance applications. The volume required to amortize these high costs has been increasing, making it increasingly expensive to afford ASIC solutions for medium-volume products. This has led to designers seeking programmable solutions of varying sorts using these so-called programmable platforms. These programmable platforms span a large range from bit-level programmable field programmable gate arrays to word-level programmable application-specific, and in some cases even general-purpose processors. The programmability comes with a power and performance overhead. Attempts to reduce this overhead typically involve making some core hardwired ASIC like logic blocks accessible to the programmable elements. This paper presents one such hybrid solution in this space---a relatively simple processor with a dynamically reconfigurable datapath acting as an accelerating coprocessor. This datapath consists of hardwired function units and reconfigurable interconnect. We present a methodology for the design of these solutions and illustrate it with two complete case studies: an MPEG2 coder, and a GSM coder, to show how significant speedups can be obtained using relatively little hardware. This work is part of the MESCAL project, which is geared towards developing design environments for the development of application-specific platforms.

A binary decoder is a common component of software development tools such as instruction set simulators, disassemblers and debuggers. The efficiency of the decoder can have a significant impact on the efficiency of these software tools. Automated synthesis of efficient binary decoders is therefore necessary for retargetable software tool development frameworks targeting the rapidly growing field of application-specific processor design. This paper describes a decoder synthesis algorithm that translates a simple instruction pattern specification into efficient binary decoders in C under given memory constraints. The algorithm constructs a decision tree with carefully chosen decoding primitives and cost models. As demonstrated through two case studies, the synthesized decoders achieve efficiency comparable to hand-coded decoders with ensured correctness. The algorithm has no limitation on the input instruction patterns and it requires only the least amount of knowledge about the instruction encoding. Therefore it can be used with any machine description scheme containing instruction encoding information.

As demand for bandwidth increases in systems-on-a-chip and chip multiprocessors, networks are fast replacing buses and dedicated wires as the pervasive interconnect fabric for on-chip communication. The tight delay requirements faced by on-chip networks have resulted in prior microarchitectures being largely performance-driven. While performance is a critical metric, on-chip networks are also extremely power-constrained. In this paper, we investigate on-chip network microarchitectures from a power-driven perspective. We first analyze the power dissipation of existing network microarchitectures, highlighting insights that prompt us to devise several power-efficient network microarchitectures: segmented crossbar, cut-through crossbar and write-through buffer. We also study and uncover the power saving potential of existing network architecture: express cube. These techniques are evaluated with synthetic as well as real chip multiprocessor traces, showing a reduction in network power of up to 44.9%, along with no degradation in network performance, and even improved latency-throughput in some cases.

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.

Increasing non-recurring engineering (NRE) and mask costs are making it harder to turn to hardwired Application Specific Integrated Circuit (ASIC) solutions for high performance applications [12]. The volume required to amortize these high costs has been increasing, making it increasingly expensive to afford ASIC solutions for medium volume products. This has led to designers seeking programmable solutions of varying sorts using these so-called programmable platforms. These programmable platforms span a large range from bit-level programmable Field Programmable Gate Arrays (FPGAs), to word-level programmable application-specific, and in some cases even general-purpose processors. The programmability comes with a power and performance overhead. Attempts to reduce this overhead typically involve making some core hardwired ASIC like logic blocks accessible to the programmable elements. This paper presents one such hybrid solution in this space - a relatively simple processor with a dynamically reconfigurable datapath acting as an accelerating co-processor. This datapath consists of hardwired function units and reconfigurable interconnect. We present a methodology for the design of these solutions and illustrate it with two complete case studies: an MPEG 2 coder, and a GSM coder, to show how significant speedups can be obtained using relatively little hardware. The co-processor can be viewed as a VLIW processor with a single instruction per kernel loop. We compare the efficiency of exploiting the operation level parallelism using classic VLIW processors and this proposed class of dynamically configurable co-processors. This work is part of the MESCAL project, which is geared towards developing design environments for the development of application specific platforms.

As designers struggle with developing application solutions consisting of complex systems-on-a-chip with a significant software component, they must deal with a diversity of tools with very different philosophies and assumptions, to help manage this task. On one hand are tools which assume a clean separation between the hardware and software parts of the design with an abstraction of the hardware available for software development. On the other hand are tools that try to handle the hardware and software parts of the design concurrently. What drives these different philosophies? Which of these is critical for emerging system designs? Which of these is viable going forward? Our panel of experts consisting of designers, embedded software tool providers, system design tool providers and an academic will answer these challenging questions.

Within the verification community, there has been a recent increase in interest in Quantified Boolean Formula evaluation (QBF) as many interesting sequential circuit verification problems can be formulated as QBF instances. A closely related research area to QBF is Boolean Satisfiability (SAT). Recent advances in SAT research have resulted in some very efficient SAT solvers. One of the critical techniques employed in these solvers is Conflict Driven Learning. In this paper, we adapt conflict driven learning for application in a QBF setting. We show that conflict driven learning can be regarded as a resolution process on the clauses. We prove that under certain conditions, tautology clauses obtained from resolution in QBF also obey the rules for implication and conflicts of regular (non-tautology) clauses; and therefore they can be treated as regular clauses and used in future search. We have implemented this idea in a new QBF solver called Quaffle and our initial experiments show that conflict driven learning can greatly speed up the solution process for most of the benchmarks we tested.

The communication sub-system of complex IC systems is increasingly critical for achieving system performance. Given this, it is important that the on-chip communication architecture should be included in any quantitative evaluation of system design during design space exploration. While there are several mature methodologies for the modeling and evaluation of architectures of processing elements, there is relatively little work done in modeling of an extensive range of on-chip communication architectures, and integrating this into a single modeling and simulation environment combining processing element and on-chip communication architectures. This paper describes a modeling framework with accompanying simulation tools that attempts to fill this gap. Based on an analysis of a wide range of on-chip communication architectures, we describe how a specific hierarchical class library can be used to develop new on-chip communication architectures, or variants of existing ones with relatively little incremental effort. We demonstrate this through three case studies including two commercial on-chip bus systems and an on-chip packet switching network. Here we show that through careful analysis and construction it is possible for the modeling environment to support the common features of these architectures as part of the library and permit instantiation of the individual architectures as variants of the library design. As part of this methodology we also show how different levels of abstraction of the model can be supported and viewed as different variants that can be used in an accuracy versus simulation time trade-off.

A variety of factors is making it increasingly difficult and expensive to design and manufacture traditional Application Specific Integrated Circuits (ASICs). This has started a significant move towards the use of programmable solutions of various forms - increasingly referred to as programmable platforms. For the platform manufacturer, programmability provides higher volume to amortize design and manufacturing costs, as the same platform can be used over multiple related applications, as well as over generations of an application. For the application implementer, programmability provides a lower risk and shorter time-to-market implementation path. The flexibility provided by programmability comes with a performance and power overhead. This can be significantly mitigated by using application specific platforms, also referred to as Application Specific Instruction Set Processors (ASIPs). This paper details the reasons for this significant change in application implementation philosophy, provides illustrative contemporary evidence of this change, examines the space of application specific platforms, outlines fundamental problems in their development, and finally presents a methodology to deal with this changing design style.

We present Orion, a power-performance interconnection network simulator that is capable of providing detailed power characteristics, in addition to performance characteristics, to enable rapid power-performance tradeoffs at the architectural-level. This capability is provided within a general framework that builds a simulator starting from a microarchitectural specification of the interconnection network. A key component of this construction is the architectural-level parameterized power models that we have derived as part of this effort. Using component power models and a synthesized efficient power (and performance) simulator a microarchitect can rapidly explore the design space. As case studies, we demonstrate the use of Orion in determining optimal system parameters, in examining the effect of diverse traffic conditions, as well as evaluating new network microarchitectures. In each of the above, the ability to simultaneously monitor power and performance is key in determining suitable microarchitectures.

Boolean Satisfiability is probably the most studied of combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in Electronic Design Automation (EDA), as well as in Artificial Intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff, which achieves significant performance gains through careful engineering of all aspects of the search - especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on difficult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO.

Communication-based design represents a formal method approach to of system-on-a-chip design that considers communication between components as important as the computations they perform. “Our network-on-chip&rdqo ; approach partitions the communication into layers to maximize reuse and provide a programmer with an abstraction of the underlying communication framework. This layered approach is cast in the structure advocated by the OSI Reference network model and is demonstrated with a reconfigurable DSP example. The Metropolis methodology of deriving layers through a sequence of successive adaptation steps between incompatible behaviors refinement of communication is illustrated through the Intercom a design example. In another approach, MESCAL provides a designer with tools for a correct-by-construction protocol stack.

This research examines the role of dynamically reconfigurable logic in systems-on-a-chip (SoC) design. Specifically we study the overhead of storing and downloading the configuration code bits for different parts of an application in a dynamically reconfigurable coprocessor environment. For SoC designs the different configuration bit-streams will likely need to be stored on chip, thus it becomes crucial to reduce the storage overhead. In addition, reducing the reconfiguration time overhead is crucial in realizing performance benefits. This study provides insight into the granularity of the reconfigurable logic that is appropriate for the SoC context. Our initial study is in the domain of multimedia and communication systems. We first present profiling results for these using the MESCAL compiler infrastructure. These results are used to derive an architecture template that consists of dynamically reconfigurable datapaths using coarse grain logic blocks and a reconfigurable interconnection network. We justify this template based on the constraints of SoC design. We then describe a design flow where we start from an application, derive the kernel loops via profiling and then map the application using the dynamically reconfigurable datapath and the simplest interconnection network. As part of this flow we have developed a mapping algorithm that minimizes the size of the interconnection network and thus the overhead of reconfiguration, which is key for systems-on-a-chip. We provide some initial results that validate our approach.

Methods based on Boolean satisfiability (SAT) typically use a conjunctive normal form (CNF) representation of the Boolean formula, and exploit the structure of the given problem through use of various decision heuristics and implication methods. We propose a new decision heuristic based on separator-set induced partitioning of the underlying CNF graph. It targets those variables whose choice generates clause partitions with disjoint variable supports. This can potentially improve performance of SAT applications by decomposing the problem dynamically within the search. In the context of a recently proposed image computation method combining SAT and BDDs, this results in simpler BDD subproblems. We provide algorithms for CNF partitioning - one based on a clause-variable dependency matrix, and another based on standard hypergraph partitioning techniques, and also for the use of partitioning information in decision heuristics for SAT. The effectiveness of the proposed partition-based heuristic is shown with practical results for reachability analysis of benchmark sequential circuits.

One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2/spl times/ speedup compared with learning schemes employed in state-of-the-art SAT solvers.

Boolean Satisfiability (SAT) is a classical NP-complete problem with both theoretical and practical interests. This paper presents our work in developing an application-specific processor for SAT based on a commercial configurable processor core. We customize the processor configuration and design new instruction extensions based on the data structure and atomic operations used in SAT. The customized processor has achieved around 24 /spl times/ speedup at a very low hardware cost. The small size of the processor makes it possible to integrate multiple processors and other customized logic into a single chip for an application-specific multiprocessor solution for SAT. Our work shows the strength of application-specific processing in accelerating applications with complex control and dynamic data structures - an area that has traditionally not been targeted by application-specific processing. It also demonstrates that configurable processor cores can be used to cut the development time and cost for designing and building such application-specific processors.

A standard design methodology for embedded processors today is the system-on-a-chip design with potentially multiple heterogeneous processing elements on a chip, such as a very long instruction word (VLIW) processor, digital signal processor (DSP), and field-programmable gate array. To be able to program these devices, we need compilers that are capable of generating efficient code for the different types of processing elements with efficiency measured in terms of power, area, and execution time. In addition, the compilers should also be highly retargetable to enable the system designer to quickly evaluate different cores for the application on hand and reduce the time to market. In this paper, we show that we can extend a conventional VLIW compilation environment to develop highly retargetable optimizing compilers for DSPs with irregular architectures. We have used the second generation Fujitsu Hiperion fixed-point DSP as our primary example to evaluate the compiler framework. We demonstrate through experimental results that execution time for the assembly code generated using our framework is roughly two times better than that of the code generated by a widely used commercially available DSP compiler. Even without incorporating DSP-specific optimizations in our extended VLIW framework, we demonstrate that the compiled code has a better performance than the code generated by a commercial DSP-specific compiler in all our examples.

This article introduces the notion of a Complete-1-Distinguishability (C-1-D) property for simplifying equivalence checking of finite state machines (FSMs). When a specification machine has the C-1-D property, the traversal of the product machine can be eliminated. Instead, a much simpler check suffices. The check consists of first obtaining a 1-equivalence mapping between the individually reachable states of the specification and the implementation machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly for specification machines on which it naturally holds---a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on an arbitrary FSM by exposing some of its latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the trade-off curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

Article Handling irregular ILP within conventional VLIW schedulers using artificial resource constraints Share on Authors: Subramanian Rajagopalan Department of Electrical, Engineering, Princeton University, Princeton, NJ Department of Electrical, Engineering, Princeton University, Princeton, NJView Profile , Manish Vachharajani Department of Electrical, Engineering, Princeton University, Princeton, NJ Department of Electrical, Engineering, Princeton University, Princeton, NJView Profile , Sharad Malik Department of Electrical, Engineering, Princeton University, Princeton, NJ Department of Electrical, Engineering, Princeton University, Princeton, NJView Profile Authors Info & Claims CASES '00: Proceedings of the 2000 international conference on Compilers, architecture, and synthesis for embedded systemsNovember 2000 Pages 157–164https://doi.org/10.1145/354880.354902Online:01 November 2000Publication History 24citation161DownloadsMetricsTotal Citations24Total Downloads161Last 12 Months3Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

The design and design automation of embedded systems is rapidly emerging as a research area in its own right. It draws from several traditional areas of study such as system specification, modeling and analysis; computer architecture and micro-architecture; as well as compilers and operating systems. However, the embedded domain adds some interesting twists in terms of tighter problem constraints that demand a fresh look at even these traditional areas. In addition, there are several emerging EDA areas such as design reuse and integration of systems on a chip that are critical to the study of embedded systems. These aspects are not typically covered by computer engineering and EDA curricula. This panel addresses the challenges associated with the educational issues in embedded systems design and design automation. The panelists will examine issues in including embedded systems in university curricula, as well as in setting up research programs that are crucial for the education of graduate students.

Comprehensive study of incremental algorithms and solutions in the context of CAD tool development is an open area of research with a great deal of potential. Incremental algorithms for synthesis and layout are needed when design undergoes local or incremental change. Often these local changes are made to react to local change in the design, correct local errors or to make local improvements in one or more of the design quality metrics. In this paper we outline fundamental problems in incremental logic synthesis and physical design. Preliminary solutions to a subset of these problems are outlined.

Demonstrating our framework on a collection of scientific loop nests, we were able to reduce an average of 84% of cache misses in the optimizable loop nests. This work lays the groundwork for handling a wide range of optimizations through further study of solution patterns in the CME solution table.

We address the problem of code generation for DSP systems on a chip. In such systems, the amount of silicon devoted of program ROM is limited, so application software must be sufficiently dense. Additionally, the software must be written so as to meet various high-performance constraints, which may include hard real-time constraints. Unfortunately, current compiler technology is unable to generate high-quality code for DSPs, whose architectures are highly irregular. Thus, designers often resort to programming application software in assembly—a time-consuming task. In this paper, we focus on providing support for architectural feature of DSPs that makes code generation difficult, namely multiple data memory banks. This feature increases memory bandwith by permitting multiple data memory accesses to occur in parallel when the referenced variables belong to different data memory banks and the registers involved conform to a strict set of conditions. We present an algorithm that attempst to maximize the benefit of this architectural feature. While previous approaches have decoupled the phases of register allocation and memory bank assignment, thereby compromising code quality, our algorithm performs these two phases simultaneously. Experimental results demonstrate that our algorithm not only generates high-quality compiled code, but also improves the quality of completely-referenced code.

This paper presents a new algorithm for exact estimation of the minimum memory size required by programs dealing with array computations. Based on parametric partitioning of the iteration space and formalized live variable analysis, our algorithm transforms the minimum memory size estimation into an equivalent problem: integer point counting for intersection/union of mappings of parameterized polytopes. A heuristics was then proposed to solve the counting problem. Experimental results show that the algorithm achieves the exactness traditionally associated with totally unrolling loops while exploiting reduced computation complexity by preserving the original loop structure.

This paper presents a new algorithm for exact estimation of the minimum memory size required by programs dealing with array computations.

The issues of software compute time and complexity are very important in current computer-aided design (CAD) tools. As field-programmable gate array (FPGA) speeds and densities increase, the opportunity for effective hardware accelerators built from FPGA technology has opened up. This paper describes and evaluates a formula-specific method for implementing Boolean satisfiability solver circuits in configurable hardware. That is, using a template generator, we create circuits specific to the problem instance to be solved. This approach yields impressive runtime speedups of up to several hundred times compared to the software approaches. The high performance comes from realizing fine-grained parallelism inherent in the clause evaluation and implication and from direct mapping of Boolean relations into logic gates. Our implementation uses a commercially available hardware system for proof of concept. This system yields more than 100 times run-time speedup on many problems, even though the clock rate of the hardware is 100 times slower than that of the workstation running the software solver. While the time to compile the solver circuit to configurable hardware can he quite long on current platforms (20-40 min per chip), this paper discusses new approaches to overcome this compilation overhead. More broadly, we view this work as a case study in the burgeoning domain of high performance configurable computing. Our approach realizes large amount of fine-grained parallelism, and has broad applications in the very large scale integration CAD area.

Embedded systems generally interact in some way with the outside world. This may involve measuring sensors and controlling actuators, communicating with other systems, or interacting with users. These functions impose real-time constraints on system design. Verification of these specifications requires computing an upper bound on the worst-case execution time (WCET) of a hardware/software system. Furthermore, it is critical to derive a tight upper bound on WCET in order to make efficient use of system resources. The problem of bounding WCET is particularly difficult on modern processors. These processors use cache-based memory systems that vary memory access time based on the dynamic memory access pattern of the program. This must be accurately modeled in order to tightly bound WCET. Several analysis methods have been proposed to bound WCET on processors with instruction caches. Existing approaches either search all possible program paths, an intractable problem, or they use highly pessimistic assumptions to limit the search space. In this paper we present a more effective method for modeling instruction cache activity and computing a tight bound on WCET. The method uses an integer linear programming formulation and does not require explicit enumeration of program paths. The method is implemented in the program cinderella and we present some experimental results of this implementation.

With the ever-widening performance gap between processors and main memory, cache memory, which is used to bridge this gap, is becoming more and more significant. Caches work well for programs that exhibit sufficient locality. Other programs, however, have reference patterns that fail to exploit the cache, thereby suffering heavily from high memory latency. In order to get high cache efficiency and achieve good program performance, efficient memory accessing behavior is necessary. In fact, for many programs, program transformations or source-code changes can radically alter memory access patterns, significantly improving cache performance. Both hand-tuning and compiler optimization techniques are often used to transform codes to improve cache utilization. Unfortunately, cache conflicts are difficult to predict and estimate, precluding effective transformations. Hence, effective transformations require detailed knowledge about the frequency and causes of cache misses in the code. This article describes methods for generating and solving Cache Miss Equations (CMEs) that give a detailed representation of cache behavior, including conflict misses, in loop-oriented scientific code. Implemented within the SUIF compiler framework, our approach extends traditional compiler reuse analysis to generate linear Diophantine equations that summarize each loop's memory behavior. While solving these equations is in general difficult, we show that is also unnecessary, as mathematical techniques for manipulating Diophantine equations allow us to relatively easily compute and/or reduce the number of possible solutions, where each solution corresponds to a potential cache miss. The mathematical precision of CMEs allows us to find true optimal solutions for transformations such as blocking or padding. The generality of CMEs also allows us to reason about interactions between transformations applied in concert. The article also gives examples of their use to determine array padding and offset amounts that minimize cache misses, and to determine optimal blocking factors for tiled code. Overall, these equations represent an analysis framework that offers the generality and precision needed for detailed compiler optimizations.

Analyzing and optimizing program memory performance is a pressing problem in high-performance computer architec-tures. Currently, software solutions addressing the processor-memory performance gap include compiler- or programmer-applied optimizations like data structure padding, matrix blocking, and other program transformations. Compiler op-timization can be effective, but the lack of precise analysis and optimization frameworks makes it impossible to confi-dently make optimal, rather than heuristic-based, program transformations. Imprecision is most problematic in situa-tions where hard-to-predict cache conflicts foil heuristic ap-proaches. Furthermore, the lack of a general framework for compiler memory performance analysis makes it impossi-ble to understand the combined effects of several program transformations. The Cache Miss Equation (CME) framework discussed in this paper addresses these issues. We express memory ref-erence and cache conflict behavior in terms of sets of equa-tions. The mathematical precision of CMEs allows us to find true optimal solutions for transformations like block-ing or padding. The generality of CMEs also allows us to reason about interactions between transformations applied in concert. Unlike our prior work, this framework applies to caches of arbitrary associativity. This paper also demon-strates the utility of CMEs by presenting precise algorithms for intra-variable padding, inter-variable padding, and se-lecting tile sizes. Our experiences with CMEs implemented in the SUIF system show that they are a unifying mathemat-ical framework offering the generality and precision impera-tive for compiler optimizations on current high-performance architectures. 1

The Boolean satisfiability problem lies at the core of several CAD applications, including automatic test pattern generation and logic synthesis. This paper describes and evaluates an approach for accelerating Boolean satisfiability using configurable hardware. Our approach harnesses the increasing speed and capacity of field-programmable gate arrays by tailoring the SAT-solver circuit to the particular formula being solved. This input-specific technique gets high performance due both to (i) a direct mapping of Boolean operations to logic gates, and (ii) large amounts of fine-grain parallelism in the implication processing. Overall, these strategies yields impressive speedups (>200X in many cases) compared to current software approaches, and they require only modest amounts of hardware. In a broader sense, this paper alerts the hardware design community to the increasing importance of input-specific designs, and documents their promise via a quantitative study of input-specific SAT solving.

This paper describes and evaluates methods for implementing formula-specific Boolean satisfiability (SAT) solver circuits in configurable hardware. Starting from a general template design, our approach automatically generates VHDL for a circuit that is specific to the particular Boolean formula being solved. Such an approach tightly customizes the circuit to a particular problem instance. Thus, it represents an ideal use for dynamically-reconfigurable hardware, since it would be impractical to fabricate an ASIC for each Boolean formula being solved. Our approach also takes advantage of direct gate mappings and large degrees of fine-grained parallelism in the algorithm's Boolean logic evaluations. We compile our designs to two hardware targets: an IKOS logic emulation system, and Digital SRC's Pamette configurable computing board. Performance evaluations on the DIMACS SAT benchmark suite indicate that our approach offers speedups from 17X to more than a thousand times. Overall, this SAT solver demonstrates promising performance speedups on an important and complex problem with extensive applications in the CAD and AI communities.

The need to reduce the power consumption of the next generation of digital systems is clearly recognized at all levels of system design. At the system level, power management is a very powerful technique and delivers large and unambiguous savings. The ideas behind power management can be extended to the logic level. This would involve determining which parts of a circuit are computing results that will be used and which are not. The parts that are not needed are then "shut off". This paper describes an approach termed guarded evaluation, which is an implementation of this idea. A theoretical framework and the algorithms that form the basis of the approach are presented. The underlying idea is to automatically determine the parts of the circuit that can be disabled on a per-clock-cycle basis. This saves the power used in all the useless transitions in those parts of the circuit. Initial experiments indicate substantial power savings and the strong potential of this approach for a large number of benchmark circuits. While this paper presents the development of these ideas at the logic level of design, the same ideas have direct application at the register-transfer level of design also.

This paper examines the problem of code-generation for Digital Signal Processors (DSPs). We make two major contributions. First, for an important class of DSP architectures, we propose an optimal O(n) algorithm for the tasks of register allocation and instruction scheduling for expression trees. Optimality is guaranteed by sufficient conditions derived from a structural representation of the processor Instruction Set Architecture (ISA). Second, we develop heuristics for the case when basic blocks are Directed Acyclic Graphs (DAGs).

The biggest obstacle in the formal verification of large designs istheir very large state spaces, which cannot be handled even bytechniques such as implicit state space traversal. The only viablesolution in most cases is validation by functional simulation. Unfortunately, this has the drawbacksof high computationalrequirementsdue to the large number of test vectors needed, and the lack of adequate coverage measures to characterize the quality of a given testset. To overcome these limitations, there has been recent interest inhybrid techniques which combine the strengths of formal verification and simulation. Formal verification-based techniques are usedon a test model (usually much smaller than the design) to derive a setof functional test vectors, which are then used for design validationthrough simulation. The test set generated typically satisfies somecoverage measure on the test model. Recent research has proposedthe use of state or transition coverage. However, no effort has beenmade to relate these measures to the coverage of design errors. Furthermore, the derivation of the test model remains largely ad-hoc,with few formal guidelines.We demonstrate that under a given set of assumptions, transitiontours on test models can be used for complete validation of an implementation against a specification, for a large and important classof designs that includes many programmable/hardwired, general-purpose processors/DSPs. A by-product of this study is specificguidelines for deriving the test model, motivated by the requirement of providing complete coverage of all errors. We illustrate theapplication of our methodology on a pipelined implementation of the DLX processor.

This paper examines the problem of statically analyzing the performance of embedded software. This problem is motivated by the increasing growth of embedded systems and a lack of appropriate analysis tools.We study different performance metrics that need tobe considered in this context and examine a range oftechniques that have been proposed for analysis. Verybroadly these can be classified into path analysis andsystem utilization analysis techniques. It is observedthat these are interdependent, and thus need to beconsidered together in any analysis framework.

We investigate the problem of code generation for DSP systems on a chip. Such systems devote a limited quantity of silicon to program ROM, so application software must be maximally dense. Additionally, the software must be written so as to meet various high-performance constraints, which may include hard real-time constraints. Unfortunately, current compiler technology is unable to generate dense, high-performance code for DSPs, whose architectures are highly irregular. Consequently, designers often resort to programming application software in assembly-a Time-consuming, error-prone, and non-portable task. Thus, DSP compiler technology must be improved substantially. We describe some optimizations that significantly improve the quality of compiler-generated code. Our optimizations are applied globally and even across procedure calls. Additionally, they are applied to the machine-dependent assembly representation of the source program. Our target architecture is the Texas Instruments' TMS320C25 DSP.

Article Free Access Share on Cache miss equations: an analytical representation of cache misses Authors: Somnath Ghosh Department of Electrical Engineering, Princeton University Department of Electrical Engineering, Princeton UniversityView Profile , Margaret Martonosi Department of Electrical Engineering, Princeton University Department of Electrical Engineering, Princeton UniversityView Profile , Sharad Malik Department of Electrical Engineering, Princeton University Department of Electrical Engineering, Princeton UniversityView Profile Authors Info & Claims ICS '97: Proceedings of the 11th international conference on SupercomputingJuly 1997 Pages 317–324https://doi.org/10.1145/263580.263657Online:11 July 1997Publication History 144citation1,052DownloadsMetricsTotal Citations144Total Downloads1,052Last 12 Months48Last 6 weeks14 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In this paper we propose a data structure for abstracting the delay information of a combinatorial circuit. The particular abstraction that we are interested in is one that preserves the delays between all pairs of inputs and outputs in the circuit. Such abstractions are useful when considering the delay of cascaded circuits in high-level synthesis and other such applications in synthesis. The proposed graphical data structure is called the concise delay network, and is of size proportional to (m+n) in best case, where m and n refer to the number of inputs and outputs of the circuit. In comparison, a delay matrix that stores the maximum delay between each input-output pair has size proportional to m/spl times/n. For circuits with hundreds of inputs and outputs, this storage and the associated computations become quite expensive, especially when they need to be done repeatedly during synthesis. We present heuristic algorithms for deriving these concise delay networks. Experimental results shows that, in practice, we can obtain concise delay network with the number of edges being a small multiple of (m+n).

Embedded computer systems are characterized by the presence of a processor running application-specific dedicated software. A large number of these systems must satisfy real-time constraints. This paper examines the problem of determining the extreme (best and worst) case bounds on the running time of a given program on a given processor. This has several applications in the design of embedded systems with real-time constraints. An important aspect of this problem is determining which paths in the program are exercised in the extreme cases. The state-of-the-art solution here relies on an explicit enumeration of program paths. This solution runs out of steam rather quickly since the number of feasible program paths is typically exponential in the size of the program. We present a solution for this problem that does not require an explicit enumeration of program paths, i.e., the paths are considered implicitly. This solution is implemented in the program cinderella (in recognition of her hard real-time constraint-she had to be back home at the stroke of midnight), which currently targets a popular embedded processor-the Intel i960. The preliminary results of using this tool are also presented here.

Power is becoming a critical constraint for designing embedded applications. Current power analysis techniques based on circuit-level or architectural-level simulation are either impractical or inaccurate to estimate the power cost for a given piece of application software. In this paper, an instruction-level power analysis model is developed for an embedded digital signal processor (DSP) based on physical current measurements. Significant points of difference have been observed between the software power model for this custom DSP processor and the power models that have been developed earlier for some general purpose commercial microprocessors. In particular, the effect of circuit state on the power cost of an instruction stream is more marked in the case of this DSP processor. In addition, the processor has special architectural features that allow dual memory accesses and packing of instructions into pairs. The energy reduction possible through the use of these features is studied. The on-chip Booth multiplier on the processor is a major source of energy consumption for DSP programs. A microarchitectural power model for the multiplier is developed and analyzed for further power minimization. In order to exploit all of the above effects, a scheduling technique based on the new instruction-level power model is proposed. Several example programs are provided to illustrate the effectiveness of this approach. Energy reductions varying from 26% to 73% have been observed. These energy savings are real and have been verified through physical measurement. It should be noted that the energy reduction essentially comes for free. It is obtained through software modification, and thus, entails no hardware overhead. In addition, there is no loss of performance since the running times of the modified programs either improve or remain unchanged.

In this paper we address the problem of code generation for basic blocks in heterogeneous memory-register DSP processors. We propose a new a technique, based on register-transfer paths, that can be used for efficiently dismantling basic block DAGs (Directed Acyclic Graphs) into expression trees. This approach builds on recent results which report optimal code generation algorithm for expression trees for these architectures. This technique has been implemented and experimentally validated for the TMS320C25, a popular fixed point DSP processor. The results show that good code quality can be obtained using the proposed technique. An analysis of the type of DAGs found in the DSPstone benchmark programs reveals that the majority of basic blocks in this benchmark set are expression trees and leaf DAGs. This leads to our claim that tree based algorithms, like the one described in this paper, should be the technique of choice for basic block code generation with heterogeneous memoryregister a...

This paper introduces the use of the Complete-1-Distinguishability (C-1-D) property for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation and the specification. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between states of the two machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly on specifications for which it naturally holds a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on arbitrary FSMs by exposing some of the latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with using this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

Retiming is often used to optimize synchronous sequential circuits for area or delay or both. If the latches that are retimed have a hardware reset value, the initial state of the circuit must also be retimed, i.e. an initial state must be derived for the retimed circuit. Previously, it has been suggested that this can be avoided if the hardware reset signals are represented explicitly. However, it was thought that this adds unnecessary area and restricts the space of possible retimings. We demonstrate that this is not the case. In addition, we show that this methodology does not require the restriction that all reset signals be asserted at the beginning of circuit operation-a restriction that was imposed by existing algorithms for determining the retimed initial state. Finally we show how our explicit reset (ER) framework enables us to retime when some latches may be driven by different hardware resets, and some others may not have any hardware resets. We also consider the case where the resets are asynchronous. We expect these solutions to the "retimed initial state" problem to help increase the practical applicability of retiming.

We present a method for determining a tight bound on the worst case execution time of a program when running on a given hardware system with cache memory. Caches are used to improve the average memory performance, however, their presence complicates the worst case timing analysis. Any pessimistic predictions on cache hits/misses will result in loose estimation. In our previous research in this area, we built an integer-linear-programming solution for this problem which included analysis of direct mapped instruction caches. In this paper we describe the complex extensions of this technique to deal with set associative instruction caches, data caches and unified caches. We believe that this research now provides a comprehensive solution to the problem of worst case performance analysis of software running on processors with caches. These techniques have been implemented in a design tool cinderella. Some experimental results are presented that demonstrate the practical applicability of this analysis.

No abstract available.

No abstract available.

We survey state-of-the-art optimization methods that target low power dissipation in VLSI circuits. Optimizations at the circuit, logic, architectural and system levels are considered.

Embedded computer systems are characterized by the presence of a processor running application specific software.A large number of these systems must satisfy real-time constraints.This paper examines the problem of determining the bound on the running time of a given program on a given processor.An important aspect of this problem is determining the extreme case program paths.The state of the art solution here relies on an explicit enumeration of program paths.This runs out of steam rather quickly since the number of feasible program paths is typically exponential in the size of the program.We present a solution for this problem, which considers all paths implicitly by using integer linear programming.This solution is implemented in the program cinderella 1 which currently targets a popular embedded processor -the Intel i960.The preliminary results of using this tool are presented here.

This paper addresses the problem of speeding up functional (delay-independent) logic simulation for synchronous digital systems. The problem needs very little new motivation-cycle-based functional simulation is the largest consumer of computing cycles in system design. Most existing simulators for this task can he classified as being either event driven or levelized compiled-code, with the levelized compiled code simulators generally being considered faster for this task. An alternative technique, based on evaluation using branching programs, was suggested about a decade ago in the context of switch level functional simulation. However, this had very limited application since it could not handle the large circuits encountered in practice. This paper resurrects the basic idea present this technique and provides significant modifications that enable its application to contemporary industrial strength circuits. We present experimental results that demonstrate up to a 10X speedup over levelized compiled code simulation for a large suite of benchmark circuits as well as for industrial examples with over 40.000 gates.

Embedded systems generally interact with the outside world. Thus, some real-time constraints may be imposed on the system design. Verification of these constraints requires computing a tight upper bound on the worst case execution time (WCET) of a hardware/software system. The problem of bounding WCET is particularly difficult on modern processors, which use cache-based memory systems that vary memory access time significantly. This must be accurately modeled in order to tightly bound WCET. Existing approaches either search all possible program paths, an intractable problem, or they use pessimistic assumptions to limit the search space. In this paper we present afar more effective and accurate method for modeling instruction cache activity and computing a tight bound on WCET. It is implemented in the program cinderella. We present some preliminary results of using this tool on sample embedded programs.

An architectural feature commonly found in digital signal processors (DSPs) is multiple data-memory banks. This feature increases memory bandwidth by permitting multiple memory accesses to occur in parallel when the referenced variables belong to different memory banks and the registers involved are allocated according to a strict set of conditions, Unfortunately, current compiler technology is unable to take advantage of the potential increase in parallelism offered by such architectures, Consequently, most application software for DSP systems is hand-written-a very time-consuming task. We present an algorithm which attempts to maximize the benefit of this architectural feature. While previous approaches have decoupled the phases of register allocation and memory bank assignment, our algorithm performs these two phases simultaneously. Experimental results demonstrate that our algorithm substantially improves the code quality of many compiler-generated and even hand-written programs.

Real-time systems are characterized by the presence of timing constraints in which a task must be completed within a specific amount of time. This paper examines the problem of determining the bound on the worst case execution time (WCET) of a given program on a given processor There are two important issues in solving this problem: (i) program path analysis, which determines what sequence of instructions will be executed in the worst case, and (ii) microarchitecture modeling, which models the hardware system and determines the WCET of a known sequence of instructions. To obtain a tight estimate on the bound both these issues must be addressed accurately and efficiently. The latter is becoming difficult to model for modern processors due to the presence of pipelined instruction execution units and cached memory systems. Because of the complexity of the problem, all existing methods that we know of focus only on one of above issues. This limits the accuracy of the estimated bound and the size of the program that can be analyzed. We present a more effective solution that addresses both issues and uses an integer linear programming formulation to solve the problem. This solution is implemented in the program cinderella which currently targets the Intel i960KB processor and we present some experimental results of using this tool.

This paper addresses the performance optimization problem for sequential logic circuits. It is shown how the notion of false paths, traditionally defined for combinational logic circuits, can be extended to the sequential context by considering the operation of the circuit over multiple clock-cycles. These multicycle false paths can be removed from the circuit using techniques similar to those proposed for combinational logic circuits. This observation offers new techniques to improve the performance of sequential logic circuits. An implementation of an algorithm that uses these ideas shows significant performance improvement on some typical benchmark circuits at a modest area overhead.>

Paths that are never exercised are referred to as false paths and timing analysis that ignores the delay contribution of these paths is referred to as functional timing analysis. Such timing analysis provides a more accurate estimate of circuit delay compared to conventional static timing analysis. We show how unmodified conventional Automatic Test Pattern Generators (ATPG) for stuck-at faults can be used for functional timing analysis without sacrificing computational efficiency in comparison with existing approaches to the same problem. This is a significant result since it enables us to use the entire body of work in ATPG for this problem and relieves us from re-inventing new solutions for this problem. The basic algorithm can be used under an arbitrary delay model. We provide delay computation results for all the ISCAS benchmark examples under the unit-delay and the mapped-delay models.>

Circuits that have an underlying acyclic topology are guaranteed to be combinational since feedback is necessary for sequential behavior. However, the reverse is not true, i,e., feedback is not a sufficient condition since there do exist combinational logic circuits that are cyclic. In fact, such combinational circuits occur often in bus structures in data paths. This class of circuits has largely been ignored by conventional combinational single-stuck-at fault test pattern generators which assume that the circuit topology is acyclic. There has not been a formal study of the test generation problem for these circuits. Also, no algorithms and tools exist for this purpose. In practice, test generation for these circuits is handled in an awkward manner, typically with poor fault coverage. This work provides, for the first time, a formal analysis of the test generation problem for these circuits. This analysis leads to a clear insight into generation of tests, as well as a classification of untestable faults for such circuits. We demonstrate that cyclic combinational circuits may have untestable faults that do not correspond to redundancies. This insight is then translated to a testing algorithm which has been implemented in the program RAM. RAM has been successful in providing complete or near complete coverage on a range of typical examples, which is significantly higher than that provided by conventional techniques.>

The contribution of this paper is an implicit method for computing the minimum cost feedback vertex set for a graph.For an arbitrary graph, we efficiently derive a Boolean function whose satisfying assignments directly correspond to feedback vertex sets of the graph.Importantly, cycles in the graph are never explicitly enumerated, but rather, are captured implicitly in this Boolean function.This function is then used to determine the minimum cost feedback vertex set.Even though computing the minimum cost satisfying assignment for a Boolean function remains an NP-hard problem, we can exploit the advances made in the area of Boolean function representation in logic synthesis to tackle this problem efficiently in practice for even reasonably large sized graphs.The algorithm has obvious application in flip-flop selection for partial scan.Our algorithm was the first to obtain the MFVS solutions for many benchmark circuits.

Manufacturing disturbances are inevitable in the fabrication of integrated circuits. These disturbances will result in variations in the delay speci cations of manufactured circuits. In order to capture the impact of these variations on the delay behavior of these circuits we propose a pair of statistical delay models for use in logic design. These models abstract the real variations from the process level and can be used for statistical delay analysis and optimization in logic design and synthesis while o ering an e ciency vs. accuracy tradeo. 1

Timing simulation is a widely used method to verify the timing behavior of a design. In a synchronous digital system the timing property that needs to be verified is that there is no event at the outputs of the combinational parts of the circuit at or after time /spl tau/, the clock period. In this paper we first show that conventional timing simulation applied to this problem has exponential complexity. Next we demonstrate that for this problem a complete history of circuit activity before time /spl tau/ is not needed. We exploit this observation and present an event suppression method that potentially leads to an exponential reduction in the number of events that need to be processed during simulation. This is backed by encouraging experimental results.>

A logic circuit is said to be combinational if the function it computes depends only on the inputs applied to the circuit, and is sequential if it depends on some past history in addition to the current inputs. Circuits that have an underlying topology that is acyclic are combinational, since feedback is a necessary condition for them to be sequential. However, it is not a sufficient condition since there exist combinational logic circuits that are cyclic. These occur often in bus structures in data paths. Traditional formal techniques in logic synthesis, logic analysis, and timing analysis of combinational circuits have restricted themselves to acyclic combinational circuits, since they have been unable to handle the analysis of circuits with cycles. Thus, in practice, these circuits are handled using clumsy work-arounds, which is obviously undesirable. This paper presents a formal analysis of these circuits and presents techniques for the logical and timing analysis of such circuits. These techniques are practically feasible on reasonably large circuits encountered in practice.>

Most research in timing verification has implicitly assumed a single vector floating mode computation of delay which is an approximation of the multivector transition delay. In this paper we examine the transition delay of a circuit and demonstrate that the transition delay of a circuit can differ from the floating delay of a circuit. We then provide a procedure for directly calculating the transition delay of a circuit. The most practical benefit of this procedure is the fact that it not only results in a delay calculation but outputs a vector sequence that may be timing simulated to certify static timing verification.>

Embedded computer systems are characterized by the presence of a dedicated processor and the software that runs on it. Power constraints are increasingly becoming the critical component of the design specification of these systems. At present, however, power analysis tools can only be applied at the lower levels of the design-the circuit or gate level. It is either impractical or impossible to use the lower level tools to estimate the power cost of the software component of the system. This paper describes the first systematic attempt to model this power cost. A power analysis technique is developed that has been applied to two commercial microprocessors-Intel 486DX2 and Fujitsu SPARClite 934. This technique can be employed to evaluate the power cost of embedded software. This can help in verifying if a design meets its specified power constraints. Further, it can also be used to search the design space in software power optimization. Examples with power reduction of up to 40%, obtained by rewriting code using the information provided by the instruction level power model, illustrate the potential of this idea.>

The last couple of years have seen the addition of a new dimension in the evaluation of circuit quality -its power requirements.Low power circuits are emerging as an important application domain, and synthesis for low power is demanding attention.The research presented in this paper addresses one aspect of low power synthesis.It focuses on the problem of mapping a technology independent circuit to a technology specific one, using gates from a given library, with power as the optimization metric.Several issues in modeling and measuring circuit power, as well as algorithms for technology mapping for low power are presented here.Empirically, it is observed that a significant variation in the power consumption is possible Just by varying the choice of gates.Technology mapping for low power provides circuits with up to 24% lower power requirements than those obtained by technology mapping for area.

A logic circuit is said to be combinational if the function it computes depends only on the inputs applied to the circuit, and is sequential if it depends on some past history in addition to the current inputs. Circuits that have an underlying topology that is acyclic are combinational, since feedback is a necessary condition for it to be sequential. However, it is not a sufficient condition since there exist combinational logic circuits that are cyclic. These occur often in bus structures in data paths. Traditional formal techniques in logic synthesis, logic analysis and timing analysis of combinational circuits have restricted themselves to acyclic combinational circuits since they have been unable to handle the analysis of circuits with cycles. Thus, in practice, these circuits are handled using clumsy work-arounds, which is obviously undesirable. This paper presents a formal analysis of these circuits, and presents techniques for the logical and timing analysis of such circuits. These techniques are practically feasible on reasonably large circuits encountered in practice.

High performance circuit design is becoming increasingly important in VLSI design. The most important problem faced in the design of these circuits is to meet a certain performance level. In the past few years CAD algorithms and tools have been well developed that improve the performance of logic circuits in the sense that the worst case delay is minimized. However, manufacturers recognize that worst case delay models are typically pessimistic and the manufactured ICs will have a range of performances reflecting the manufacturing variations. Thus, the real problem that needs to be solved in the performance optimization of these circuits is to maximize the percentage of fabricated circuits that will achieve a certain performance level, as opposed to minimizing the worst case delay which has been the focus thus far. We develop methods to improve the statistical timing behavior of a combinational logic circuit, given probability distributions for the gate and wire delays. This work uses a statistical timing analysis technique developed earlier to drive timing optimization in the right direction to achieve a prescribed goal with the least area overhead.>

Addresses the problem of accurately computing the delay of a combinational logic circuit in the floating mode of operation. (In this mode the state of the circuit is considered to be unknown when a vector is applied at the inputs.) It is well known that using the length of the topologically longest path as an estimate of circuit delay may be pessimistic since this path may be false, i.e., it cannot propagate an event. Thus, the true delay corresponds to the length of the longest true path. This forces one to examine the conditions under which a path is true. The authors introduce the notion of static cosensitization of paths which leads to necessary and sufficient conditions for determining the truth or falsity of a single path, or a set of paths. The authors apply these results to develop a delay computation algorithm that has the unique feature that it is able to determine the truth or falsity of entire sets of paths simultaneously. This algorithm uses conventional stuck-at-fault testing techniques to arrive at a delay computation method that is both correct and computationally practical, even for particularly difficult circuits.>

Delay computation in combinational logic circuits is complicated by the existence of unsensitizable (false) paths and this problem is arising with increasing frequency in circuits produced by high-level synthesis procedures. Various sensitization conditions have been proposed in the past to eliminate false paths in logic circuits, but the authors use a recently developed single-vector condition, that is known to be necessary and sufficient for a path to be responsible for the delay of a circuit (i.e., true) in the floating delay model. They build on this theory and develop an efficient and correct delay computation algorithm, for the floating mode delay. The algorithm uses a technique called timed-test generation and can be incorporated into any stuck-at fault test generation framework. The authors describe in detail an implementation of the timed-test generation algorithm that uses both logical and timed forward/backward implication and backtrace procedures to simultaneously prove the truth or falsity of sets of paths in the circuit. Logical and temporal conflict detection during implication and backtrace are used to speed up the algorithm. Unlike previous techniques, the algorithm remains highly efficient: even when a large number of distinct gate and path delays exist in the given circuit.>

The problem of minimizing the cycle time of a given pipelined circuit is considered. The idea of simultaneous retiming and resynthesis is used to optimize a pipelined circuit to meet a given cycle time. An instance of the pipelined cycle optimization problem is specified by the circuit, a set of input arrival times relative to the clock, a set of required output times relative to the clock, and a given cycle time that it must meet. Given the instance of the pipelined performance optimization problem, the authors construct an instance of a combinational speedup problem. This is specified by a combinational logic circuit, a set of arrival times on the inputs, and a set of required times for the outputs which must be met. A constructive proof that the pipelined problem has a solution if and only if the combinational problem has a solution is given. This result shows that it is enough to consider only the combinational speedup problem, and all known techniques for that can be directly applied to generate a solution for the pipelined problem.>

Efficient methods for computing an exact probability distribution of the delay of a combinational circuit, given probability distributions for the gate and wire delays, are developed. The derived distribution can give the probability that a combinational circuit will achieve a certain performance, across the possible range. This information can then be used to predict the expected performance of the entire circuit. The techniques presented target fast analysis as well as reduced memory requirements. The notion of a correct approximation, based on convex inequality, which never overestimates the percentage of circuits that will achieve any given performance is defined. It is shown that given the assumption that all the topologically longest paths are responsible for the delay, the computation technique provides a correct probabilistic measure in the sense given above. Methods are given to identify and to ignore false paths in the probabilistic analysis, so as to obtain correct and less pessimistic answers to the performance prediction question. Some practical results are given for a number of benchmark combinational circuits.>

It is shown how the notion of false paths, traditionally defined for combinational logic circuits, can be extended to the sequential context by considering the operation of the circuit over multiple clock-cycles. Multicycle false paths can be removed from the circuit using techniques similar to those proposed for combinational logic circuits. This observation offers techniques to improve the performance of sequential logic circuits. A preliminary implementation of an algorithm that uses these ideas shows significant performance improvement on some typical benchmark circuits at a very modest area overhead.>

The problem of verifying that the gate-level implementation of an asynchronous circuit, with given or extracted bounds on wire and gate delays, is equivalent to a specification of the asynchronous circuit behavior described as a classical flow table, under the fundamental mode of operation, is considered. A procedure for extracting the complete set of possible flow tables from a gate-level description of an asynchronous circuit under the bounded wire delay model is given. Given an extracted flow table and the initial flow table specification, procedures for constructing a product flow table so as to check for machine equivalence are discussed.>

The authors develop efficient methods for computing an exact probability distribution of the delay of a combinational circuit, given probability distributions for the gate and wire delays. The derived distribution can give the probability that a combinational circuit will achieve a certain performance, across the possible range. The techniques target fast analysis as well as reduced memory requirements. The authors define a notion of falsity of paths when dealing with probability distributions on gate and wire delays, and they give methods for identifying and ignoring false paths in their probabilistic analysis, so as to obtain correct and accurate answers to the performance prediction question. Some results and comparisons are given for a number of combinational circuit benchmarks.>

Techniques for the optimization of multilevel logic with multiple-valued input variable is presented. The motivation for this is to tackle the input encoding problem in logic synthesis, where binary codes must be found for the different values that a symbolic input variable can take. It is shown how the other multilevel optimization techniques are easily extended with multiple-valued variables. These ideas have been implemented as algorithms in the program MIS-MV. The practical issues involved in the implementation of these ideas are discussed, and results of using MIS-MV for input encoding on benchmark examples presented.>

Becauseof its inherent complexity, the problem Multifault Compaction forFlattenable Circuits 3.1

The authors provide necessary and sufficient conditions for a path to be true in the floating mode of operation. Static cosensitization is introduced as a necessary condition, which allows one to avoid the problem of identifying false paths as responsible for delay. The results are extended to determine the truth or falsity of entire sets of paths simultaneously by expressing them in terms of the testability of a multifault in an ENF (equivalent normal form) expression. This result is applied directly to an unmodified multilevel circuit. Because the circuits that are most troublesome for false-path-eliminating static timing analyzers are those with millions of paths, and in particular millions of longest paths, the ability to handle entire sets of paths simultaneously results in a very efficient delay computation procedure. This is demonstrated by the results from a preliminary implementation of the algorithm.>

The question of whether single stuck-at-fault redundancies are necessary to increase performance or whether they are only an unnecessary by-product of performance optimization is addressed. A constructive resolution of this question is given in the form of an algorithm that takes as input a combinational circuit and returns an irredundant circuit that is as fast. The utility of this algorithm is demonstrated on a well-known circuit, the carry-skip adder, and a novel irredundant design of that adder is presented. As the algorithm may either increase or decrease circuit area, the authors leave unresolved the question as to whether every circuit has an irredundant circuit that is at least as fast and is of equal or lesser area.>

Sequential networks contain combinational logic blocks separated by registers. Application of combinational logic minimization techniques to the separate logic block results in improvement that is restricted by the placement of the registers; information about logical dependencies between blocks separated by registers is not utilized. Temporarily moving all the registers to the periphery of a network provides the combinational logic minimization tools with a global view of the logic. A technique is proposed for optimizing a sequential network by moving the registers to the boundary of the network using an extension of retiming, resynthesizing the combinational logic between the registers using existing logic minimization techniques, and replacing the registers throughout the network using retiming algorithms.>

Logic optimization procedures principally attempt to optimize three criteria: performance, area and testability. The relationship between area optimization and testability has recently been explored. As to the relationship between performance and testability, experience has shown that performance optimizations can, and do in practice, introduce single stuck-at-fault redundancies into designs. Are these redundancies necessary to increase performance or are they only an unnecessary byproduct of performance optimization? In this paper we give a constructive resolution of this question in the form of an algorithm that takes as input a combinational circuit and returns an irredundant circuit that is as fast. We demonstrate the utility of this algorithm on a well known circuit, the carry-skip adder, and present a novel irredundant design of that adder. As our algorithm may either increase or decrease circuit area, we leave unresolved the question as to whether every circuit has an irredundant circuit that is at least as fast and is of equal or lesser area.

Techniques are presented for the optimization of multi-level logic with multiple-valued input variables. The motivation for this is to tackle the input encoding problem in logic synthesis, where binary codes need to be found for the different values of a symbolic input variable. Multi-level multiple-valued optimization is used to generate constraints that are used to determine the codes. The state assignment problem in sequential logic synthesis can be approximated as an input encoding problem by ignoring the next state field, which is reasonable when the primary output logic, dominates the next state logic. A novel technique is presented for extracting common factors with multiple-valued variables, and it is shown how other multi-level optimization techniques are easily extended with multiple-valued variables. These ideas have been implemented as algorithms in the MIS-MV program. Practical issues are also presented regarding implementation. Experimental results are also given.>

The problem of minimizing the cycle time of a given pipelined circuit is considered. Existing approaches are sub-optimal since they do not consider the possibility of simultaneously resynthesizing the combinational logic and moving the latches using retiming. In the work of S. Malik et al. (Proc. of the Hawaii Inter. Conf. on System Sciences, 1990) the idea of simultaneous retiming and resynthesis was introduced. The authors use the concepts presented in that work to optimize a pipelined circuit to meet a given cycle time. Given an instance of the pipelined performance optimization problem, an instance of a combinational speedup problem is constructed. A constructive proof is given that the pipelined problem has a solution if and only if the combinational problem has a solution. This result is significant since it shows that it is enough to consider only the combinational speedup problem and all known techniques for that domain can be directly applied to generate a solution for the pipelined problem.>

An investigation was made of the analogous graph structure for representing and manipulating discrete variable problems. The authors define the multi-valued decision diagram (MDD), analyze its properties (in particular prove a strong canonical form) and provide algorithms for combining and manipulating MDDs. They give a method for mapping an MDD into an equivalent BDD (binary decision diagram) which allows them to provide a highly efficient implementation using the previously developed BDD packages. A direct implementation of the MDD structure has also been carried out, but this initial implementation has not yet been tuned to the same extent as the BDDs to allow a reasonable comparison to be made. The authors have used the mapping to BDDs to provide an initial understanding of the limits on the sizes of real problems that can be executed. The results are encouraging.>

The results of a formal logic verification system implemented as part of the multilevel logic synthesis system MIS are discussed. Combinational logic verification involves checking two networks for functional equivalence. Techniques that flatten networks or use cube enumeration and simulation cannot be used with functions that have very large cube covers. Binary decision diagrams (BDDs) are canonical representations for Boolean functions and offer a technique for formal logic verification. However, the size of BDDs is sensitive to the variable ordering. Ordering strategies based on the network topology are considered. Using these strategies with BDDs, it has been possible to carry out formal verification for a larger set of networks than with existing verification systems. The present method proved significantly faster on the benchmark set of examples tested.>