jagadeesh97@root:~$

Formal Verification Coverage for CORDIC IP and Wrappers

This document describes the scope and intent of the formal verification collateral for the CORDIC IP and its wrappers.
The verification focuses on functional safety, protocol correctness, and mathematical invariants, not on high-precision numerical accuracy.

The CORDIC is verified in two operating modes:

  • Rotation mode
    • sin
    • cos
    • tan
    • combined sin/cos/tan wrapper
  • Vectoring mode
    • magnitude
    • atan2

Only properties that are structurally guaranteed by a correct CORDIC implementation are asserted.

Common Verification Themes (All Modules)

All formal modules share the following guarantees:

1. Handshake Correctness

  • start is a single-cycle pulse
  • No new start is allowed while busy is asserted
  • valid is a single-cycle pulse
  • valid never overlaps with a previous valid

2. Progress / Termination

  • Once started, the operation must complete within ITER + 1 cycles
  • No deadlock or infinite busy condition is possible

3. Input Stability

  • All symbolic inputs (angle, x_in, y_in) are assumed stable while busy is high
  • Inputs are latched at start and compared against the final output

4. Numerical Safety

  • Outputs are always within their declared signed range
  • Saturation limits (where applicable) are explicitly checked

Rotation Mode Verification

Rotation mode verifies trigonometric functions driven by an input angle.

1. cordic_sine_formal

Verified properties:

  • Output range is representable in SIN_COS_OUT_WIDTH
  • Odd symmetry
    • sin(-x) = -sin(x)
  • Local monotonicity near zero
    • For small angles around 0, sine is strictly increasing
  • Structural correctness only; no absolute sine values are checked

What is intentionally not checked:

  • Exact sine magnitude
  • Quadrant correctness outside the small-angle window

2. cordic_cos_formal

Verified properties:

  • Output range safety
  • Even symmetry
    • cos(-x) = cos(x)
  • Local monotonicity near zero
    • Cosine decreases as angle increases near 0

What is intentionally not checked:

  • Exact cosine value at any angle
  • Global periodic behavior

3. cordic_tan_formal

Verified properties:

  • Output saturation behavior matches design limits
  • Odd symmetry
    • tan(-x) = -tan(x)
  • Local monotonicity near zero
    • Tangent increases near 0

Assumptions:

  • Verification avoids angles close to ±π/2 using a small-angle window

What is intentionally not checked:

  • Exact slope of tangent
  • Asymptotic behavior near π/2

4. cordic_trig_formal (Cross-Consistency Wrapper)

This module verifies consistency across sine, cosine, and tangent computed in parallel.

Verified properties:

  • All three results assert valid on the same cycle
  • Outputs remain within a realistic magnitude guard band
  • Local sign consistency
    • Sign of sin matches angle sign near zero
    • cos remains positive near zero
    • Sign of tan matches sin / cos sign expectations

Purpose:

  • Detect internal sign, quadrant, or pipeline misalignment bugs
  • Catch mismatched scaling or control errors between blocks

Vectoring Mode Verification

Vectoring mode verifies magnitude and angle extraction from (x, y) inputs.

5. cordic_mag_formal

Verified properties:

  • Progress and termination
  • Even symmetry
    • |x, y| = |-x, y| = |x, -y| = |-x, -y|
  • Zero vector
    • (0, 0) produces magnitude 0

What is intentionally not checked:

  • Exact Euclidean length
  • Scaling constant accuracy

6. cordic_atan2_formal

Verified properties:

  • Progress and handshake correctness
  • Odd symmetry in Y
    • atan2(-y, x) = -atan2(y, x)
  • 180-degree rotation symmetry
    • atan2(-y, -x) = atan2(y, x) ± π
  • Correct handling of quadrant transitions modulo π

What is intentionally not checked:

  • Exact angular value
  • Zero-vector angle definition (left optional)

Intent

This formal suite is designed to:

  • Prove the CORDIC control logic is correct
  • Prove the mathematical structure of the implementation is sound
  • Catch sign, symmetry, scaling, and sequencing bugs
  • Remain fully parametric and scalable with word width and iteration count

Numerical accuracy validation is intentionally delegated to simulation or software reference testing.