EEE4701: Automated Hardware/Software Verification

Course Description

EEE 4701 Automated Hardware/Software Verification addresses the question that dominates modern digital system development: how do you establish that a design is correct? Verification consumes more effort than design in most hardware projects — commonly cited at sixty to seventy per cent of the total — and it is where the majority of entry-level digital hardware jobs are.

The Statewide Course Numbering System titles it Automated Hardware/Software Verification and describes it as a course in which students “develop modeling, formal specification, and automated verification skills for analyzing complex hardware and/or software systems” with “hands-on experience with model checking tools.” The statewide prerequisites are EEL 3744C and COP 3530.

⚠⚠ The two institutions carrying this number teach genuinely different methods. This is the most consequential thing on this page, and it is not ordinary title drift:

	University of Florida	University of Central Florida
Title	Automated Hardware/Software Verification	Verification and Validation of Digital Systems
Description	“Modeling, formal specification, and automated verification skills for analyzing complex hardware and/or software systems.”	“Verification of digital hardware systems at the Register-Transfer Level focusing on Constrained Random Verification and the use of Universal Verification Methodology.”
Method	Formal methods — model checking, temporal logic, exhaustive proof	Simulation-based — constrained-random stimulus, coverage, UVM
Prerequisite	EEL 3744C or equivalent and COP 3530 or equivalent	EEL 3801C Computer Organization (minimum grade C)
Scope	Hardware and/or software	Digital hardware

Both are legitimate and both are called verification, but the skills barely overlap. Formal verification proves a property holds for every possible input; simulation-based verification exercises a design with a very large number of randomly generated inputs and measures how much of it was covered. One is a mathematical argument, the other an engineering campaign. A graduate trained in one is not thereby qualified in the other, and the Special Information section explains what to do about that.

This guide covers both, labelled throughout. Both institutions carry the course at 3 credits; UCF offers it in the Fall only and schedules laboratory hours alongside the lecture.

Learning Outcomes

Required Outcomes (both readings)

• Explain why verification dominates the effort in digital system development, and distinguish verification from validation and from testing.
• Construct a formal or executable specification of intended behaviour that is separate from the implementation.
• Build an abstract model of a hardware or software system suitable for analysis, and justify the abstraction.
• Distinguish safety properties from liveness properties and express each precisely.
• Develop a verification plan from a specification, identifying what must be checked and how completion will be judged.
• Use an industry or research verification tool to analyse a non-trivial design.
• Diagnose a reported failure, produce a minimal reproducing case, and trace it to a defect in the design or in the specification.
• Assess verification completeness and argue, with evidence, when verification is sufficient.

Required Outcomes — formal reading (UF)

• Model a system as a finite-state transition system or Kripke structure.
• Express properties in temporal logic (LTL and CTL) and explain the difference in expressive power.
• Apply explicit-state and symbolic model checking, and explain the role of binary decision diagrams and bounded model checking with SAT/SMT solvers.
• Explain and confront the state-explosion problem, and apply abstraction, symmetry reduction and compositional reasoning to mitigate it.
• Interpret a counterexample trace produced by a model checker and act on it.
• Apply equivalence checking between two representations of a design.

Required Outcomes — simulation reading (UCF)

• Construct a layered testbench separating stimulus generation, driving, monitoring, checking and scoreboarding.
• Write constrained-random stimulus generators and reason about the constraint solver’s distribution.
• Define functional coverage models and cover groups, and use coverage results to close a verification plan.
• Interpret code coverage metrics (line, branch, toggle, FSM) and explain why high code coverage is not sufficient.
• Build reusable verification components using the Universal Verification Methodology: agents, drivers, sequencers, monitors and the factory.
• Write SystemVerilog assertions and integrate assertion-based checking into a simulation flow.

Optional Outcomes

• Apply formal property verification alongside a simulation flow (the hybrid approach used in industry).
• Apply theorem proving to systems beyond the reach of model checking.
• Apply software model checking and static analysis to source code.
• Verify cache coherence, bus and interconnect protocols.
• Apply emulation and hardware-accelerated verification.
• Apply verification techniques to security properties and information-flow analysis.
• Analyse verification in safety-critical certification contexts (DO-254, ISO 26262).

Major Topics

Required Topics

• The verification problem — why correctness cannot be established by design alone, the cost of defects found late, the verification-to-design effort ratio, and famous failures (the Pentium FDIV bug, Ariane 5, Therac-25) as motivation.
• Specification — separating intent from implementation, formal versus informal specification, ambiguity in natural-language requirements, and the observation that a substantial fraction of “bugs” are specification defects rather than implementation defects.
• Modelling and abstraction — finite-state models, transition systems, the choice of abstraction level, and what an abstraction preserves and discards.
• Properties — safety (“nothing bad happens”) and liveness (“something good eventually happens”), invariants, fairness assumptions, and the practical difficulty of writing a property that says what you meant.
• Coverage and completeness — what it means to have verified enough, and why no single metric answers the question.
• Tools and flow — hands-on use of a verification tool, integration into a development flow, regression, and the interpretation of results.
• Debugging from a failure — counterexample or failing-trace analysis, minimisation, and root-cause attribution.

Required Topics — formal reading (UF)

• Temporal logic — linear temporal logic operators, computation tree logic, path versus state quantification, and expressing real requirements in each.
• Model checking algorithms — explicit-state search, automata-theoretic LTL model checking, CTL fixed-point computation.
• Symbolic methods — binary decision diagrams and their variable-ordering sensitivity; bounded model checking with SAT; SMT solvers and their theories.
• State explosion — the exponential growth of state space, and the mitigations: abstraction and refinement (CEGAR), partial-order reduction, symmetry reduction, compositional and assume–guarantee reasoning.
• Equivalence checking — combinational and sequential equivalence, and its industrial role in confirming that synthesis preserved behaviour.
• Tools — NuSMV/nuXmv, SPIN and Promela, TLA+, CBMC, and Z3.

Required Topics — simulation reading (UCF)

• Register-transfer level verification — the design under test, the testbench boundary, and clocking and reset discipline.
• SystemVerilog for verification — classes, randomisation and constraints, interfaces and clocking blocks, mailboxes and semaphores, and the separation of the testbench from the design.
• Constrained-random verification — the argument for random stimulus over directed tests, constraint solving and distribution control, seeds and reproducibility, and directed tests for corner cases the random generator will not reach.
• Coverage-driven verification — functional coverage, covergroups, coverpoints and crosses; code coverage metrics; the coverage-closure loop; and why one hundred per cent code coverage proves very little.
• The Universal Verification Methodology — UVM class hierarchy, agents, drivers, sequencers and sequences, monitors, scoreboards, the configuration database and the factory; phases; and verification component reuse.
• Assertion-based verification — SystemVerilog Assertions, immediate and concurrent assertions, sequences and properties, and binding assertions to a design.
• Tools — Synopsys VCS, Cadence Xcelium, Siemens EDA Questa; the open-source Verilator and cocotb.

Resources & Tools

• Formal reading: Principles of Model Checking (Baier and Katoen) is the standard graduate reference; Model Checking (Clarke, Grumberg and Peled) is the foundational text by the field’s Turing Award winners; The SPIN Model Checker (Holzmann) and Specifying Systems (Lamport, on TLA+, free online) are the practical companions.
• Simulation reading: SystemVerilog for Verification (Chris Spear) is the standard text and the book most verification engineers learn from; The UVM Primer (Ray Salemi) is the accessible introduction; Writing Testbenches using SystemVerilog (Bergeron) and the Accellera UVM User Guide (free) are the references.
• Comprehensive Functional Verification (Wile, Goss and Roesner) covers the discipline as a whole and is a good bridge between the two readings.
• Formal tools — NuSMV and nuXmv, SPIN, TLA+ with the TLC checker, CBMC, and the Z3 SMT solver. All are free, which makes the formal side unusually accessible for self-study.
• Simulation tools — commercial simulators (VCS, Xcelium, Questa) are the industry standard and are available through university programmes. Verilator (free, very fast) and cocotb (Python-based testbenches) are genuine open alternatives, and EDA Playground provides browser-based access to several simulators for small examples.
• Reference material — the Accellera UVM standard and IEEE 1800 (SystemVerilog); the Design and Verification Conference (DVCon) proceedings, which is where verification practice is published; Verification Academy (Siemens) for free tutorial material.

Career Pathways

• Design verification engineer — the direct destination, and worth emphasising: verification engineers substantially outnumber design engineers in the semiconductor industry. Students frequently overlook this because design sounds more prestigious; the job market does not agree.
• Formal verification engineer — a smaller and more specialised role, well paid, concentrated at large processor and IP companies (Intel, AMD, Arm, Apple, NVIDIA) and in aerospace.
• Verification lead and verification methodology engineer — senior roles building the infrastructure other engineers use.
• Software verification and validation engineer — particularly in aerospace and medical devices, where certification requires evidence.
• Safety and certification engineer — DO-254 (airborne hardware), DO-178C (airborne software) and ISO 26262 (automotive) all require documented verification evidence, and engineers who understand both the methods and the standards are in demand.
• Security verification engineer — verifying information-flow and access-control properties in hardware, an area where UF has particular strength.
• ⚠ A practical observation for job seekers. Verification is one of the more accessible entry points into the semiconductor industry for a bachelor’s graduate, because the demand is large and the skills are teachable and demonstrable. A student who can show a UVM testbench they built, or a model-checked protocol, has something specific to discuss — and interviewers in this field ask exactly that.
• Florida employers include L3Harris (Palm Bay and Melbourne — where DO-254 verification for airborne hardware is routine work), Lockheed Martin (Orlando), Northrop Grumman (Melbourne), Raytheon/RTX (Largo), and the Space Coast avionics sector. Verification for commercial semiconductor companies is largely outside Florida, so plan on a national search for those — though verification is also one of the specialisations most amenable to remote work.

Special Information

⚠⚠ Know which method your course teaches — the skills are not interchangeable

The divergence described at the top of this guide has direct practical consequences:

• If you are at UCF, you will learn constrained-random verification and UVM. This is what the great majority of verification jobs actually use, and it is immediately marketable. You will not learn model checking or temporal logic.
• If you are at UF, you will learn formal specification and model checking. This is intellectually deeper, applies to software as well as hardware, and is what a smaller number of specialised and well-paid roles require. You will not learn UVM.
• A transfer student should not assume equivalence. A UCF student transferring to UF with EEE 4309C-adjacent verification experience has not covered formal methods; a UF student arriving at UCF has not written a testbench. In either direction, check the topic list rather than the number, and expect to fill the gap.

A syllabus test. If the assessed work is temporal logic properties, counterexample traces and NuSMV or SPIN, you are in the formal course. If it is SystemVerilog classes, covergroups, UVM agents and a coverage-closure report, you are in the simulation course.

The honest recommendation: industry uses both, and increasingly together — formal property verification is now a routine complement to simulation in large projects. If your institution offers only one, it is worth spending time on the other independently. The formal tools are all free, and TLA+ in particular has excellent free learning material, so the formal side is the easier of the two to pick up alone.

Prerequisites

UF requires EEL 3744C or equivalent and COP 3530 or equivalent — microprocessor applications and data structures. UCF requires EEL 3801C Computer Organization with a minimum grade of C. The statewide record lists EEL 3744C and COP 3530.

⚠ UF’s data-structures requirement is a genuine signal, not a formality. Model checking algorithms are graph algorithms over state spaces, symbolic methods rest on binary decision diagrams, and complexity reasoning is constant. A student weak in data structures and algorithms will find the formal course hard for reasons that have nothing to do with hardware.

⚠ For the simulation reading, the unnamed requirement is object-oriented programming. UVM is a large class library, and SystemVerilog verification code is object-oriented code: inheritance, polymorphism, factories and callbacks. A student whose programming experience is procedural C will find UVM’s structure — not its syntax — the obstacle. If that describes you, spending time with object-oriented design before the term will pay for itself.

Both readings assume comfort with hardware description languages and digital design, since you cannot verify a design you cannot read.

⚠ Course-code variation across Florida

• EEE 4701 — UF and UCF, with the divergence described above.
• EEE 4404 Mixed Signal IC Testing I — University of Florida: testing rather than verification, and a genuinely different activity (verifying a design against its specification versus testing a manufactured part for defects). Do not conflate them.
• Related material appears in computer engineering courses under CDA and CEN prefixes, and in software engineering courses, at several institutions.

SCNS equivalency does not cross course numbers or prefixes. Carry the syllabus, and keep the artefacts — a testbench or a model-checked specification is far more persuasive than a course description, to a substitution committee and to an employer alike.

Position in the curriculum

EEE 4701 is a senior-level elective following computer organisation or microprocessor applications. At UCF it complements EEE 3342C Digital Systems and EEE 4334 VLSI Design; at UF it sits alongside the hardware security sequence (EEE 4714, EEE 4740), with which it shares a formal-reasoning outlook. It is directly useful for senior design projects, where a disciplined verification approach is often what separates a project that works from one that nearly works.

⚠ UCF offers this course in Fall only. Plan accordingly if it is required for a concentration.

Difficulty and time commitment

Both readings are demanding, in different ways.

The formal course is mathematically demanding: temporal logic is unfamiliar, and writing a property that expresses what you actually meant is genuinely hard — students routinely write properties that are trivially true or vacuously satisfied and conclude a design is correct when nothing was checked. Vacuity is the characteristic beginner failure in formal verification, and learning to detect it is a real part of the course.

The simulation course is demanding in volume: UVM is a large framework with a great deal of boilerplate, and the learning curve is steep before anything works. Students commonly spend the first several weeks fighting the infrastructure rather than verifying anything.

Plan on ten to twelve hours a week in either. In the simulation course specifically, start assignments immediately — a UVM testbench that does not elaborate cannot be debugged the night before it is due.

Articulation and transfer

SCNS records EEE 4701 as guaranteed to transfer to an institution offering the same course. Two Florida institutions carry it, both at 3 credits — but as set out above, the guarantee transfers the credit, not the skill set. The course is upper-division and carries no general-education or Gordon Rule designation.

FE exam relevance

The NCEES Fundamentals of Engineering (Electrical and Computer) exam covers digital systems and software development but does not test verification methodology. This is an elective taken for its substantial employability value rather than for FE coverage.

AI Integration

Verification is one of the fields where AI assistance has been adopted fastest, and also one where the reasoning about why it helps is unusually clear — which makes this section genuinely useful rather than cautionary.

Where AI is genuinely used in the discipline. Commercial EDA vendors now ship machine learning in verification flows: regression optimisation selects which tests to run from a large suite, coverage closure guidance suggests stimulus likely to hit uncovered bins, bug triage clusters failures by likely root cause, and test generation proposes stimulus for hard-to-reach states. Large language models are increasingly used to draft testbench boilerplate and SystemVerilog assertions from natural-language requirements. A verification engineer entering the field now will use these tools, and the productive framing is that they generate candidate work that a human must judge.

Where a general-purpose assistant helps in coursework. Explaining a temporal logic operator or why CTL and LTL differ in expressive power; generating UVM boilerplate, which is voluminous and formulaic and is the single best use of a code assistant in this course; explaining a simulator elaboration error; drafting covergroups from a specification; and summarising what a counterexample trace is showing.

⚠ Where it fails, and why the failure is exactly this course’s subject. The characteristic error is the deepest one available in this field: an AI tool generates a testbench or a property from the same understanding of the specification that produced the design — and therefore reproduces the design’s misunderstandings.

This is precisely what verification exists to prevent. The entire discipline rests on the checker being derived independently of the implementation: if the specification says a FIFO must never overflow and the designer misread it, a checker written from the same misreading will pass. Asking a model to generate both the RTL and its testbench, or to generate assertions by reading the RTL, produces a verification environment that confirms what the design does rather than what it should do. It is a tautology dressed as evidence, and it is the most dangerous failure mode in the field because everything appears to pass.

Two further failures are specific and common. Generated SystemVerilog assertions are frequently vacuous — the antecedent never holds, so the property passes without ever checking anything. A vacuity check is a standard tool feature and is essential when using generated assertions. And generated constraints frequently produce a distribution nobody intended, technically satisfying the constraint while concentrating stimulus in a narrow region, so coverage stalls for reasons that are invisible until the coverage report is read carefully.

On the formal side: models are unreliable at the state-explosion reasoning that determines whether a model checking problem is tractable at all, and will confidently propose an approach that will not terminate.

The engineer’s responsibility. Verification produces evidence that a design meets its specification, and in certified domains — DO-254, ISO 26262 — that evidence is a regulatory artefact with an engineer’s name attached. The discipline is independence: the checker must come from the specification, not from the implementation, and a human must confirm that the property says what was meant. A passing test is only as good as the reason it could have failed. If you cannot describe the bug a check would catch, the check is not evidence.

Academic integrity. The University of Florida Student Honor Code and UCF’s Rules of Conduct both cover AI-generated work, and practice varies by instructor. Verification plans, property specifications and coverage analysis are normally expected to be your own even where boilerplate generation is permitted — and they are the assessed intellectual content in any case. Generated coverage or simulation results are data fabrication. Ask before you rely on a tool, and disclose its use where the syllabus requires it.