13. Hardware Design Methodology, Simulation, and Verification

Introduction and Context

Digital hardware is rarely designed successfully by moving directly from an informal idea to gates and wires. Modern processors, accelerators, controllers, and system-on-chip devices contain millions or billions of state elements and must satisfy interacting requirements for functionality, performance, power, area, reliability, security, manufacturability, and cost. A design error discovered after fabrication may require a costly mask revision or make an entire product unusable. Hardware design methodology therefore provides a disciplined path from requirements to an implemented and verified artifact.

This chapter examines that path for both application-specific integrated circuits (ASICs) and field-programmable gate arrays (FPGAs). It connects requirements analysis, architectural exploration, hardware description languages (HDLs), register-transfer-level (RTL) design, simulation, emulation, synthesis, timing analysis, formal verification, testing, prototyping, and hardware-software co-verification. The central idea is that verification is not a final inspection activity. It is a continuous engineering process in which assumptions are made explicit, evidence is collected, and design risks are reduced at progressively greater levels of implementation detail.

The topic is closely related to digital logic, computer architecture, operating systems, embedded systems, and computer-aided design. At postgraduate level, the important question is not merely how an individual tool works, but how engineering decisions made at one stage constrain later stages and how a team can establish confidence in the complete system.

Learning Objectives

After studying this chapter, the learner should be able to:

1. Explain the principal stages of an ASIC and FPGA design flow.

2. Translate system requirements into measurable hardware specifications and verification properties.

3. Compare behavioral, RTL, gate-level, emulation, FPGA-prototyping, and formal-verification approaches.

4. Analyze the trade-offs among performance, power, area, schedule, cost, and verification effort.

5. Interpret synthesis reports, timing constraints, coverage results, and verification evidence.

6. Describe hardware-software co-verification and its role in embedded systems.

7. Identify common methodological failures and recommend appropriate professional practices.

From Requirements to an Executable Design Plan

A hardware project begins with a problem statement, but a problem statement is not yet a design specification. Requirements must be divided into functional and non-functional classes. Functional requirements describe operations such as instruction execution, packet classification, memory access, interrupt handling, or sensor conversion. Non-functional requirements establish limits or qualities: clock frequency, latency, throughput, energy per operation, silicon area, operating temperature, safety integrity, security, and permissible defect rates.

A useful requirement is measurable, traceable, and testable. “The accelerator shall be fast” is inadequate; “the accelerator shall process at least 100 million samples per second at a specified clock frequency and input width” is more useful. Each requirement should have an owner, an acceptance criterion, and a planned verification method. Traceability links the requirement to architectural decisions, RTL modules, assertions, test cases, coverage goals, and final evidence.

Requirements also contain assumptions. For example, a memory interface may assume bounded response latency, aligned accesses, or a particular ordering model. If assumptions are not documented, the design may appear correct in simulation while failing in a real system. Interface contracts should specify signal meanings, clock and reset behavior, legal and illegal sequences, error responses, and ownership of shared resources.

Architectural Exploration

Architecture is the level at which the major organization of the system is selected. Designers choose data widths, pipeline depth, memory hierarchy, parallelism, interconnects, buffering, clock domains, and hardware-software partitioning. An algorithm that is efficient in software may be unsuitable for hardware if it requires irregular memory access or excessive control overhead. Conversely, a repetitive numerical kernel may justify dedicated datapaths or parallel execution units.

Architectural exploration compares alternatives before detailed RTL is written. Models may be constructed in a spreadsheet, a mathematical environment, a transaction-level language, C/C++, Python, or a high-level synthesis framework. Such models estimate throughput, storage requirements, bandwidth, and numerical accuracy. They do not replace RTL verification because timing, reset behavior, finite-state control, and implementation effects are represented incompletely. Their purpose is to eliminate poor architectural choices early.

A common decision is whether functionality should be implemented in hardware, software, or a combination. Hardware can provide deterministic latency and high parallel throughput, but it reduces flexibility and may consume substantial design effort. Software is easier to modify and debug, but may not meet real-time or energy constraints. A programmable processor with application-specific hardware often provides a balanced solution.

HDL and RTL Design

HDLs such as VHDL, Verilog, and SystemVerilog describe structure and behavior. At RTL, a design is expressed in terms of registers, combinational logic, and the transfer of data between registers on clock events. RTL is not ordinary sequential software. A clocked process describes hardware that operates concurrently with other processes, and careless coding can infer unintended latches, multiple drivers, combinational loops, or priority structures.

A synchronous RTL module normally includes clearly defined clock and reset behavior, combinational next-state logic, sequential state updates, and interface protocols. Nonblocking assignments are generally used for clocked behavior so that all state updates model the same clock edge. Combinational logic should assign every output on every path. Widths and signedness should be explicit because implicit conversions can silently alter arithmetic and comparisons.

Design quality depends on more than syntactic correctness. Parameterization can support reuse, but excessive configurability may complicate verification. A clean module should have a limited responsibility, documented assumptions, stable interfaces, and deterministic behavior for illegal inputs. Coding standards, linting, interface assertions, and peer review identify many defects before simulation.

Design Abstraction and Refinement

Design proceeds through abstraction levels. A behavioral model emphasizes what the system computes. RTL introduces clocked state and cycle-level behavior. Synthesis maps RTL to a technology-independent or technology-specific gate representation. Place-and-route assigns physical resources and wiring. Post-layout models include delays and sometimes power-related effects. At each refinement, equivalence or consistency must be checked where appropriate.

Abstraction reduces complexity but can hide implementation hazards. A transaction-level model may show correct packet results while ignoring backpressure. An untimed algorithm may produce mathematically correct values while overlooking overflow, fixed-point quantization, or pipeline latency. Verification plans must therefore identify which properties are preserved at each abstraction and which require a more detailed model.

Simulation as an Executable Experiment

Simulation executes a model of the design under controlled stimuli. A testbench supplies inputs, observes outputs, checks protocols, and records failures. Simulation is valuable because it provides waveforms, repeatability, controllable corner cases, and a relatively fast debugging cycle. It is especially effective for understanding temporal behavior and diagnosing the first divergence between expected and actual state.

Simulation environments range from simple directed testbenches to constrained-random and coverage-driven verification systems. A directed test is appropriate for a known reset sequence or a specific bug. Constrained-random generation explores combinations of transactions within legal limits. A reference model, or scoreboard, predicts expected behavior and compares it with the design under test. Monitors convert signal activity into transactions, while functional coverage records whether meaningful scenarios have occurred.

A testbench must avoid reproducing the same error as the design. Independent reference models, diverse stimulus, assertions, and manually reviewed scenarios improve confidence. Random tests are not inherently effective: unconstrained randomness may spend most of its time in uninteresting states. Coverage feedback is used to target unvisited behaviors, boundary conditions, and cross-product combinations.

Simulation has fundamental limits. A passing test suite proves only that selected executions passed. Very large state spaces, rare protocol interleavings, and long-duration failures may not be explored. Four-state HDL simulation can reveal unknown or uninitialized values, but an overly permissive testbench may mask them. Gate-level simulation can expose reset, initialization, and timing-related issues, but it is usually much slower than RTL simulation.

Formal Verification and Complementary Evidence

Formal verification mathematically analyzes a design over a specified state space. A property may state that a request is eventually acknowledged, that a FIFO never underflows, that two grants are never asserted simultaneously, or that an output remains stable while a valid signal is held without acceptance. Assertions express such properties in languages such as SystemVerilog Assertions.

Property checking attempts to prove that no legal sequence violates a property, or produces a counterexample when one exists. Bounded model checking explores behavior for a finite number of cycles; induction and related techniques may establish results beyond that bound. Equivalence checking compares two representations, for example RTL and a synthesized netlist, to determine whether they implement the same behavior under defined assumptions.

Formal methods are particularly effective for control logic, arbitration, protocol compliance, security invariants, and corner cases that are difficult to reach randomly. They can struggle with very large datapaths, deep state spaces, inadequate assumptions, or properties that are poorly formulated. A vacuous proof is dangerous: if assumptions prohibit every meaningful transaction, a property may pass without testing the intended behavior. Formal verification must therefore include review of assumptions, proof coverage, and reachable-state analysis.

Simulation and formal verification answer different questions. Simulation asks whether observed scenarios behave correctly. Formal analysis asks whether a stated property holds for all behaviors within a model and its assumptions. Neither alone establishes complete system correctness.

Synthesis, Constraints, and Physical Reality

Synthesis transforms RTL into a gate-level or device-specific implementation while attempting to satisfy constraints. For ASICs, the flow proceeds through logic synthesis, floorplanning, placement, clock-tree synthesis, routing, extraction, and signoff. For FPGAs, synthesis maps RTL to lookup tables, flip-flops, block RAMs, digital signal-processing units, and routing resources, followed by placement and routing.

Timing constraints communicate design intent. Clock definitions, input and output delays, generated clocks, false paths, and multicycle paths describe how timing should be analyzed. An unconstrained path is not automatically a harmless path; it may indicate that the tool lacks essential information. A false-path declaration that is used merely to suppress a violation can conceal a real functional risk. Constraints should be reviewed, version-controlled, and checked for completeness.

Static timing analysis (STA) examines setup and hold requirements across relevant process, voltage, and temperature conditions without relying on simulation vectors. A setup violation means data may arrive too late before the receiving clock edge; a hold violation means data may change too soon after that edge. Remedies include reducing logic depth, restructuring pipelines, changing placement, improving clock distribution, or modifying the interface protocol. Increasing clock frequency is not free: deeper pipelines may increase latency, control complexity, power, and verification burden.

Synthesis reports also reveal inferred memories, arithmetic units, resource utilization, fanout, and optimization decisions. A functionally correct design can still fail because it exceeds available area, routing capacity, power limits, or timing margin. Thus verification results and implementation results must be reviewed together.

Emulation, FPGA Prototyping, and Testing

Emulation maps a design onto specialized hardware that can execute substantially faster than software simulation while retaining instrumentation and controllability. It is useful for long workloads, operating-system boot, realistic traffic, and software development before fabrication. FPGA prototyping offers practical speed and often supports real peripherals, but adapting an ASIC design to an FPGA may require clock, memory, primitive, and interface changes.

A prototype demonstrates behavior in an implementation environment, not necessarily correctness under all conditions. Limited observability, altered timing, unavailable analog behavior, and simplified memories can hide problems. Hardware debugging commonly uses trace buffers, performance counters, scan access, logic analyzers, and firmware logging. These facilities should be planned early because adding observability after deployment may be difficult.

Manufacturing test addresses defects introduced during fabrication rather than design errors alone. Design-for-test techniques include scan chains, automatic test-pattern generation, memory built-in self-test, boundary scan, and test access mechanisms. Test coverage is a statistical or structural measure, not a guarantee of absence of defects. Safety-critical products may additionally require diagnostic coverage, fault injection, redundancy, and documented failure responses.

Hardware-Software Co-Verification

Embedded systems cannot be verified solely at the RTL boundary. Firmware depends on register maps, reset values, interrupt semantics, memory ordering, DMA behavior, and error reporting. Hardware may pass unit-level tests while firmware fails because a status bit is cleared on read rather than on write, an interrupt races with a buffer update, or a cache-coherency assumption is invalid.

Co-verification combines hardware models, instruction-set simulation, emulation, FPGA prototypes, device drivers, and application workloads. Early software development can use virtual platforms or fast functional models. Later stages replace models with cycle-accurate or prototype implementations. The verification plan should include boot, power-management transitions, exception handling, concurrent DMA and CPU access, malformed inputs, recovery from faults, and performance under realistic workloads.

The interface specification should be treated as a contract shared by hardware and software teams. Register descriptions can be generated from a single source to reduce inconsistencies, while automated tests can compare specification, RTL, firmware headers, and documentation. This is an area in which automation provides substantial value, but generated artifacts still require review.

A Practical Verification Framework

A mature project uses several complementary layers:

• Unit verification checks individual modules and local invariants.
• Subsystem verification examines interactions among units, memories, and protocols.
• System verification evaluates complete workloads and external interfaces.
• Formal verification proves selected safety, liveness, and equivalence properties.
• Implementation verification checks timing, power, area, and physical constraints.
• Manufacturing test verifies the fabricated device can be screened and diagnosed.

The verification plan should begin with a risk assessment. High-risk features are those with complex control, safety or security consequences, difficult observability, novel technology, or costly failure. Each risk is assigned evidence: simulation scenarios, assertions, formal properties, reviews, coverage targets, prototype tests, or physical measurements.

Coverage must be interpreted rather than merely maximized. Code coverage can show that statements or branches were executed, while functional coverage asks whether meaningful behaviors occurred. Assertion coverage records whether properties were exercised. Coverage holes may indicate missing tests, unreachable behavior, an overconstrained environment, or a design defect. Closing coverage without understanding the cause can create false confidence.

A useful exit criterion combines passing regression tests, reviewed coverage, closed high-severity defects, successful formal proofs or justified exceptions, clean lint and CDC results, timing closure, acceptable power and area, and documented requirement traceability. “Zero failures” is not sufficient if important behavior was never exercised.

Illustrative Case Study: A Network Packet-Processing Accelerator

Background

Consider an illustrative postgraduate design project for a packet-processing accelerator attached to a processor through a memory-mapped control interface and an AXI-like streaming data interface. The accelerator classifies packets, updates counters, and forwards or discards each packet. It must sustain one packet per cycle after pipeline fill, support backpressure, and report malformed headers without corrupting later traffic.

Situation and Problem

The first RTL prototype produced correct results in short directed simulations but occasionally lost packets during long software-driven tests. The design team initially suspected a synthesis problem because the failure did not appear in the basic testbench.

Analysis

Trace analysis showed that the input stream used separate valid and ready signals. The testbench had assumed that a transfer occurred whenever valid was asserted, whereas the actual protocol required a transfer only when both valid and ready were high in the same cycle. In addition, a counter-update path assumed that classification completed in one cycle, although the pipeline introduced a three-cycle latency. The software driver also read counters while a DMA update was in progress.

Approach and Solution

The team first rewrote the interface contract using cycle-level timing diagrams. Assertions were added to check that data remained stable while valid was high and ready was low, that packets were neither duplicated nor dropped, and that output ordering was preserved. A transaction-level scoreboard tracked packet identity through stalls and pipeline latency. Formal properties proved that the elastic buffers could not underflow or overflow under their stated capacity assumptions.

The counter interface was changed to use explicit snapshot and update semantics. A co-verification test exercised processor reads, DMA activity, interrupts, reset during idle periods, and malformed packets. Constrained-random traffic varied packet length, classification result, and backpressure. FPGA prototyping then exposed a timing problem on a high-fanout classification signal; pipeline restructuring and placement constraints restored timing margin.

Outcome

The corrected design passed directed, random, formal, and software-driven tests. More importantly, the project demonstrated that the defect was methodological rather than purely syntactic. An incomplete protocol model, insufficient latency awareness, and an underspecified software interface allowed the original design to appear correct at one verification level.

Learning Points

The case illustrates several principles: interface assumptions must be executable; latency must be represented in scoreboards and software contracts; formal properties are effective for protocol invariants; hardware and firmware require a shared specification; and implementation analysis can reveal risks not visible in functional simulation.

Challenges, Risks, and Professional Responsibilities

The principal risk in verification is false confidence. Passing regressions may reflect weak stimulus, an incorrect reference model, disabled assertions, or excessive environmental assumptions. Another risk is late discovery of architectural constraints. A design that cannot meet timing or power limits should be redirected before detailed optimization consumes the schedule.

Clock-domain crossings deserve special attention. A signal crossing asynchronously between unrelated clocks can metastabilize or cause event loss unless synchronized, handshaked, or buffered appropriately. Reset-domain crossings, power-state transitions, low-power isolation, and retention behavior create related hazards. Automated CDC tools are useful, but waivers must be technically justified rather than used to silence warnings.

Security and safety are also design concerns. Hardware may expose debug ports, privilege transitions, speculative state, fault-handling paths, or side channels. Verification should consider unauthorized register access, information leakage, fault injection, denial of service, and secure boot assumptions where relevant. Safety-related designs require hazard analysis, independence of evidence, controlled change management, and standards-specific processes.

Ethically, engineers must report known limitations, unverified assumptions, and residual risks accurately. Coverage numbers should not be presented as proof of correctness. Reusing third-party IP requires attention to licensing, quality evidence, security advisories, and integration assumptions. Configuration management is essential: a result is meaningful only when the RTL, constraints, tools, libraries, testbench, and scripts are reproducible.

Emerging Directions

Design flows increasingly combine simulation, formal methods, emulation, and machine-assisted analysis. High-level synthesis can reduce RTL development time for suitable algorithms, although generated hardware still requires timing, interface, numerical, and verification analysis. Portable stimulus and reusable verification components aim to generate coordinated tests across simulation, emulation, and prototypes.

Machine learning is being explored for regression selection, coverage-hole analysis, bug triage, placement optimization, and power estimation. These applications can improve productivity but should support, not replace, engineering judgment. A model trained on historical failures may miss novel defects, and an optimization that improves a proxy metric may degrade a system-level requirement.

Chiplet-based integration, heterogeneous compute, advanced packaging, open instruction-set architectures, and increasingly complex security requirements are extending verification beyond a single RTL block. Verification must address die-to-die protocols, shared fabrics, thermal behavior, software ecosystems, and lifecycle updates. The trend is toward evidence assembled across multiple abstraction levels and organizations rather than reliance on one final simulation campaign.

Best Practices for an Effective Design Flow

A robust methodology commonly follows these principles:

1. Make every important requirement measurable and traceable.

2. Explore architecture before committing to detailed RTL.

3. Treat interfaces, clocks, resets, latency, and error behavior as explicit contracts.

4. Use lint, CDC analysis, assertions, simulation, formal verification, and coverage together.

5. Maintain independent reference models and review their assumptions.

6. Constrain synthesis and timing analysis completely and conservatively.

7. Plan observability, test access, and debug infrastructure early.

8. Verify hardware and firmware against a shared, version-controlled specification.

9. Use risk-based priorities rather than measuring success only by test count.

10. Preserve reproducibility through configuration management and documented tool versions.

Chapter Summary

Hardware design methodology transforms requirements into an implemented and evidenced digital system. Architectural exploration evaluates performance, cost, power, memory, and hardware-software partitioning before RTL commitment. HDL and RTL provide a cycle-level description of registers, combinational logic, and interfaces, but coding quality must be supported by linting and clear contracts.

Simulation provides controlled execution and debugging; formal verification examines properties over broad or complete state spaces; emulation and FPGA prototyping support realistic, long-running workloads. Synthesis, static timing analysis, power estimation, physical implementation, and manufacturing test determine whether a functionally correct design can become a usable product. Hardware-software co-verification is essential for embedded systems because register semantics, interrupts, DMA, memory ordering, and error handling cross the hardware boundary.

No single technique proves correctness. Confidence comes from layered evidence, meaningful coverage, explicit assumptions, risk-based planning, and disciplined review. The most effective flows begin verification early, preserve traceability, and treat implementation, software, security, safety, and testability as parts of one engineering problem.

Key Terms

Requirement traceability: The linkage of a requirement to design elements, tests, properties, and acceptance evidence.

Architectural exploration: Comparison of alternative system organizations before detailed implementation.

HDL: A language used to describe digital hardware structure and behavior.

RTL: A design abstraction describing registers, combinational logic, and transfers between registers.

Testbench: A simulation environment that stimulates and checks a design under test.

Scoreboard: A verification component that compares observed results with predictions from a reference model.

Functional coverage: A measure of whether intended behaviors and scenarios have been exercised.

Assertion: An executable statement of an expected design property or protocol rule.

Formal verification: Mathematical analysis used to prove properties or find counterexamples.

Equivalence checking: Verification that two design representations preserve specified behavior.

Synthesis: Transformation of RTL into gates or device-specific programmable resources.

Static timing analysis: Constraint-based analysis of timing paths without requiring simulation vectors.

Setup violation: A condition in which data arrives too late before a receiving clock edge.

Hold violation: A condition in which data changes too soon after a receiving clock edge.

Emulation: Execution of a hardware design on specialized equipment for faster, realistic testing.

FPGA prototyping: Implementation of a design on programmable hardware for experimentation and software development.

Design for test: Techniques that improve controllability and observability for manufacturing tests.

Clock-domain crossing: Transfer of information between domains driven by unrelated or differently timed clocks.

Co-verification: Joint verification of hardware, firmware, and software behavior.

Coverage closure: The reviewed completion of defined coverage goals with justified treatment of gaps.

Review Questions

Short Answer Questions

1. Why must a hardware requirement be measurable and traceable?

2. What is the role of a scoreboard in simulation-based verification?

3. Distinguish setup violations from hold violations.

4. Why are formal assumptions reviewed for vacuity?

5. What is the purpose of design-for-test techniques?

Long Answer Questions

1. Explain the progression from requirements analysis through RTL, synthesis, physical implementation, and testing in an ASIC flow.

2. Compare simulation, formal verification, emulation, and FPGA prototyping in terms of speed, observability, coverage, and typical use.

3. Discuss how architectural exploration supports hardware-software partitioning and prevents late design failure.

4. Explain the importance of timing constraints and static timing analysis in a synchronous digital design.

5. Describe a layered verification strategy for an embedded accelerator, including functional, formal, implementation, and software evidence.

Analytical / Application Questions

1. A streaming module loses data only when its downstream consumer applies backpressure. Identify the likely modeling error and propose assertions and tests to isolate it.

2. A design achieves 98% code coverage but has never exercised simultaneous DMA, interrupt, reset, and processor register access. Evaluate the coverage claim and recommend additional evidence.

3. An FPGA prototype meets functional requirements but misses its target frequency after synthesis. Analyze possible causes and propose changes at the architectural, RTL, constraint, and physical levels.

22. Multiple Choice Questions with Answers

Question 1

Which statement best describes the purpose of requirement traceability in a hardware project?

A. It links requirements to design elements, verification activities, and acceptance evidence.

B. It guarantees that synthesis will produce the smallest possible circuit.

C. It replaces the need for simulation and formal verification.

D. It records only the final physical layout of the chip.

Correct Answer: A. It links requirements to design elements, verification activities, and acceptance evidence.

Question 2

A streaming interface transfers data on a cycle only when valid and ready are both asserted. Which testbench assumption would most likely conceal a packet-loss defect?

A. A transfer occurs whenever valid is asserted, regardless of ready.

B. The monitor records every accepted transaction.

C. The scoreboard models pipeline latency explicitly.

D. The testbench applies randomized backpressure.

Correct Answer: A. A transfer occurs whenever valid is asserted, regardless of ready.

Question 3

Which verification approach is most suitable for proving that two requesters can never receive a shared resource grant simultaneously?

A. A waveform inspection of one directed test

B. A formal assertion checked over the modeled state space

C. A synthesis utilization report

D. A manufacturing scan test

Correct Answer: B. A formal assertion checked over the modeled state space

Question 4

What is the principal danger of declaring a false path merely to remove a timing violation?

A. It may conceal a path that is functionally or temporally significant.

B. It always increases dynamic power by a fixed amount.

C. It prevents all RTL simulation from completing.

D. It converts an FPGA design into an ASIC design.

Correct Answer: A. It may conceal a path that is functionally or temporally significant.

Question 5

Which result provides the strongest evidence that meaningful behaviors, rather than merely lines of code, have been exercised?

A. High functional coverage supported by reviewed scenarios and coverage goals

B. A large number of randomly generated transactions with no checking

C. Successful compilation of every RTL file

D. A reduction in the number of waveform signals

Correct Answer: A. High functional coverage supported by reviewed scenarios and coverage goals

Question 6

A setup violation is observed on a synchronous path. Which change could directly help by reducing the time required for combinational evaluation?

A. Increasing the logic depth between registers

B. Adding or restructuring pipeline stages

C. Removing all clock definitions from the constraints

D. Disabling the receiving register

Correct Answer: B. Adding or restructuring pipeline stages

Question 7

Why is hardware-software co-verification necessary for a memory-mapped accelerator?

A. Software behavior depends on register semantics, interrupts, ordering, and DMA interactions.

B. Software can determine transistor leakage without hardware models.

C. It eliminates the need for hardware timing analysis.

D. It ensures that every possible RTL state is simulated.

Correct Answer: A. Software behavior depends on register semantics, interrupts, ordering, and DMA interactions.

Question 8

Which statement correctly characterizes FPGA prototyping?

A. It proves correctness for every possible ASIC physical condition.

B. It can support realistic workloads and fast execution but may differ in timing and available resources.

C. It is always slower than RTL simulation.

D. It is used only for manufacturing defect screening.

Correct Answer: B. It can support realistic workloads and fast execution but may differ in timing and available resources.

Question 9

A formal property passes immediately, but its assumptions prohibit all legal transactions. What is the most appropriate interpretation?

A. The design is proven correct in all operating conditions.

B. The property may be vacuous and its assumptions require review.

C. The synthesis tool has optimized the property into hardware.

D. The testbench has achieved complete functional coverage.

Correct Answer: B. The property may be vacuous and its assumptions require review.

Question 10

Which combination most appropriately supports a credible verification exit decision?

A. Zero test failures alone

B. High code coverage alone

C. Passing tests, reviewed coverage, justified formal results, clean implementation checks, and requirement traceability

D. A successful compilation followed by physical packaging

Correct Answer: C. Passing tests, reviewed coverage, justified formal results, clean implementation checks, and requirement traceability