Class Periods: Tue 3:00-4:55pm, Thu 4:00-4:55pm
Location: Rinker Hall 215
Academic Term: Fall 2024
Instructor:
- Name: Sandip Ray
- Email Address: sandip@ece.ufl.edu
- Office Phone Number: +1 (352) 392-1605
Course Description
Our reliance on computing and microelectronics systems and software of all forms is increasing every day. It is obviously critical to ensure that they operate as intended. Formal methods constitute the technology of using mathematical analysis to verify key correctness, security, and safety properties of such systems. The course will provide a comprehensive overview of formal methods, focusing in particular on hands-on exploration of various formal tools and technologies and their applications on industrial problems.
Course Pre-Requisites / Co-Requisites
No specific pre-requisites. However, knowledge of C++ and Verilog will be helpful for some of the topics.
Course Objectives
Upon completion of the course, students should have a good understanding of principles and practice of formal verification techniques for developing assurance in modern microelectronics and software systems.
- Different categories of formal analysis techniques and their domains of applicability
- Major application domains for formal methods in industry
- Hands-on experience with various formal tools and their applications on industrial application
- Limitations of formal verification and emergent approaches to address them
Materials and Supply Fees
None
Required Textbooks and Software
No required textbook. Relevant research papers and other notes will be provided in class. The course will include significant hands-on component, with the students exploring a number of industrial tools. Software tools to be explored include Cadence Jaspergold and Conformal, Synopsys VCFormal, IBM SixthSense, Intel VOSS, and Z3 and Dafny from Microsoft as well as tools from academia with significant industrial applications including ABC toolsuite (Berkeley), ACL2 theorem prover (UT Austin), and KLEE symbolic simulation (Stanford). These tools will be made available to students in the ECE server.
Recommended Materials
The following books can be used by students for further readings of the topics covered in the class.
- M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith. Model Checking, Second Edition. MIT Press
- Kaufmann, P. Manolios, J S. Moore. Computer-Aided Reasoning: An Approach. Springer
- Christel Baier and Joost-Pieter Katoen, Principles of Model Checking. MIT Press
Course Schedule (Tentative)
- Week 1: Introduction to formal verification: Distinction between formal verification and simulation/testing
- Week 2: Boolean logic, Equivalence Checking (EC), SAT solving; Role of EC in industrial formal verification
- Week 3: Arithmetic Logic Verification; Use of Equivalence Checking; Property-based verification
- Week 4: Temporal logic basics; Introduction to Model Checking
- Week 5: Introduction to Theorem Proving; theorem proving vs model checking in industrial designs
- Week 6: Term paper Topics
- Week 7: Assertion based verification; introduction to SystemVerilog Assertions
- Week 8: Review Topics; In-class Exam
- Week 9: Verification of Industrial Arithmetic Circuits
- Week 9: Introduction to Microarchitecture Verification; Verification as an agile integration activity
- Week 10: Symbolic Model Checking; Binary Decision Diagram; And-Inverter Graphs
- Week 11: Verification of Concurrent Systems; Use of Symmetry in Verification
- Week 12: State Exploration; Symbolic Simulation
- Week 13: Concolic Testing; Test Generation
- Week 14: Term paper / Project Presentation
- Week 15: Term paper / Project Presentation
Attendance Policy, Class Expectations, and Make-Up Policy
Excused absences must be consistent with university policies in the Graduate Catalog () and require appropriate documentation. Additional information can be found here: ()
Evaluation of Grades
| Assignment | Total Points | Percentage of Final Grade |
| Class Participation | 100 | 5% |
| Paper presentation | 100 (each) | 20% |
| Critique & review | 100 (each) | 10% |
| Homework Tool Exercises | 100 (each) | 20% |
| In-term Final Exam | 100 | 20% |
| Project | 100 | 25% |
| TOTAL | — | 100% |
This is a hands-on course. Focus will be on formal tools and their usage in solving various verification problems. Students will learn to use the available tools and get a flavor of how they are used in various industrial applications. While we will have some materials to cover the underlying formal foundations these will be primarily to help comprehend the operations and limitations of tools.
Class participation grade will be based on your interactions in class. We will keep track of the class interactions, and make the class participation grade available to the students on or before the last day of class.
Papers/tools for presentation will be selected by the instructor and suggested to the class. Each student will be required to give one short presentation in class of the paper, followed by a brief Q&A. The topic of the presentation will correspond to the topic being covered in the corresponding week. Each student will give 1-2 presentations during the course of the semester. The grade for the presentation will be based on the content presented (50%) and clarity of presentation (50%).
Each student not presenting a paper can choose a paper to write a critique. A student needs to choose at least 4 papers for critique throughout the semester. The critique should be a 1-page review in two parts: critique of the paper (60%) and critique of the presentation (40%).
Tool exercises will be homeworks that will be assigned regularly by the instructor during the course of the semester. These would consist of short implementation assignments requiring the students to play with the different formal tools introduced in the course. Each exercise will target a specific tool (e.g., Jaspergold, ACL2, etc.) or a combination of tools and ask the students to implement the solution to a specific formal verification problem using the tool(s). The focus is to provide the students hands-on experience of various industrial tools and their interaction, and instill the understanding that different tools are useful for different problems. Late submissions will incur a 10% penalty per day. The tool exercise with the lowest grade will be dropped.
The final project is an implementation project on an area related to the course, providing more extensive hands-on experience on a specific tool or combination of tools. Project ideas will be presented in class and will typically involve sanitized or simplified versions of actual formal methods problems experienced in industry. Projects can be done in a team of no more than 3 students. The project will have three components: (1) a 1-page proposal (10%), and (2) in-class presentation (40%), and a final report (50%). For projects done in team, the contribution of each team member should be explicitly stated in the presentation and the final report. The report should not be more than 5 pages. During presentation, each member of the project must present the part of the project they contributed to, and answer questions. Presentation grade will be based on the quality of the overall project (40%, each project member gets the same grade), and the quality and presentation of your specific part (60%). The report should have (1) a motivation, introduction, and related work section (30% of grade) (2) individual sections on each member contribution (40% of report grade), and (3) a summary section explaining how the individual sections fit together to solve the overall problem. Students will be graded as a team for parts 1 and 3 and individually for part 2.
The in-term final will be given in class on November 19 (Tuesday the week before Thanksgiving). No makeup exams will be given except for documented medical or other emergencies.
Grading Policy
| Percent | Grade | Grade Points |
| 93.0 – 100 | A | 4.00 |
| 90.0 – 92.9 | A- | 3.67 |
| 87.0 – 89.9 | B+ | 3.33 |
| 83.0 – 86.9 | B | 3.00 |
| 80.0 – 82.9 | B- | 2.67 |
| 77.0 – 79.9 | C+ | 2.33 |
| 73.0 – 76.9 | C | 2.00 |
| 70.0 – 72.9 | C- | 1.67 |
| 67.0 – 69.9 | D+ | 1.33 |
| 63.0 – 66.9 | D | 1.00 |
| 60.0 – 62.9 | D- | 0.67 |
| 0 – 59.9 | E | 0.00 |
More information on UF grading policy may be found at:
Students Requiring Accommodations
Students with disabilities who experience learning barriers and would like to request academic accommodations should connect with the disability Resource Center by visiting https://disability.ufl.edu/students/get-started/Links to an external site.. It is important for students to share their accommodation letter with their instructor and discuss their access needs, as early as possible in the semester.
Course Evaluation
Students are expected to provide professional and respectful feedback on the quality of instruction in this course by completing course evaluations online via GatorEvals. Guidance on how to give feedback in a professional and respectful manner is available at https://gatorevals.aa.ufl.edu/students/Links to an external site.. Students will be notified when the evaluation period opens, and can complete evaluations through the email they receive from GatorEvals, in their Canvas course menu under GatorEvals, or via https://ufl.bluera.com/ufl/Links to an external site.. Summaries of course evaluation results are available to students at https://gatorevals.aa.ufl.edu/public-results/Links to an external site..
In-Class Recording
Students are allowed to record video or audio of class lectures. However, the purposes for which these recordings may be used are strictly controlled. The only allowable purposes are (1) for personal educational use, (2) in connection with a complaint to the university, or (3) as evidence in, or in preparation for, a criminal or civil proceeding. All other purposes are prohibited. Specifically, students may not publish recorded lectures without the written consent of the instructor.
A “class lecture” is an educational presentation intended to inform or teach enrolled students about a particular subject, including any instructor-led discussions that form part of the presentation, and delivered by any instructor hired or appointed by the University, or by a guest instructor, as part of a University of Florida course. A class lecture does not include lab sessions, student presentations, clinical presentations such as patient history, academic exercises involving solely student participation, assessments (quizzes, tests, exams), field trips, private conversations between students in the class or between a student and the faculty or lecturer during a class session.
Publication without permission of the instructor is prohibited. To “publish” means to share, transmit, circulate, distribute, or provide access to a recording, regardless of format or medium, to another person (or persons), including but not limited to another student within the same class section. Additionally, a recording, or transcript of a recording, is considered published if it is posted on or uploaded to, in whole or in part, any media platform, including but not limited to social media, book, magazine, newspaper, leaflet, or third party note/tutoring services. A student who publishes a recording without written consent may be subject to a civil cause of action instituted by a person injured by the publication and/or discipline under UF Regulation 4.040 Student Honor Code and Student Conduct Code.
University Honesty Policy
UF students are bound by The Honor Pledge which states, “We, the members of the University of Florida community, pledge to hold ourselves and our peers to the highest standards of honor and integrity by abiding by the Honor Code. On all work submitted for credit by students at the University of Florida, the following pledge is either required or implied: “On my honor, I have neither given nor received unauthorized aid in doing this assignment.” The Conduct Code (https://sccr.dso.ufl.edu/process/student-conduct-code/)Links to an external site. specifies a number of behaviors that are in violation of this code and the possible sanctions. If you have any questions or concerns, please consult with the instructor or TAs in this class.
Commitment to a Safe and Inclusive Learning Environment
The Herbert Wertheim College of Engineering values broad diversity within our community and is committed to individual and group empowerment, inclusion, and the elimination of discrimination. It is expected that every person in this class will treat one another with dignity and respect regardless of gender, sexuality, disability, age, socioeconomic status, ethnicity, race, and culture.
If you feel like your performance in class is being impacted by discrimination or harassment of any kind, please contact your instructor or any of the following:
- Your academic advisor or Graduate Program Coordinator
- HWCOE Human Resources, 352-392-0904, student-support-hr@eng.ufl.edu
- Curtis Taylor, Associate Dean of Student Affairs, 352-392-2177, taylor@eng.ufl.edu
- Toshikazu Nishida, Associate Dean of Academic Affairs, 352-392-0943, nishida@eng.ufl.edu
Software Use
All faculty, staff, and students of the University are required and expected to obey the laws and legal agreements governing software use. Failure to do so can lead to monetary damages and/or criminal penalties for the individual violator. Because such violations are also against University policies and rules, disciplinary action will be taken as appropriate. We, the members of the University of Florida community, pledge to uphold ourselves and our peers to the highest standards of honesty and integrity.
Student Privacy
There are federal laws protecting your privacy with regards to grades earned in courses and on individual assignments. For more information, please see: https://registrar.ufl.edu/ferpa.htmlLinks to an external site.
Campus Resources:
Health and Wellness
U Matter, We Care:
Your well-being is important to the University of Florida. The U Matter, We Care initiative is committed to creating a culture of care on our campus by encouraging members of our community to look out for one another and to reach out for help if a member of our community is in need. If you or a friend is in distress, please contact umatter@ufl.edu so that the U Matter, We Care Team can reach out to the student in distress. A nighttime and weekend crisis counselor is available by phone at 352-392-1575. The U Matter, We Care Team can help connect students to the many other helping resources available including, but not limited to, Victim Advocates, Housing staff, and the Counseling and Wellness Center. Please remember that asking for help is a sign of strength. In case of emergency, call 9-1-1.
Counseling and Wellness Center: https://counseling.ufl.eduLinks to an external site., and 392-1575; and the University Police Department: 392-1111 or 9-1-1 for emergencies.
Sexual Discrimination, Harassment, Assault, or Violence
If you or a friend has been subjected to sexual discrimination, sexual harassment, sexual assault, or violence contact the Office of Title IX ComplianceLinks to an external site., located at Yon Hall Room 427, 1908 Stadium Road, (352) 273-1094, title-ix@ufl.edu
Sexual Assault Recovery Services (SARS)
Student Health Care Center, 392-1161.
University Police Department at 392-1111 (or 9-1-1 for emergencies), or http://www.police.ufl.edu/Links to an external site..
Academic Resources
E-learning technical support, 352-392-4357 (select option 2) or e-mail to Learning-support@ufl.edu. https://lss.at.ufl.edu/help.shtmlLinks to an external site..
Career Resource Center, Reitz Union, 392-1601. Career assistance and counseling; https://career.ufl.eduLinks to an external site..
Library Support, http://cms.uflib.ufl.edu/askLinks to an external site.. Various ways to receive assistance with respect to using the libraries or finding resources.
Teaching Center, Broward Hall, 392-2010 or 392-6420. General study skills and tutoring. https://teachingcenter.ufl.edu/Links to an external site..
Writing Studio, 302 Tigert Hall, 846-1138. Help brainstorming, formatting, and writing papers. https://writing.ufl.edu/writing-studio/Links to an external site..
Student Complaints Campus: https://sccr.dso.ufl.edu/policies/student-honor-code-student-conduct-code/Links to an external site.;https://care.dso.ufl.eduLinks to an external site..
On-Line Students Complaints: http://www.distance.ufl.edu/student-complaint-process