In 2015, a team of software and hardware developers at Microsoft shipped the world?s first commercial search engine accelerated using FPGAs in the datacenter. During the sprint to production, new algorithms in the Bing ranking service were ported into FPGAs and deployed to a production bed within several weeks of conception, leading to significant gains in latency and throughput. The fast turnaround time of new features demanded by an agile software culture would not have been possible without a disciplined and effective approach to co-design in the datacenter. This talk will describe some of the learnings and best practices developed from this unique experience.

We present a heterogeneous computing solution to the Boolean satisfiability (SAT) problem. Our field-programmable gate array (FPGA)-based implementation for accelerating the common case computation within a SAT solver utilizes most of the FPGA resources and it seamlessly integrates with our software host. Algorithms and data structures were redesigned to maximize the strengths of customized computing and generalizable optimizations are proposed to maximize throughput, minimize communication latencies, and compact hardware memory. We are significantly faster than state-of-the-art SAT solvers in software and hardware.

Datacenter workloads demand high computational capabilities, flexibility, power efficiency, and low cost. It is challenging to improve all of these factors simultaneously. To advance datacenter capabilities beyond what commodity server designs can provide, we have designed and built a composable, reconfigurable fabric to accelerate portions of large-scale software services. Each instantiation of the fabric consists of a 6×8 2-D torus of high-end Stratix V FPGAs embedded into a half-rack of 48 machines. One FPGA is placed into each server, accessible through PCIe, and wired directly to other FPGAs with pairs of 10 Gb SAS cables. In this paper, we describe a medium-scale deployment of this fabric on a bed of 1,632 servers, and measure its efficacy in accelerating the Bing web search engine. We describe the requirements and architecture of the system, detail the critical engineering challenges and solutions needed to make the system robust in the presence of failures, and measure the performance, power, and resilience of the system when ranking candidate documents. Under high load, the largescale reconfigurable fabric improves the ranking throughput of each server by a factor of 95% for a fixed latency distribution—or, while maintaining equivalent throughput, reduces the tail latency by 29%.

We propose a hardware architecture to accelerate boolean constraint propagation (BCP). Although satisfiability (SAT) solvers in software use varying search and learning strategies, BCP is a fundamental component and by far consumes the most CPU time. Our field-programmable gate array (FPGA) design uses on-chip SRAM to facilitate the acceleration of BCP. We discuss many insights to our innovative hardware memory layout, which is very compact and enables extremely fast BCP. It also supports multithreading to minimize the idle time in hardware and to fully utilize the multicore processor host. Additionally, many industrial SAT instances encode logic gates as constraints. We compact these to simultaneously reduce the hardware memory usage as well as speed up the computation (enhanced BCP). We implemented our enhanced BCP core and integrated it with a simple software SAT solver which communicates over PCI Express. Hardware performance counters show that a single processing engine is up to 4x faster than a state-of-the-art software SAT solver.

We propose an exact solution to the single constant multiplication (SCM) problem. Existing optimal algorithms are limited to constants of up to 19 bits. Our algorithm requires less than 10 s on average to find a solution for a 32 bit constant. Optimality is guaranteed via an exhaustive search. We analyze two common SCM frameworks and the corresponding search strategies that each framework facilitates. Combining the strengths of both frameworks, we obtain highly aggressive pruning. The various strategies used in our algorithm and their underlying intuition are discussed extensively in this paper.

Existing optimal single constant multiplication (SCM) algorithms are limited to 19 bit constants. We propose an exact SCM algorithm. For 32 bit constants, the average run time is under 10 seconds. Optimality is ensured via an exhaustive search. The novelty of our algorithm is in how aggressive pruning is achieved by combining two SCM frameworks.

We propose new optimal and heuristic approaches for solving the multiple constant multiplication (MCM) problem. Bounded depth first search (BDFS), our proposed optimal algorithm, is benchmarked on problem sizes that are impractical for the existing optimal method. We focus on MCM problems with few constants but on large bit widths. In this scenario, we outperform the existing heuristics in minimizing the number of adders. In addition, subject to a given quality of solution, our run time is faster. We reuse our heuristics for pruning within BDFS.

Common subexpression elimination (CSE) algorithms try to minimize the number of adders (or subtracters) required to implement constant multiplication by searching and substituting common patterns in the CSE representation of a constant. CSE algorithms, in general, cannot find certain patterns due to inherent restrictions in the CSE representation. We propose overlapping digit patterns (ODPs) to remove some of these restrictions. We integrate ODPs into H(k), the best existing heuristic algorithm for single constant multiplication (SCM). H(k) is not applicable to the multiple constant multiplication (MCM) problem, so we cannot consider this problem. Generally, H(k) finds solutions very close to optimal, so there is a strict limitation on any further improvement which applies to any new heuristic. Instead, by integrating ODPs within H(k), we can on average significantly improve the run time of the algorithm (typically by one order of magnitude) while still reducing the number of adders.