The course CSEE 6863 Formal Verification of Hardware and Software Systemsis intended for CS, CE and EE students. Phd students, MS students, and advanced undergraduates are all welcome. The course is relevant to students interested in *any* of the following topics: hardware design/verification, software verification, algorithms, system design. The lectures will focus on theoretical topics--no specific background in Computer Hardware (HW) design, or Software/Programming (SW) is needed. In addition, to accommodate the diverse interests of the attendees, each student will be able to choose a project that is suitable for his/her background. That is, a student who has a background in algorithms will be able to do a project on an algorithmic topic. Likewise, students with an interest in hardware (software) design, may pursue a hardware (software) verification topic. You might want to consider taking this course if *any* of the following applies... -> you love graph algorithms -> you wonder how to write algorithms that manipulate lots of objects at the same time -> you wonder how to prove a property (assertion) without writing a proof -> you are intrigued by searching large state spaces -> you wonder how to avoid buffer overflows -> you wonder how to make good use of an NP-complete problem -> you like to apply algorithms to solve tough problems -> you wonder how to verify/test software and/or hardware Prerequisites: Familiarity with basic propositional logic, finite automata/statemachines, and search algorithms (depth and breadth first search) would be useful. These concepts are usually taught in any data structures, algorithms or discrete mathematics course. If you are unsure whether you have sufficient background for the course, please contact the instructors. Special prerequisite for hardware students: If you are a student interested in hardware design/verification, then your project will typically involve the verification of RTL designs (SystemVerilog) using state-of-the art commercial CAD tools from the leading vendors. That is, you will use the same tools used in industry. Knowledge of SystemVerilog is fairly essential for most hardware positions in industry, but we understand that not every student has yet been exposed to the language. Students who have no background in Verilog or SystemVerilog will be given support at the beginning of the semester to learn basic language concepts necessary for the course project. Overview: Model checking and related computer-aided verification techniques are emerging as practical alternatives to simulation for debugging complex systems. These methods allow the designer to verify that a mathematical model of a system satisfies its abstract logical specification. This approach has been most effective for the analysis of control-intensive hardware components, and is rapidly becoming an integral part of the design cycle. More recently, similar techniques have been developed for the analysis of software and have been applied to real-world programs such as device drivers. The course will cover the theory and practice of formal verification approaches. Interestingly, the three model checking pioneers Clarke, Emerson and Sifakis have recently been awarded the Turing award, frequently referred to as the 'Nobel Prize' of computing ( http://amturing.acm.org/award_winners/clarke_1167964.cfm) (Links to an external site.) While simulation, or testing, is an approach to find bugs in a hardware, or software design, these techniques are incapable of proving the absence of bugs. In contrast, model checking systematically explores all states in an efficient way to ensure there are no bugs. For example, we can use model checking to prove that a buffer (in C), or a FIFO (in RTL) can never overflow. Particular topics that will be covered in the course include an overview of formal verification approaches, formal verification vs. simulation/testing, temporal logic, Binary Decision Diagrams, SAT (satisfiability) solvers, explicit-state and symbolic model checking, liveness and safety properties, abstraction techniques, software model checking, formal verification in the HW and SW industry (which techniques really work and which do not). How the course covers specific interests:For HW students: This course will prove very useful if you intend to look for an entry-level job in the hardware industry as this course teaches state-of-the-art verification skills and you can use industry-standard tools. Entry-level hardware jobs often require some knowledge of verification. For SW students: Formal verification techniques are important not only to prove properties but also for automated test generation and security. You will be able to explore these approaches during the project phase of the course. For students interested in CS/Algorithms/Theory: Model Checking algorithms are extensions of graph algorithms that represent and traverse huge state spaces using implicit data structures such as binary decision diagrams (BDDs). In a somewhat counter-intuitive way, satisfiability (SAT) solvers can be used as an efficient compute engine for verification problems. Interestingly, the topics covered in the course were at the core of three (!!!) Turing awards. ============================================================================ Class Time: Wednesdays 6:10 - 8:00 PMCall number: 25121============================================================================ Questions/Contact:Should you have any questions regarding the course, then please do not hesitate to email the instructors at: mt148@columbia.edu ============================================================================ Note:After being offered as a special topics course for several years, the course was recently assigned its own permanent course designator CSEE 6863. The new "CSEE 6863" designator may not have made it into all documents yet; the course may still be listed under CS6998. Should you run into any problems (unable to register, unable to include into your program) because of the new course designator, then please let us know. |