HLS verification should establish one traceable chain of evidence: an agreed functional model is exercised by a self-checking, requirements-based testbench; the synthesizable C++ is checked at C level; the generated RTL is compared with it; and the RTL then passes the same implementation checks as any hand-written block. No single test or tool replaces that chain.
Read the diagram as steps
Build a traceable evidence chain
- Reference modelDefine behavior, ranges, rounding and tolerance.
- Bit-accurate C++Run self-checking tests, boundary cases and regressions.
- C simulationDebug functionality with sanitizers and continuous integration.
- C / RTL compareCheck co-simulation, equivalence and interface behavior.
- RTL sign-offComplete coverage, lint, CDC, synthesis and timing checks.
Start with an executable contract
The reference model defines what “correct” means. It may be the customer's existing C, C++, Python, MATLAB, or SystemC model, but its assumptions must be explicit: accepted input ranges, frame boundaries, state between calls, reset behavior, ordering, rounding, saturation or wraparound, and responses to invalid input. If those points remain implicit, two individually reasonable implementations can disagree.
Keep the reference independent of the synthesizable implementation where practical. Reusing the same helper code in both sides can create a common-mode bug that always compares equal. A feasibility study is a good place to freeze this contract, identify unavailable test vectors, and agree which results are exact and which use a stated tolerance.
Build a reusable C++ testbench
A good C++ testbench drives transactions, invokes the design under test, compares every meaningful output with the reference, and exits non-zero on failure. It should report the seed, transaction, expected value, actual value, and relevant context so a failure is reproducible. Directed cases cover requirements and known boundaries; constrained-random cases explore combinations that were not anticipated. Save random seeds or generated vectors for regression and RTL reuse.
Tests should include zero and full-scale values, signed boundaries, minimum and maximum lengths, reset and restart, empty and back-to-back traffic, legal stalls, and state carried across calls. Protocol-aware tests also vary ready/valid timing and memory response behavior rather than presenting an always-ready environment.
Make numeric behavior bit-accurate
Hardware precision is part of the function. Check every conversion between floating point, fixed point, and integer types; confirm intermediate widths; and test rounding, truncation, saturation, sign extension, overflow, and underflow at their boundaries. A floating-point algorithmic model can remain the quality reference, while a separate bit-accurate model explains the exact result expected from the hardware. Record tolerances in the verification plan rather than adding them ad hoc when a test fails.
Use C simulation first, then C/RTL co-simulation
C simulation is the main functional debug loop. Run it in continuous integration with warnings enabled and, where the compiler supports them, sanitizers that expose undefined behavior, invalid shifts, out-of-bounds accesses, and uninitialised data. C simulation does not prove that the synthesized interface, reset logic, latency, or backpressure behavior is correct, so it is necessary but not sufficient.
C/RTL co-simulation reuses the C++ testbench to drive generated Verilog or VHDL and compare its outputs. The regression should include more than a smoke vector: exercise multiple transactions, stalls, pipeline fill and drain, reset, and representative frame lengths. Review measured latency and initiation interval as well as pass/fail. Vendor restrictions matter; for example, AMD documents both its automatic RTL verification flow and interface-specific co-simulation requirements.
Use formal and equivalence where they fit
Formal checking can complement simulation by reasoning over all values allowed by its assumptions. Depending on the tool and flow, it may compare high-level source with RTL, compare alternative RTL scenarios, or prove interface and safety properties. This is not one interchangeable “equivalence” step: C++-to-RTL sequential equivalence differs from RTL-to-gate logical equivalence.
Before relying on a proof, document the compared models, black boxes, memories, reset assumptions, environmental constraints, and any unsupported constructs. An inconclusive proof is not a pass. Siemens describes high-level coverage and C++/SystemC equivalence capabilities in its Catapult verification overview; applicability still depends on the selected flow and design.
Close coverage against requirements
Compiler line, branch, condition, and expression coverage can expose untested C++ paths, but structural coverage alone cannot show that the specification was tested. Maintain functional coverage for operations, modes, numeric ranges, frame sizes, state transitions, errors, interfaces, and meaningful crosses between them. Link coverage points and directed tests to requirements.
At RTL, use appropriate code coverage, assertions, protocol checkers, and functional coverage. Generated RTL structure can change when constraints or tool versions change, so unexplained percentage targets are fragile. Closure means reviewing every uncovered item, adding a test where it represents useful behavior, and documenting a technically justified exclusion where it does not.
Apply normal RTL sign-off before handoff
Generated RTL still enters the standard ASIC or FPGA flow. Run lint and review tool-generated waivers. Check clock-domain and reset-domain crossings against the integrated clocking architecture. Synthesize against the intended libraries or device, validate clocks and I/O delays, and justify every false or multicycle path. Review timing, resource or area reports, memory inference, reset implementation, interface assertions, and any tool warnings that could affect integration.
This downstream evidence is especially important during an RTL-to-HLS migration, where preserved behavior and intentional interface or latency changes must be distinguished. The broader HLS flow overview explains where verification sits, while Videalt's HLS verification service covers hands-on testbench and sign-off support.
Typical verification deliverables
- Verification plan and traceability from requirements to tests and coverage
- Reference-model contract, bit-accurate model, synthesizable source, and build scripts
- Self-checking testbench, deterministic regressions, seeds, vectors, and expected results
- C simulation, co-simulation, coverage, synthesis, lint, CDC, and timing reports
- Generated RTL, constraints, justified waivers, known limitations, and integration notes
Buyer FAQs
Is C/RTL co-simulation enough to sign off an HLS block?
No. Co-simulation is important evidence that the generated RTL matches the tested C++ behavior, but sign-off also needs requirements-based tests, coverage closure, interface and reset verification, and the project's normal RTL checks such as lint, CDC, synthesis, and timing analysis.
Can an existing software model be used as the HLS reference model?
Usually, provided its behavior is defined for the hardware's numeric precision, overflow, rounding, framing, and error cases. Keep an independent reference where practical so the implementation and checker do not share the same mistake.
When is formal equivalence useful in an HLS project?
It is useful when a supported tool can prove correspondence across the abstraction or transformation being checked, particularly for broad input spaces that simulation cannot exhaust. Confirm the supported language, memory, interface, and scheduling assumptions before making the proof a sign-off requirement.
What verification deliverables should an HLS supplier provide?
Agree the list before work starts. A useful handoff normally includes the reference-model contract, synthesizable source, reproducible test environment, regression inputs or seeds, coverage and co-simulation reports, generated RTL, constraints, sign-off results, justified waivers, and integration notes.
