CSEE E6863 Formal Verification of Hardware and Software Systems

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.