The course CSEE 6863 Formal Verification of Hardware and Software Systems
is 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/state
machines, 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 PM
Call number:
============================================================================
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.