publications

2023

1. DAC 23

   Automating Constraint-Aware Datapath Optimization using E-Graphs

   Samuel Coward, George A. Constantinides, and Theo Drane

   2023 60th ACM/IEEE Design Automation Conference (DAC), 2023
2. Automatic Generation of Complete Polynomial Interpolation Design Space for Hardware Architectures

   B. Orloski, S. Coward, and T. Drane

   Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, 2023

   Abs HTML

   Hardware implementations of elementary functions regularly deploy piecewise polynomial approximations. This work determines the complete design space of piecewise polynomial approximations meeting a given accuracy specification. Knowledge of this design space determines the minimum number of regions required to approximate the function accurately enough and facilitates the generation of optimized hardware which is competitive against the state of the art. Designers can explore the space of feasible architectures without needing to validate their choices. A heuristic based decision procedure is proposed to generate optimal ASIC hardware designs. Targeting alternative hardware technologies simply requires a modified decision procedure to explore the space. We highlight the difficulty in choosing an optimal number of regions to approximate the function with, as this is input width dependent.

3. Combining E-Graphs with Abstract Interpretation

   Samuel Coward, George A Constantinides, and Theo Drane

   In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, 2023

   HTML

2022

1. ARITH 22

   Automatic Datapath Optimization using E-Graphs

   S. Coward, G.A. Constantinides, and T. Drane

   Proceedings - Symposium on Computer Arithmetic, 2022

   Abs HTML

   Manual optimization of Register Transfer Level (RTL) datapath is commonplace in industry but holds back development as it can be very time consuming. We utilize the fact that a complex transformation of one RTL into another equivalent RTL can be broken down into a sequence of smaller, localized transformations. By representing RTL as a graph and deploying modern graph rewriting techniques we can automate the circuit design space exploration, allowing us to discover functionally equivalent but optimized architectures. We demonstrate that modern rewriting frameworks can adequately capture a wide variety of complex optimizations performed by human designers on bit-vector manipulating code, including significant error-prone subtleties regarding the validity of transformations under complex interactions of bitwidths. The proposed automated optimization approach is able to reproduce the results of typical industrial manual optimization, resulting in a reduction in circuit area by up to 71%. Not only does our tool discover optimized RTL, but also correctly identifies that the optimal architecture to implement a given arithmetic expression can depend on the width of the operands, thus producing a library of optimized designs rather than the single design point typically generated by manual optimization. In addition, we demonstrate that prior academic work on maximally exploiting carry-save representation and on multiple constant multiplication are both generalized and extended, falling out as special cases of this paper.

2. FMCAD 22

   Small Proofs from Congruence Closure

   O. Flatt, S. Coward, M. Willsey, and 2 more authors

   Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, 2022

   Abs HTML

   Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification and conflict clause generation. Smaller proof certificates speed up these activities. Though the problem of generating proofs of minimal size is known to be NP-complete, existing proof minimization algorithms for congruence closure generate unnecessarily large proofs and introduce asymptotic overhead over the core congruence closure procedure. In this paper, we introduce an O(n5) time algorithm which generates optimal proofs under a new relaxed "proof tree size"metric that directly bounds proof size. We then relax this approach further to a practical O(n log(n)) greedy algorithm which generates small proofs with no asymptotic overhead. We implemented our techniques in the egg equality saturation toolkit, yielding the first certifying equality saturation engine. We show that our greedy approach in egg quickly generates substantially smaller proofs than the state-of-the-art Z3 SMT solver on a corpus of 3760 benchmarks.

3. Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

   S. Coward, L. Paulson, T. Drane, and 1 more author

   Formal Aspects of Computing, 2022

   Abs HTML

   We present a method for formal verification of transcendental hardware and software algorithms that scales to higher precision without suffering an exponential growth in runtimes. A class of implementations using piecewise polynomial approximation to compute the result is verified using MetiTarski, an automated theorem prover, which verifies a range of inputs for each call. The method was applied to commercial implementations from Cadence Design Systems with significant runtime gains over exhaustive testing methods and was successful in proving that the expected accuracy of one implementation was overly optimistic. Reproducing the verification of a sine implementation in software, previously done using an alternative theorem-proving technique, demonstrates that the MetiTarski approach is a viable competitor. Verification of a 52-bit implementation of the square root function highlights the method’s high-precision capabilities.

2021

2020

1. Automatic Design Space Exploration for an Error Tolerant Application

   S. Coward, T. Drane, and Y. Harel

   Proceedings - Symposium on Computer Arithmetic, 2020

   Abs HTML

   Creating optimized hardware for error tolerant applications presents significant challenges as well as opportunities. Many algorithms in computer graphics & vision are error tolerant, as their application level correctness ultimately rests on human perception. This error tolerance can be exploited in reducing hardware implementation cost. The challenge is how to explore the space of application level correct designs to determine the optimized hardware architecture. This paper puts forward an approach to automatically explore the space which maximally exploits the acceptable error to minimize hardware cost for a particular graphics algorithm - Level-Of-Detail. Results, so far, have shown a 26% hardware area improvement.

2019