In computer engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, most commonly to design ASICs and program FPGAs.
Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.
The School of Computer Science (SCS) at Carnegie Mellon University in Pittsburgh, Pennsylvania, US is a school for computer science established in 1988. It has been consistently ranked among the top computer science programs over the decades. As of 2022 U.S. News & World Report ranks the graduate program as tied for second with Stanford University and University of California, Berkeley. It is ranked second in the United States on Computer Science Open Rankings, which combines scores from multiple independent rankings.
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Unlike other compressed representations, operations are performed directly on the compressed representation, i.e. without decompression.
Formal equivalence checking process is a part of electronic design automation (EDA), commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior.
Hsiang-Tsung Kung is a Taiwanese-born American computer scientist. He is the William H. Gates professor of computer science at Harvard University. His early research in parallel computing produced the systolic array in 1979, which has since become a core computational component of hardware accelerators for artificial intelligence, including Google's Tensor Processing Unit (TPU). Similarly, he proposed optimistic concurrency control in 1981, now a key principle in memory and database transaction systems, including MySQL, Apache CouchDB, Google's App Engine, and Ruby on Rails. He remains an active researcher, with ongoing contributions to computational complexity theory, hardware design, parallel computing, routing, wireless communication, signal processing, and artificial intelligence.
Charles Eric Leiserson is a computer scientist and professor at Massachusetts Institute of Technology (M.I.T.). He specializes in the theory of parallel computing and distributed computing.
An and-inverter graph (AIG) is a directed, acyclic graph that represents a structural implementation of the logical functionality of a circuit or network. An AIG consists of two-input nodes representing logical conjunction, terminal nodes labeled with variable names, and edges optionally containing markers indicating logical negation. This representation of a logic function is rarely structurally efficient for large circuits, but is an efficient representation for manipulation of boolean functions. Typically, the abstract graph is represented as a data structure in software.
Edmund Melson Clarke, Jr. was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.
Ernest Allen Emerson II, better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States.
Krishna V. Palem is a computer scientist and engineer of Indian origin and is the Kenneth and Audrey Kennedy Professor of Computing at Rice University and the director of Institute for Sustainable Nanoelectronics (ISNE) at Nanyang Technological University (NTU). He is recognized for his "pioneering contributions to the algorithmic, compilation, and architectural foundations of embedded computing", as stated in the citation of his 2009 Wallace McDowell Award, the "highest technical award made solely by the IEEE Computer Society".
Pradeep Kumar Khosla is an Indian-American computer scientist and university administrator. He is the current chancellor of the University of California, San Diego.
Rob A. Rutenbar is an American academic noted for contributions to software tools that automate analog integrated circuit design, and custom hardware platforms for high-performance automatic speech recognition. He is Senior Vice Chancellor for Research at the University of Pittsburgh, where he leads the university's strategic and operational vision for research and innovation.
Helmut Veith was an Austrian computer scientist who worked on the areas of computer-aided verification, software engineering, computer security, and logic in computer science. He was a Professor of Informatics at the Vienna University of Technology, Austria.
Daniel Kroening is a German computer scientist, Professor in computer science at the University of Oxford, and Chief Science Officer at the company he co-founded, Diffblue Ltd. He is a fellow of Magdalen College.
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
Lawrence Pileggi is the Coraluppi Head and Tanoto Professor of Electrical and Computer Engineering at Carnegie Mellon University. He is a specialist in the automation of integrated circuits, and developing software tools for the optimization of power grids. Pileggi's research has been cited thousands of times in engineering papers.
Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages. He is a professor in the computer science department at the University of Texas at Austin, where he holds the Admiral B.R. Inman Centennial Chair in Computing Theory.
Karem Sakallah is an American electrical engineer and computer scientist, a professor at University of Michigan known for his work on computational logic, functional verification, SAT solvers, satisfiability modulo theories, and the Graph automorphism problem. He was elevated to the rank of IEEE Fellow in 1998. In 2009, he shared the CAV award with eight other individuals "for major advances in creating high-performance Boolean satisfiability solvers." In 2012, Sakallah became an ACM Fellow "for algorithms for Boolean Satisfiability that advanced the state-of-the-art of hardware verification."
