Memory access errors remain one of the most pervasive bugs in GPU programming. Existing GPU sanitizers such as compute-sanitizer detect memory access errors by instrumenting every memory instruction in low-level IRs or binaries, which imposes high overhead and provides minimal memory access error diagnostic context for fixing problems. We present Triton-Sanitizer, the first device-agnostic memory sanitizer designed for Triton, a domain-specific language for developing portable, efficient GPU kernels for deep learning workloads. Triton-Sanitizer leverages Triton's tile-oriented semantics to construct symbolic expressions for memory addresses and masks, verifies them with an SMT solver, and selectively falls back to eager simulation for indirect accesses. This hybrid analysis enables precise detection of memory access errors without false positives while avoiding the cost of per-access instrumentation. Beyond detection, Triton-Sanitizer generates rich diagnostic reports that attribute violations to the tensors nearest to the violated addresses, track the complete call path, and expose the symbolic operations responsible for incorrect addresses. Evaluated on seven widely used open-source repositories of Triton kernels, Triton-Sanitizer uncovered 24 previously unknown memory access errors, of which 8 have already been fixed and upstreamed by us. Compared to compute-sanitizer, Triton-Sanitizer achieves speedups ranging from 1.07× to 14.66×, with an average improvement of 1.62×, demonstrating its ability to enhance performance, precision, and usability in memory access error detection.

In this paper, we propose Mercury, a multi-GPU operator compiler based on a loop-based intermediate representation, CommIR. At the core of Mercury is an abstraction that treats remote GPU memory as an explicitly managed extension of the memory hierarchy, expanding the available storage and communication resources beyond local HBM. This unified view enables the compiler to reason holistically about data placement and inter-device communication, unlocking a vastly larger design space that encompasses and extends beyond existing manual strategies. As a result, Mercury is able to automatically reproduce the performance of hand-optimized baselines like RingAttention and Ulysses, and in some configurations, even discovers more effective strategies that manual designs have overlooked. Our implementation is open-sourced at https://github.com/ChandlerGuan/mercury_artifact.

Deep Learning (DL) techniques have been widely deployed in many application domains. The growth of DL models’ size and complexity demands distributed training of DL models. Since DL training is complex, software implementing distributed DL training is error-prone. Thus, it is crucial to test distributed deep learning software to improve its reliability and quality. To address this issue, we propose adifferentialtesting technique—D3, which leverages adistributedequivalence rule that we create to test distributeddeeplearning software. The rationale is that the same model trained with the same model input under different distributed settings should produce equivalent prediction output within certain thresholds. The different output indicates potential bugs in the distributed deep learning software. D3automatically generates a diverse set of distributed settings, DL models, and model input to test distributed deep learning software. Our evaluation on two of the most popular DL libraries, i.e., PyTorch and TensorFlow, shows that D3detects 21 bugs, including 12 previously unknown bugs.

Since Deep Learning (DL) libraries undergo rapid development with thousands of lines of code changes daily, they require continuous testing to detect software bugs and ensure code quality. In this paper, we explore DL testing approaches in a continuous testing setting. To make it feasible, we present the first continuous testing framework for DL libraries-CEDAR-that integrates two state-of-the-art DL testing approaches (DocTer and EAGLE) efficiently to test two popular DL libraries, PyTorch and TensorFlow. Through the application of CEDAR to 20 versions of PyTorch and TensorFlow, CEDAR detects 83 bugs in 140 APIs. Out of the 83 bugs, 23 are previously unknown bugs with 21 confirmed or fixed by the developers. The results also show CEDAR has effectively shortened the bug detection latency by almost a year (338.6 days) on average. In addition, CEDAR demonstrates its effectiveness in detecting new regression bugs and masked bugs. With three optimization strategies, CEDAR reduces the time and space overhead by a factor of 15.4 and 9.7. We share insights and lessons learned from our research, aiming to advance the development of more effective and efficient continuous testing for DL libraries, benefiting both developers and researchers.

Voice over IP (VoIP) gains more and more attractiveness by large companies as well as private users. Therefore, the risk increases that VoIP systems get attacked by hackers. In order to effectively protect VoIP users from misuse, researchers use, e.g., honeynets to capture and analyze VoIP attacks occurring in the Internet. Global VoIP security threats are analyzed by studying several millions of real-world attacks collected in independent VoIP honeynet solutions with different capture mechanisms over a long period of time. Due to the validation of results from several honeynet designs we have achieved a unique, much broader view on large scale attacks. The results show similar attacker behavior, confirm previous assumptions about attacks and present new insights in large scale VoIP attacks, e.g., for toll fraud.

VoIP systems, based on the Session Initiation Protocol (SIP), are becoming more and more widespread in the Internet. However, this creates security issues and opens up new opportunities for misuse and fraud. The most widespread threat are multi-stage attacks to commit Toll Fraud. To devise effective countermeasures, it is crucial to know how attacks on these systems are performed in reality. In this paper, we introduce a novel distributed monitoring system with Sensor nodes located in Norway, Germany and China that allow to detect SIP-based attacks from the Internet. Based on experiences from experiments spanning several years, we propose a new setup which allows simple and straightforward addition of new remote observation points. We have deployed this setup in the NorNet testbed and highlight its advantages compared to a previous setup with physically distributed Sensors. We also present results from a 45 day field test with 13 observation points. These results confirm the advantages of a widely distributed monitoring setup and give some new insights into the behavior of the attackers.

Modern CMOS manufacturing processes have significant variability, which necessitates guard banding to achieve reasonable yield. We study an FPGA architecture with a dual voltage supply wherein the supply voltage for individual CLBs can be assigned after fabrication; this yields a mechanism for fixing chips that fail because of manufactured transistors being slower than designed. The fundamental advance our work makes is that we assign voltages based on manufactured data rather than designed values. The key contributions of our work are a CAD methodology and a detailed quantitative study using realistic data on the latest process technologies of the impact of post-manufacturing tuning on yield and power for dual-Vdd FPGAs. We find that, for a representative modern process, post-manufacturing tuning can increase the yield by up to 10 × compared with a conventional dual-Vdd design that selects the voltage supply pre-manufacturing, even with guard banding. Overall, the geometric mean of yield/power ratio is 27% greater using post-manufacturing tuning.

We consider the problem of optimal netlist simplification in the presence of constraints. Because constraints restrict the reachable states of a netlist, they may enhance logic minimization techniques such as redundant gate elimination which generally benefit from unreachability invariants. However, optimizing the logic appearing in a constraint definition may weaken its state-restriction capability, hence prior solutions have resorted to suboptimally neglecting certain valid optimization opportunities. We develop the theoretical foundation, and corresponding efficient implementation, to enable the optimal simplification of netlists with constraints. Experiments confirm that our techniques enable a significantly greater degree of redundant gate elimination than prior approaches (often greater than 2x), which has been key to the automated solution of various difficult verification problems.

SRAMs typically represent half of the area and more than half of the transistors on a chip today. Variability increases as feature size decreases, and the impact of variability is especially pronounced on SRAMs since they make extensive use of minimum sized devices. Variability leads to a large amount of guard banding in the design phase in order to meet frequency and yield targets. We develop an SRAM architecture that eliminates guard banding. Specifically, our SRAM uses multiple supply voltages that are assigned post-manufacturing. We compensate for variation by powering up manufactured devices that are slower than designed. Specifically, we assign supply voltages to 6T cells on a per-column basis; this gives us sufficiently fine-grained control over devices without excessive area overhead. We show that post-manufacturing voltage assignment results in a 28% reduction in bitline energy compared to a fixed voltage design for the same yield using data from a real-world 45 nm process.

Embedded systems typically consist of a composition of a set of hardware and software IP modules. Each module is heavily optimized by itself. However, when these modules are composed together, significant additional opportunities for optimizations are introduced because only a subset of the entire functionality is actually used. We propose COSE-a technique to jointly optimize such designs. We use symbolic execution to compute invariants in each component of the design. We propagate these invariants as constraints to other modules using global flow analysis of the composition of the design. This captures optimizations that go beyond, and are qualitatively different than, those achievable by compiler optimization techniques such as common subexpression elimination, which are localized. We again employ static analysis techniques to perform optimizations subject to these constraints. We implemented COSE in the Metropolis platform and achieved significant optimizations using reasonable computational resources.

This paper examines the use of a switch based architecture to implement a Radix-2 decimation in frequency fast Fourier transform engine. The architecture interconnects M processing elements with 2*M memories. An algorithm to detect and resolve memory access contention is presented. The implementation of 1024-point FFTs with 2 processing elements is discussed in detail, including timing and place-and-route results. The switch based architecture provides a factor of M speedup over a single processing element realization.

The alloy tool-set has been gaining popularity as an alternative to traditional manual testing and checking for design correctness. Alloy uses a first-order relational logic for modeling designs. The alloy analyzer translates alloy formulas for a given scope, i.e., a bound on the universe of discourse, to Boolean formulas in conjunctive normal form (CNF), which are subsequently checked using prepositional satisfiability solvers. We present SERA, a novel algorithm that compiles a relational logic formula for a given scope to a sequential circuit. There are two key advantages of sequential circuits: they form a more succinct representation than CNF formulas, sometimes by several orders of magnitude. Also sequential circuits are amenable to a range of powerful automatic analysis techniques that have no counterparts for CNF formulas. Our experiments show that SERA, used in conjunction with a sequential circuit analyzer, can check formulas for scopes that are an order of magnitude higher than those feasible with the alloy analyzer.

A number of researchers have proposed the use of Boolean satisfiability solvers for verifying C programs. They encode correctness checks as Boolean formulas using finitization: loops and recursion are bounded, as is the size of the input instances. The SAT approach has been shown to find subtle bugs with reasonable resources. However, it does not scale well; in particular, it lacks the ability to handle larger bounds. We present SEBAC, which can handle the same class of programs as the SAT approach, and scales to bounds that are orders of magnitude higher. The key difference between SEBAC and SAT techniques is SEBAC's use of imperative Boolean sequential circuits, which are Boolean formulas with memory elements instead of the Boolean formulas which are stateless

Many DSP algorithms are very computationally intensive. They are typically implemented using an ensemble of processing elements (PEs) operating in parallel. The results from PEs need to be communicated with other PEs, and for many applications the cost of implementing the communication between PEs is very high. Given a DSP algorithm with high communication complexity, it is natural to use a network-on-chip (NoC) to implement the communication. We address two key optimization problems that arise in this context - placement, i.e., assigning computations to PEs on the NoC, and scheduling, i.e., constructing a detailed cycle-by-cycle scheme for implementing the communication between PEs on the NoC

This paper examines the superscalar pipeline Fast Fourier Transform algorithm and architecture. The algorithm presents a memory management scheme to prevent memory contention throughout the pipeline stages. The fundamental algorithm, a switch-based FFT pipeline architecture and an example 64-point FFT pipeline are presented. The proposed superscalar architecture substantially improves the FFT processing. The pipeline consists of log2N stages, where N is number of FFT points. Each stage can have M Processing Elements (PEs.) As a result, the architecture speed up is M*log2N. The pipeline algorithm is configurable to any M ≫ 1.

State-equivalence based reduction techniques, e.g. bisimulation minimization, can be used to reduce a state transition system to facilitate subsequent verification tasks. However, the complexity of computing the set of equivalent state pairs often exceeds that of performing symbolic property checking on the original system. We introduce a fully-automated efficient compositional minimization approach which requires only static analysis. Key to our approach is a heuristic algorithm that identifies components with high reduction potential in a bit-level netlist. We next inject combinational logic which restricts the component's inputs to selected representatives of symbolically-computed equivalence classes thereof. Finally, we use existing transformations to synergistically exploit the dramatic netlist reductions enabled by these input filters. Experiments confirm that our technique is able to efficiently yield substantial reductions on large industrial netlists.

Error correcting codes are widely used in communication and storage applications. Codec complexity has usually been measured with a software implementation in mind. A recent hardware implementation of a Low Density Parity Check code (LDPC) indicates that interconnect complexity dominates the VLSI cost. We describe a heuristic interconnect-aware synthesis algorithm which generates LDPC codes that use an order of magnitude less wiring with little or no loss of coding efficiency.

We present new results and numerical studies of very fast schedulers for SMS (switch-memory-switch) routers, which emulate output-queuing by buffering packets in a partitioned shared-memory located between input and output ports. The architecture of Juniper's core routers and Brocade's storage switches is based on SMS. Our numerical results demonstrate that RiPSS, a randomized highly parallel SMS scheduler that we had developed recently, runs in just 3 rounds on switches with up to 4,096 inputs, and has a very low drop probability. We also show that RiPSS makes effective use of the shared-memory, with packets being uniformly distributed across the memory hanks for both Bernoulli and bursty arrivals. We describe a new and improved randomized pipelined scheduler, PRiPSS, and analyze its performance. Both our analysis and our simulation results for PRiPSS show that it has better throughput than RiPSS with a slightly higher latency in terms of rounds of communication in the underlying hardware. Our analysis also shows that PRiPSS is self-stabilizing, i.e., if occasional lapses occur due to the probabilistic nature of the algorithm, it resumes normal behavior without the need for external intervention. While the choice of RiPSS or PRiPSS would depend on whether throughput or latency is the primary concern, our results indicate that both schedulers are much faster than other schedulers for output-queuing, whether implemented directly or through emulation on SMS

Simulation by random vectors is meaningful only if the vectors meet certain requirements on the environment that drives the design under verification. When that environment is modeled by constraints, we face the problem of solving constraints efficiently. We present an efficient algorithm for simplifying conjunctive Boolean constraints defined over state and input variables, and apply it to constrained random simulation vector generation using binary decision diagrams (BDDs). The method works by extracting "hold-constraints" from the system of constraints. Hold-constraints are deterministic and trivially resolvable. They can be used to simplify the original constraints as well as refine the conjunctive partition. Experiments demonstrate significant reductions in the time and space required for constructing the conjunction BDDs, and the time spent in vector generation during simulation.

Modeling design environment with constraints instead of a traditional testbench is advantageous in a hybrid verification framework that encompasses simulation and formal verifica-tion. This movement is gaining popularity in industry and sparks research in the constraint-based environment mod-eling and stimulus generation problem. We present an ap-proach, called constraint synthesis, to this problem. Con-straint synthesis falls in the general category of parametric Boolean equation solving but is novel in utilizing don’t care information unique to hardware constraints and heuristic variable removal to simplify the solution. Experimental re-sults have demonstrated the effectiveness of the proposed approach.

We present a simple and near optimal randomized parallel scheduling algorithm for scheduling packets in routers based on the Switch-Memory-Switch (SMS)architecture, which emulates 'output queuing' by using a collection of small memories within the switch to buffer packets, and which forms the basis of the fastest routers in use today. For a router with N inputs and N outputs, our algorithm computes the schedule in O(log* N) rounds, where a round is a communication of a few bits between input ports and memory together with simple local computation at the inputs and memory. Furthermore, by using an O(log* N) deep pipeline at each input, our algorithm computes the schedule in a constant number of rounds. Our pipelined algorithm is quite simple and achieves optimal (i.e.,constant) throughput with a tiny O(log* N) delay.We show that the total amount of buffer memory required by our algorithm is close to the minimum required. We also show that the number of buffer memories is within an εN additive term of 2N -- 1, for any positive constant ù>0 (and is within an additive term of o(N)for the basic scheduler), where 2N -- 1 is the minimum number of memories needed under adversarial placement of packets. Furthermore we show that the number of extra memories that we use over the minimum of N that is required in the offline version, is within a constant factor of the minimum required by any on-line scheduler, even if that scheduler is allowed to fail occasionally.Our scheduling algorithm is randomized and works with high probability in N. We also prove that it has the 'self-stabilizing' property, i.e., it resumes its normal behavior if occasional lapses occur due to the probabilistic nature of the algorithm.

Packet classification is a computationally intensive task that routers need to perform in order to implement basic functions such as next-hop lookup, as well as advanced features such as quality of service and security. Formally, a classifier examines each incoming packet, and determines which rules to apply to it. Semantically, the classifier is characterized by a function mapping the packet header to an integer encoding the action to be taken for that packet. The function itself is syntactically presented as a chain of if-then-else statements. Since the header consists of a fixed number of bits, it is natural to use logic synthesis to implement fast small classifiers in hardware. When doing this, there are two key issues that must be kept in mind: 1) these functions change over time, so the target architecture needs to be reconfigurable and 2) classification functions have a structure which should be exploited. We show that Internet Protocol forwarding, which is a special case of classification, can be performed by provably small circuits at very high speed by mapping the binary decision diagram (BDD) representation of the classification function to a cascaded array of lookup tables. This approach does not immediately carry over to general packet classification; the BDD for the classification function grows very large. We develop a solution based on partitioning to overcome this problem. We prove NP-completeness of optimal partitioning. We describe a heuristic for partition. The latency introduced by pipelining can be reduced by partially collapsing the BDD. We present an efficient algorithm based on dynamic programming to obtain an optimum grouping of variables that minimizes the total amount of memory required for a given number of levels.

We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and consequently a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We review the concept of safe replaceability which does away with these assumptions and the delay-safe replaceability notion, which is applicable when the design's output is not used for a certain number of cycles after power-up. We then develop procedures for optimizing the combinational next-state and output logic, as well as routines for reencoding the state space and removing state bits under these replaceability criteria. Experimental results demonstrate the effectiveness of our algorithms.

We present an algorithm for simplifying the solution of conjunctive Boolean constraints of state and input variables, in the context of constrained random vector generation using BDDs. The basis of our approach is extraction of "hold-constraints" from constraint system. Hold-constraints are deterministic and trivially resolvable; in addition, they can be used to simplify the original constraints as well as refine the conjunctive partition. Experiments demonstrate significant reduction in the time and space needed for constructing the conjunction BDDs, and the time spent in vector generation during simulation.

Output queued switches are appealing because they have better latency and throughput than input queued switches. However, they are difficult to build: a direct implementation of an N/spl times/N output-queued switch requires the switching fabric and the packet memories at the outputs to run at N times the line rate. Attempts have been made to implement output queuing with slow components, e.g., by having memories at both inputs and outputs running at twice the line rate. In these approaches, even though the packet memory speed is reduced, the scheduler time complexity is high - at least /spl Omega/(N). We show that idealized output queuing can be simulated in a shared memory architecture with (3N-2) packet memories running at the line rate, using a scheduling algorithm whose time complexity is O(log/sup 2/ N) on a parallel random access machine (PRAM). The number of processing elements and memory cells used by the PRAM are a small multiple of the size of the idealized switch.

One of the most challenging issues in today's high-performance VLSI design is to ensure high-quality power supply to each individual circuit blocks. Reduced power supply voltage can result in slower cell switching, or even circuit failure. Nevertheless, most floorplanning methodologies have ignored power supply considerations. Thus, the resulting floorplan may suffer from local hot spots and insufficient power supply for certain circuit blocks. In this paper, we present an optimal power supply planning algorithm based on network flow to shorten the current paths from power bumps to local power supply wirings. We have incorporated our algorithm into a floorplanning algorithm for integrated floorplanning and power supply planning. Experimental results are encouraging.

State explosion is a common problem when verifying large designs. Partial state exploration using guided techniques has become a subject of wide research. We propose a rarity-based metric for state prioritization and several techniques which use the metric for enhanced state space search. These techniques use latch toggle activity and latch support for partitioning the design. The computation overhead for these techniques is minimal. Coverage results on the large industrial designs show the effectiveness of our approach.

We develop algorithms for exploring the reachable state-space of hardware designs that can be partitioned into control and data. The core procedure is a symbolic algorithm that tries to visit as many controller states as is computationally feasible. Here, we describe heuristics for making this traversal efficient. Experiments demonstrate that our approach is capable of achieving significantly greater coverage of the control state-space than conventional symbolic reachability analysis.

We address the problem of developing suitable criteria for design replacement in the context of sequential logic synthesis. There have been previous efforts to characterize replacements for such designs. However, all previous attempts either make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and, consequently, a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We present the notion of safe replaceability, which does away with these assumptions, and prove a number of properties that hold of it. Most importantly, we show that the notion is sound, i.e., if design D/sub 1/ is a safe replacement for design D/sub 0/, then no environment can determine if D/sub 1/ is used in place of D/sub 0/ and that the notion is complete, i.e., if D/sub 1/ is not a safe replacement for D/sub 0/ then there exists an environment that can detect if D/sub 1/ is used in place of D/sub 0/. Completeness is important for logic synthesis and verification because it specifies the maximum allowable flexibility for replacement. When the design's output is not used for a certain number of cycles after power up, then safe replaceability can be relaxed to obtain what we refer to as delay safe replaceability; we analyze properties of this notion too. Since our work, many papers have used this notion effectively for sequential optimization.

With shrinking feature sizes and increasing transistor counts on chips, demands for higher speed and lower power make it necessary to look for alternative design styles that offer better performance than static complementary metal-oxide-semiconductors. Among them, pass transistor logic (PTL) is of great promise. Since delay in a transistor chain is quadratically proportional to the number of transistors and a signal may degenerate passing through a transistor, buffers are necessary to guarantee performance and restore signal strength in PTL circuits. In this paper, we first analyze effects of buffer insertion on a circuit and give a sufficient and necessary condition for safe buffer insertion. Then, a buffer minimization problem is formulated. Although it is NP-hard in general, it can be solved linearly when buffers are required on multifan-out nodes. We also consider the case when buffers are inverters, where phase assignment needs to be done with buffer insertion.

We are concerned with optimizing gate-level netlists containing “black boxes,” that is, components whose functionality is not available to the optimization tool. We establish a notion of equivalence for gate-level netlists containing black boxes, and prove that it is sound and complete. We show that conventional approaches to optimizing such netlists fail to fully exploit the don't care flexibility available for synthesis. Based on our new notion of equivalence, we introduce a procedure that computes the complete don't care set. Experiments indicate that our procedure can achieve more minimization than conventional synthesis.

We address the problem of inserting repeaters, selected from a library, at feasible locations in a placed and routed network to meet user-specified delay constraints for deep submicron (DSM) technology. We use minimal repeater area by taking advantage of slacks available in the network. Specifically, we transform the problem into an unconstrained optimization problem and solve it by iterative local refinement. We show that the optimal repeater locations and sizes that locally minimize the objective function in the unconstrained problem can be efficiently computed. We have implemented our algorithm and tested it on a set of benchmarks; experimental results are promising.

Previous researchers have suggested the use of "lighthouses" to act as guides in directed state space search. The drawback of using lighthouses is that the user has to manually, derive them, through a potentially laborious examination of the design. Additionally specifying a large number of lighthouses results in wasted effort during the search. We present approaches to automatically generate high-quality lighthouses for hard-to-cover targets.

We present a novel algorithm for delay constrained optimization of combinational logic, extending the state-of-the-art sizing algorithm based on Lagrangian relaxation. We tightly integrate fanout tree construction, buffer insertion/sizing and gate sizing, thereby achieving more optimization than if they were performed independently. We consider the network in its entirety, thereby taking full advantage of the slacks available on the noncritical paths. We have implemented our algorithm and experimented with it on ISCAS-89 benchmark circuits; the results demonstrate that it is effective as well as fast.

We propose an integrated clock tree construction algorithm which performs simultaneous routing, wire sizing and buffer insertion.In existing approaches, wire sizing and clock buffer insertion are typically applied sequentially after a clock tree is generated and routed, i.e., they are done as post-processing steps.None of the known methods can perform clock routing while simultaneously considering wire sizing and buffer insertion.We introduce wire widths and levels of buffers inserted as variables in forming merging segments in the proposed Integrated Deferred-Merge Embedding (IDME) algorithm.As a result, more zero-skew merging locations are made possible and the clock trees generated are zero-skew by construction.Our experiments show that by taking the advantage offered by wire sizing, we are able to minimize phase delay as well as to reduce wire length and use less buffers.

Since the technical limits of existing circuit families, such as static CMOS, alternative circuit families are pursued for the development of chips that can operate at speeds significantly above 500 MHz. Among them, pass transistor logic (PTL) circuits offer great promise. Since the delay in a pass-transistor chain is quadratically proportional to its length, and a signal may degenerate when pass through a transistor, buffers are necessary to guarantee the performance and restore the signals in PTL. In this paper, we first analyze the effects of buffer insertion on a circuit and give the sufficient and necessary condition for safe buffer insertion. Then the buffer minimization problem is formulated, which asks for a minimum number of buffers to make sure that no path has length longer than a given upper bound. Although NPhard generally, when buffers are required on multiple fan-outs, it can be solved linearly. We also consider the case when buffers are inverters, where phase assignment...

We propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant solutions to problems arising in the synthesis and optimization of synchronous digital hardware. Specifically, we derive a logical expression which yields a single finite state automaton characterizing the set of implementations that can replace a component of a larger design. The power of our approach is demonstrated by the fact that it generalizes immediately to arbitrary interconnection topologies, and to designs containing nondeterminism and fairness. We also describe control aspects of sequential synthesis and relate controller realizability to classical work on program synthesis and tree automata.

During the routing of global interconnects, macro blocks form useful routing regions which allow wires to go through but forbid buffers to be inserted. They give restrictions on buffer locations. In this paper, we take these buffer location restrictions into consideration and solve the simultaneous maze routing and buffer insertion problem. Given a block placement defining buffer location restrictions and a pair of pins (a source and a sink), we give a polynomial time exact algorithm to find a buffered route from the source to the sink with minimum Elmore delay.

We present a logical formalism for expressing properties of continuous-time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete-time Markov chains to continuous time. The major result is that the verification problem is decidable; this is shown using results in algebraic and transcendental number theory.

We introduce Simulation Verification with Augmentation (SIVA), a tool for checking safety properties on digital hardware designs.SIVA integrates simulation with symbolic techniques for vector generation.Specifically, the core algorithm uses a combination of ATPG and BDDs to generate input vectors which cover behavior not excited by simulation.Experimental results demonstrate considerable improvement in state space coverage compared with either simulation or formal verification in isolation.

Article Free Access Share on Simultaneous routing and buffer insertion with restrictions on buffer locations Authors: Hai Zhou Department of Computer Sciences, University of Texas, Austin, TX Department of Computer Sciences, University of Texas, Austin, TXView Profile , D. F. Wong Department of Computer Sciences, University of Texas, Austin, TX Department of Computer Sciences, University of Texas, Austin, TXView Profile , I-Min Liu Department of Electrical and Computer Engineering, University of Texas, Austin, TX Department of Electrical and Computer Engineering, University of Texas, Austin, TXView Profile , Adnan Aziz Department of Electrical and Computer Engineering, University of Texas, Austin, TX Department of Electrical and Computer Engineering, University of Texas, Austin, TXView Profile Authors Info & Claims DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation ConferenceJune 1999 Pages 96–99https://doi.org/10.1145/309847.309885Published:01 June 1999Publication History 44citation315DownloadsMetricsTotal Citations44Total Downloads315Last 12 Months43Last 6 weeks8 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

Constraining and input biasing are frequently used techniques in functional verification methodologies based on randomized simulation generation. Constraints confine the simulation to a legal input space, while input biasing, which can be considered as a probabilistic constraint, makes it easier to cover interesting "corner" cases. In this paper, we propose to use constraints and biasing to form a simulation environment instead of using an explicit testbench in hierarchical functional verification. Both constraints and input biasing can depend on the state of the design and thus are very expressive in modeling the environment. We present a novel method that unifies the handling of constraints and biasing via the use of Binary Decision Diagrams (BDDs). The distribution of input vectors under the effect of constraints and input biasing are determined by what we refer to as the constrained probabilities. A BDD representing the constraints is first built, then an algorithm is applied to bias the branching probabilities in the BDD. During simulation, this annotated BDD is used to generate input vectors whose distribution matches their predetermined constrained probabilities. The simulation generation is a one-pass process, i.e., no backtracking or retry is needed. Also, we describe a partitioning method to minimize the size of BDDs used in simulation generation. Our techniques were used in the verification of a set of commercial designs; experimental results demonstrated their effectiveness.

We propose a novel buffer insertion algorithm for handling more general networks, whose underlying topology is a directed acyclic graph rather than just a RC tree. The algorithm finds a global buffering which minimizes buffer area while meeting the timing constraints. We use Lagrangian relaxation to translate the timing constraints to a cost in the objective function, and simplify the resulting objective function using the special structure of the problem we are solving. The core of the algorithm is a local refinement procedure, which iteratively computes the optimal buffering for each edge so as to minimize a weighted area and delay objective. The resulting procedure is fast, and takes full advantage of the slack available on noncritical paths.

We develop a verification paradigm called saturated simulation, that is applicable to designs which can be decomposed into a set of interacting controllers. The core procedure is a symbolic algorithm that explores the space of controller interactions; heuristics for making this traversal efficient are described. Experiments demonstrate that our procedure explores substantially more of the controller interactions, and is more efficient than conventional symbolic reachability analysis.

W e implement and experiment with techniques for the functional simulation of very large digital systems. We consider techniques that are a hybrid of classical compiled code simulation and recent branching program based simulation in order to resolve memory performance problems inherent to BDD based cycle simulation. Specifically, predefined functional units (“macros”) are extracted from the circuit and evaluated directly instead of building BDDs for them. The functionality of those macros, such as multipliers, filters, etc., can in turn be verified by simulation of their gate-level implementations respectively or by formal verification techniques. Our results demonstrate that this approach leads to considerably faster simulation.

Pass Transistor Logic (PTL) circuits have been successfully used to implement digital ICs which are smaller, faster, and more energy efficient than static CMOS implementations of the same designs. Thus far, most PTL implementations have been handcrafted; as such, designer acceptance of PTL has been limited. In this paper, we develop efficient algorithms for automated synthesis of high quality PTL designs. Our approach is based on the use of Binary Decision Diagrams (BDDs) to represent logic functions. We present several BDD optimization techniques targeting minimum area PTL implementations. We compare our results with prior work on PTL synthesis; we also provide comparison between synthesized static CMOS and synthesized PTL at the layout level for control logic from a commercial microprocessor.

We define a notion of equivalence for designs containingblack boxes i.e., components whose functionality is notknown; these arise naturally in the course of hierarchicaldesign. Using this notion, we describe a sound andcomplete methodology for optimizing such designs.

We propose an algorithm for area optimisation of sequential circuits through redundancy removal. The algorithm finds compatible redundancies by implying values over nets in the circuit. The potentially exponential cost of state space traversal is avoided and the redundancies found can all be removed at once. The optimised circuit is a safe delayed replacement of the original circuit. The algorithm computes a set of compatible sequential redundancies and simplifies the circuit by propagating them through the circuit. We demonstrate the efficacy of the algorithm even for large circuits through experimental results on benchmark circuits.

We present a mathematical framework for analyzing the synthesis of interacting, finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in sequential synthesis. We obtain exact and approximate sets of permissible FSM network behavior, and address the issue of FSM realizability. This approach is also applied to synthesizing systems with fairness and timed systems.

Article Free Access Share on HSIS: a BDD-based environment for formal verification Authors: A. Aziz Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , F. Balarin Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S.-T. Cheng Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. Hojati Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. Kam Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. C. Krishnan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Ranjan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. R. Shiple Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , V. Singhal Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. Tasiran Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , H.-Y. Wang Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Brayton Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , A. L. Sangiovanni-Vincentelli Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 454–459https://doi.org/10.1145/196244.196467Published:06 June 1994Publication History 39citation325DownloadsMetricsTotal Citations39Total Downloads325Last 12 Months36Last 6 weeks17 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

We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting finite state machines (FSMs).Orderings are derived from the communication structure of the system.Communication complexity arguments are used to prove upper bounds on the size of the BDD for the transition relation of the product machine in terms of the communication graph, and optimal orderings are exhibited for a variety of regular systems.Based on the bounds we formulate algorithms for variable ordering.We perform reached state analysis on a number of standard verification benchmarks to test the effectiveness of our ordering strategy; experimental results demonstrate the efficacy of our approach.The algorithms described in this paper have been implemented in HSIS, a hierarchical synthesis and verification tool currently under development at Berkeley.

We address the problem of compositional minimization of collections of interacting finite state machines that arise in the context of formal verification of hardware designs by language containment. Typically much of the behavior of the system is redundant with respect to a given property being verified, and so the system can be replaced by substantially simpler representations. We show that these redundancies can be captured by computing states that are input-output equivalent in the presence of fairness. Since computing complete equivalences is computationally expensive, we propose a spectrum of approximations which are efficiently computable. Directly minimizing the entire system requires forming the complete product machine, which can be very large, and hence we describe procedures that hierarchically minimize the system with respect to explicit and BDD representations. We present experimental results on some standard verification examples to show that our algorithms allow the product machine to be represented by very small implicit or explicit representations. We conclude with some further directions.>