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.
Allen Newell was an American researcher in computer science and cognitive psychology at the RAND Corporation and at Carnegie Mellon University's School of Computer Science, Tepper School of Business, and Department of Psychology. He contributed to the Information Processing Language (1956) and two of the earliest AI programs, the Logic Theorist (1956) and the General Problem Solver (1957). He was awarded the ACM's A.M. Turing Award along with Herbert A. Simon in 1975 for their contributions to artificial intelligence and the psychology of human cognition.
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.
Arvind is the Johnson Professor of Computer Science and Engineering in the Computer Science and Artificial Intelligence Laboratory (CSAIL) at the Massachusetts Institute of Technology (MIT). He is a Fellow of the Institute of Electrical and Electronics Engineers (IEEE) and the Association for Computing Machinery (ACM). He was also elected as a member into the National Academy of Engineering in 2008 for contributions to dataflow and multithread computing and the development of tools for the high-level synthesis of digital electronics hardware.
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.
Gary Lee Miller is a professor of Computer Science at Carnegie Mellon University, Pittsburgh, United States. In 2003 he won the ACM Paris Kanellakis Award for the Miller–Rabin primality test. He was made an ACM Fellow in 2002 and won the Knuth Prize in 2013.
Prabhu Goel is an Indian American researcher, entrepreneur and businessman, known for having developed the PODEM Automatic test pattern generation and Verilog hardware description language.
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.
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
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.
Sharad Malik is an Indian-American computer scientist working in formal methods, electronic design automation, and computer architecture. He is currently the George Van Ness Lothrop Professor of Engineering in the Electrical and Computer Engineering Department at Princeton University.
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."
