The focus of this paper is on dynamic power management in virtualized multi-core server systems. The paper starts by analyzing the effect of virtualization and CPU consolidation on power dissipation and performance (latency) of such systems, and concludes by presenting two new CPU consolidation algorithms for multi-core servers. The paper also reports an extensive set of experimental results founded on a realistic multi-core server system setup and well-developed benchmarks, i.e., SPEC2K and SPECWeb2009 and obtained through hardware measurements.

This paper presents a transactional specification framework (T-spec) for describing a datapath and the tool T-piper to synthesize automatically an in-order pipelined implementation with arbitrary user-specified pipeline-stage boundaries. T-spec abstractly views a datapath as executing one transaction at a time, computing the next system states based on the current ones. The synthesized pipeline maintains this semantics, yet allows concurrent execution of multiple overlapped transactions in different pipeline stages, where each stage performs a part of the next-state computation of each transaction. T-spec makes the state reading and writing events in a datapath explicit to enable T-piper to perform exact read-after-write (RAW) hazard analysis between the overlapped transactions. T-piper can automatically generate the pipeline control not only to ensure the correctness of the pipelined executions but also to minimize (using forwarding and speculation) the performance loss due to pipeline stalls in the presence of RAW dependencies. This paper reports design case studies applying T-spec and T-piper to reduced instruction set computing and complex instruction set computing processor pipeline development. In the latter, we report the results from a rapid design space exploration of 60 generated x86-subset pipelines, varying in pipeline depth, forwarding, and speculative execution, all starting from a single T-spec.

We present a technique to automatically synthesize a multithreaded in-order pipeline from a high-level unpipelined datapath specification. This work extends the previously proposed transactional specification (T-spec) and synthesis technology (T-piper). The technique not only works with instruction processors but also flexible enough to accept any sequential datapath. It maintains previously proposed non-threaded pipeline features and is enhanced with multithreading features. We report a design space exploration study of 32 multithreaded x86 processor pipelines, all synthesized from a single T-spec.

We present a transactional datapath specification (T-spec) and the tool (T-piper) to synthesize automatically an in-order pipelined implementation from it. T-spec abstractly views a datapath as executing one transaction at a time, computing next system states based on current ones. From a T-spec, T-piper can synthesize a pipelined implementation that preserves original transaction semantics, while allowing simultaneous execution of multiple overlapped transactions across pipeline stages. T-piper not only ensures the correctness of pipelined executions, but can also employ forwarding and speculation to minimize performance loss due to data dependencies. Design case studies on RISC and CISC processor pipeline development are reported.

This paper presents a method for correct-by-construction microarchitectural pipelining that handles cyclic systems with dependencies between iterations. Our method combines previously known bypass and retiming transformations with a few transformations valid only for elastic systems with early evaluation (namely, empty FIFO insertion, FIFO capacity sizing, insertion of anti-tokens, and introducing early evaluation multiplexors). By converting the design to a synchronous elastic form and then applying this extended set of transformations, one can pipeline a functional specification with an automatically generated distributed controller that implements stalling logic resolving data hazards off the critical path of the design. We have developed an interactive toolkit for exploring elastic microarchitectural transformations. The method is illustrated by pipelining a few simple examples of instruction set architecture ISA specifications.

This paper presents a new tool for SystemVerilog RTL modifications with on-the-fly validation of local RTL changes. The tool, SV-rewrite, imports an initial version of SystemVerilog RTL and elaborates it into a hierarchical design description visualized as structural diagrams. From the design cockpit the user can select any set of visualized components, open a favorite text editor, modify then validate the new RTL description, and finally substitute this new rewritten RTL into the larger model to replace the originally selected components. This process of local validated rewrites can be repeated until the entire RTL is safely rewritten. We studied RTL abstraction using SV-rewrite to abstract the Pentium 80602 (P54CS) integer execution unit and register file. We have produced a significantly more readable RTL that is 2 to 3 times smaller than the original one. The abstracted RTL was validated by booting Linux on an FPGA-based emulation platform.

Technology mapping, based on directed acyclic graph covering, suffers from the problem of structural bias: The structure of the mapped netlist depends strongly on the subject graph. In this paper, the authors present a new mapper aimed at mitigating structural bias. It is based on a simplified cut-based Boolean-matching algorithm, and using the speed afforded by this simplification, they explore two ideas to reduce structural bias. The first, called lossless synthesis, leverages recent advances in structure-based combinational-equivalence checking to combine the different networks seen during technology-independent synthesis into a single network with choices in a scalable manner. They show how cut-based mapping extends naturally to handle such networks with choices. The second idea is to combine several library gates into a single gate (called a supergate) in order to make the matching process less local. They show how supergates help address the structural-bias problem and how they fit naturally into the cut-based Boolean-matching scheme. An implementation based on these ideas significantly outperforms state-of-the-art mappers in terms of delay, area, and run-time on academic and industrial benchmarks

Technology mapping based on DAG-covering suffers from the problem of structural bias: the structure of the mapped netlist depends strongly on the subject graph. In this paper we present a new mapper aimed at mitigating structural bias. It is based on a simplified cut-based Boolean matching algorithm, and using the speed afforded by this simplification we explore two ideas to reduce structural bias. The first, called lossless synthesis, leverages recent advances in structure-based combinational equivalence checking to combine the different networks seen during technology independent synthesis into a single network with choices in a scalable manner. We show how cut based mapping extends naturally to handle such networks with choices. The second idea is to combine several library gates into a single gate (called a supergate) in order to make the matching process less local. We show how supergates help address the structural bias problem, and how they fit naturally into the cut-based Boolean matching scheme. An implementation based on these ideas significantly outperforms state-of-the-art mappers in terms of delay, area and run-time on academic and industrial benchmarks.

Structuring and mapping of a Boolean function is an important problem in the design of complex integrated circuits. Library-aware constructive decomposition offers a solution to this problem. This paper proposes novel techniques to improve the quality and runtime of constructive decomposition. The improvements are effective both in the stand-alone mapping procedure and in the context of re-synthesis applied to a mapped multi-level network. Experiments with public and proprietary benchmarks show promising results.

High performance microprocessor designs are partially characterized by functional blocks consisting of a large number of operations that are packed into very few cycles (often single-cycle) with little or no resource constraints but tight bounds on the cycle time. Extreme parallelization, conditional and speculative execution of operations is essential to meet the processor performance goals. However, this is a tedious task for which classical high-level synthesis (HLS) formulations are inadequate and thus rarely used. In this paper, we present a new methodology for application of HLS targeted to such microprocessor functional blocks that can potentially speed up the design space exploration for microprocessor designs. Our methodology consists of a coordinated set of source-level and fine-grain parallelizing compiler transformations that targets these behavioral descriptions, specifically loop constructs in them and enables efficient chaining of operations and high-level synthesis of the functional blocks. As a case study in understanding the complexity and challenges in the use of HLS, we walk the reader through the detailed design of an instruction length decoder drawn from the Pentium-family of processors. The chief contribution of this paper is formulation of a domain-specific methodology for application of high-level synthesis techniques to a domain that rarely, if ever, finds use for it.

Although model checking is an exhaustive formal verification method, a bug can still escape detection if the erroneous behavior does not violate any verified property.We propose a coverage metric to estimate the "completeness" of a set of properties verified by model checking.A symbolic algorithm is presented to compute this metric for a subset of the CTL property specification language.It has the same order of computational complexity as a model checking algorithm.Our coverage estimator has been applied in the course of some real-world model checking projects.We uncovered several coverage holes including one that eventually led to the discovery of a bug that escaped the initial model checking effort.

We present an automated formal verification method that can detect common pipeline-control bugs of logic-design components containing thousands of registers. The method models logic designs using controlled token nets. A controlled token net consists of: a token net that models the data flow in the datapath using token semantics; a control logic that models the control machines using traditional finite state semantics. We provide algorithms to (1) extract a controlled token net from a logic design, (2) minimize the controlled token net, and (3) compute an abstract interpretation of the controlled token net for efficient model checking. We implemented and applied the method to 6 Intel logic-design components containing up to 4500 registers and successfully detected 8 pre-silicon errata. 1.1 Keywords Pipeline control verification, controlled token net, abstract interpretation, processor verification, model checking, formal verification, functional verification, computer-aided design 2.

The computation of sets of compatibles of incompletely specified finite-state machines (ISFSMs) is a key step in sequential synthesis. This paper presents implicit computations to obtain sets of maximal compatibles, compatibles, prime compatibles, implied sets, and class sets. The computations are implemented by means of BDDs that realize the characteristic functions of these sets. We have demonstrated with experiments from a variety of benchmarks that implicit techniques allow us to handle examples exhibiting a number of compatibles up to 2/sup 1500/, an achievement outside the scope of programs based on explicit enumeration. We have shown, in practice, that ISFMSs with a very large number of compatibles may be produced as intermediate steps of logic synthesis algorithms, for instance, in the case of asynchronous synthesis. This shows that the proposed approach not only has a theoretical interest, but also practical relevance for current logic synthesis applications, as shown by its application to ISFSM state minimization.

This paper addresses state minimization problems of different classes of nondeterministic finite-state machines (NDFSMs). We describe a fully implicit algorithm for state minimization of pseudo nondeterministic FSM's (PNDFSMs). The results of our implementation are reported and shown to be superior to a previous explicit formulation. We could solve exactly all but one problem of a published benchmark, while an explicit program could complete approximately one half of the examples, and in those cases, with longer run times. Then we present a theoretical solution to the problem of exact state minimization of general NDFSMs, based on the proposal of generalized compatibles. This gives an algorithmic framework to explore behaviors contained in a general NDFSM.

We survey techniques for solving binate covering problems, an optimization step often occurring in logic synthesis applications. Standard exact solutions are found with a branch-and-bound exhaustive search, made more efficient by bounding away regions of the search space. Standard approaches are said to be explicit because they work on a direct representation of the binate table, usually as a matrix. Recently, covering problems involving large tables have been attacked with implicit techniques. They are based on the representation by reduced-ordered binary decision diagrams of an encoding of the binate table. We show how table reductions, computation of a lower bound, and of a branching column can be performed on the table so represented. We report experiments for two different applications that demonstrate that implicit techniques handle instances beyond the reach of explicit techniques. Various aspects of our original research are presented for the first time, together with a selection of the most important old and new results scattered in many sources.

This paper addresses state minimization problems of different classes of non-deterministic finite state machines (NDFSMs). We present a theoretical solution to the problem of exact state minimization of general NDFSMs, based on the proposal of generalized compatibles. This gives an algorithmic frame to explore behaviors contained in a general NDFSM. Then we describe a fully implicit algorithm for state minimization of pseudo non-deterministic FSMs (PNDFSMs). The results of our implementation are reported and shown to be superior to a previous explicit formulation. We could solve exactly all but one problem of a published benchmark, while an explicit program could complete approximately one half of the examples, and in those cases with longer run times.

This paper discusses a formal verification technique for comparing the functionality of a transistor netlist extracted from a layout with a design description in a hardware description language (HDL). Using novel techniques based on binary decision diagrams (BDD's), a state machine is first abstracted from a transistor netlist, given information relating to clock signals and clock models. The resulting state machine behavior is then compared with another that is derived from the HDL description. The basic ingredients of the technique used can be directly applied (or, in other cases, extended) to various related contexts of interest. In particular, the abstracted machine(s) can be represented as BDD relations or as synchronous sequential networks, both of which are common starting points for sequential synthesis and verification tools.>

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

Implicit computations of the solution set of optimization problems arising in logic synthesis hold the promise of enlarging the size of instances that can be solved exactly. The state minimization problem for incompletely specified machines is an important step for sequential circuit optimization. The problem is NP-hard. An exact algorithm consists of two steps: generation of sets of compatibles, and solution of a binate covering problem. This paper presents an implicit algorithm for exact state minimization of FSM's. There are various applications of logic synthesis that generate FSM's beyond the reach of state-of-art state minimization tools. Therefore it is of practical importance to revisit exact state minimization of ISFSM's and address the issue of representing implicitly the solution space. In this paper we show how to compute sets of maximal compatibles, compatibles and prime compatibles with implicit techniques and demonstrate that in this way it is possible to handle examples exhibiting a number of compatibles up to 21200, a number outside the scope of programs based on explicit enumeration [13]. We indicate also where such examples arise in practice. Then we address the final step of an implicit exact state minimization procedure, i.e. solving a binate table covering problem [24]. We present the first published algorithm for fully implicit exact binate covering. We report preliminary results of a prototype implementation capable of reducing huge binate tables (up to 106 rows and column)s and of carrying on the branch-and-bound procedure on an implicit representation of the table. Exact solutions to problems beyond the reach of traditional tools are so found

The authors discuss a formal verification technique using binary decision diagrams (BDDs) for comparing the functionality of a transistor netlist extracted from a layout with a design description in a hardware description language (HDL). A state machine is first abstracted from a transistor netlist, given information relating to clock signals and clock models. The resulting state machine behavior is then compared with another that is derived from the HDL description. The basic ingredients of the technique used can be directly applied (or, in other cases, extended) to various related contexts of interest.>

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.>