Design & Formal Verification of Parameterizable Fixed-Point CORDIC IP
SystemVerilog
Verilog
Mircoarchitecture
Pipelining
Formal Verification
IP Packaging
| Repository | Mummanajagadeesh/cordic-algorithm-verilog |
|---|---|
| Start Date | Dec 2024 |
Summary
| Item | Description |
|---|---|
| Type | Fully synthesizable fixed-point CORDIC Soft IP |
| Modes | 6 modes (Rotation/Vectoring × Linear/Circular/Hyperbolic) |
| Focus | Parameterization, numerical characterization, formal verification |
| Precision | ~\(10^{-5}\) RMS (@ 32-bit, 16 iterations) |
| Verification | SVA + SymbiYosys (Yices2 backend) |
Core Features
- Shift–add iterative datapath (no multipliers)
- 6 operating modes across 3 coordinate systems
- Deterministic latency: \( \text{ITER} + 1 \) cycles
- Clean
start / busy / validhandshake - Fully parameterized width, iterations, angle precision, scaling
- Python auto-generation of LUTs and parameter headers
- FuseSoC packaged IP
- Formal verification of control and structural invariants
- Drop-in architectural variants (iterative, pipelined, SIMD, multi-issue)
- Demonstrated integration in QAM16 demodulator
Operating Modes
| Architecture ↓ / Algorithm → | Rotation Mode (Forward) | Vectoring Mode (Inverse / Reduction) |
|---|---|---|
| Linear | mult | div |
| Circular | sin, cos, tan | atan2, magnitude |
| Hyperbolic | sinh, cosh, tanh, exp | ln |
Parameterization
| Parameter | Description |
|---|---|
WIDTH | Internal fixed-point datapath width |
ITER | Iteration depth |
ANG_FRAC | Angle fractional precision |
OUT_WIDTH | Output width |
SHIFT | Deterministic scaling/truncation control |
Trade-offs explored between accuracy, latency, and area.
Accuracy Characterization
Circular Rotation (sin/cos)
Configuration:
- \( \text{WIDTH} = 32 \)
- \( \text{ITER} = 16 \)
Results:
- RMS error ≈ \( 3.9 \times 10^{-5} \)
- Max error ≈ \( 7 \times 10^{-5} \)
Circular Vectoring (Magnitude)
- RMS error ≈ \( 2.6 \times 10^{-5} \)
Linear Mode (mult/div)
- Rapid convergence
- Error dominated by final truncation
- Stable across full dynamic range when prescaled
Hyperbolic Mode
- Scheduled repeated iterations required
- ~\(10^{-5}\) absolute error typical
- Limited by argument range reduction and scaling
Known Numerical Sensitivities
| Issue | Cause |
|---|---|
| Amplitude collapse | Underscaled outputs |
| Instability | Overscaled internal widths |
| Systematic bias | Incorrect gain compensation |
| Clipping / sign inversion | Mismatched output shifts |
tan(x) instability | Near \( \pm \pi/2 \) |
atan2 sensitivity | Near \( (0,0) \) |
Iterative Update Equations
Rotation Mode
\[ x_{i+1} = x_i - d_i (y_i \gg i) \]
\[ y_{i+1} = y_i + d_i (x_i \gg i) \]
\[ z_{i+1} = z_i - d_i \tan^{-1}(2^{-i}) \]
\[ d_i = \begin{cases} +1 & z_i \ge 0 \ -1 & z_i < 0 \end{cases} \]
Vectoring Mode
\[ x_{i+1} = x_i + d_i (y_i \gg i) \]
\[ y_{i+1} = y_i - d_i (x_i \gg i) \]
\[ z_{i+1} = z_i + d_i \tan^{-1}(2^{-i}) \]
\[ d_i = \begin{cases} +1 & y_i \ge 0 \ -1 & y_i < 0 \end{cases} \]
Wrapper Semantics
Wrappers provide:
- Gain compensation
- Deterministic scaling
- Format conversion
- Mode-specific preconditioning
| Function | Output Mapping |
|---|---|
sin | final \( y \) |
cos | final \( x \) |
tan | ratio \( y/x \) |
mag | final \( x \) |
atan2 | accumulated \( z \) |
exp, ln | hyperbolic wrappers |
Correct scaling is mandatory to prevent saturation or collapse.
Formal Verification
Scope: Core iteration engine and control FSM
Tools: SymbiYosys + Yices2
Assertions: SystemVerilog Assertions (parametric)
Proven Structural Properties
- Single-cycle
start - Non-overlapping transactions
- Bounded progress \( \le ITER + 1 \)
- Deadlock-free execution
- Input stability while
busy - Output range safety
Rotation Mode Properties
- Odd/even symmetry
\( \sin(-x) = -\sin(x) \)
\( \cos(-x) = \cos(x) \) - Local monotonicity near zero
- Sign consistency
Vectoring Mode Properties
- Magnitude symmetry across quadrants
- Correct zero-vector handling
- \( \text{atan2} \) odd symmetry
- \( \pi \)-rotation consistency
Note: Numerical precision is validated through simulation, not formal proof.
Drop-In CORDIC Core Families
Family A — Iterative / Control-Oriented
| Core ID | Description | Purpose |
|---|---|---|
| A1 | Iterative rolled | Minimum-area baseline |
| A2 | Iterative unrolled | Reduced latency |
| A3 | 2-stage micro-pipeline | Shorter critical path |
| A4 | 3-stage micro-pipeline | Higher Fmax |
Family B — Throughput / Feed-Forward
| Core ID | Description | Purpose |
|---|---|---|
| B1 | Fully unrolled | 1 result/cycle |
| B2 | 2-stage pipeline | Balanced throughput |
| B3 | Balanced 2-stage | Even stage distribution |
| B4 | 3-stage deep pipeline | High-frequency design |
Family C — SIMD / Spatial
| Core ID | Description | Purpose |
|---|---|---|
| CS | Scalar unrolled | Reference |
| CR2 | Replicated ×2 | Dual lane |
| CR4 | Replicated ×4 | Quad lane |
| CSR4 | Shared ROM quad | Area optimized |
| CVEC4 | Packed SIMD | Vector datapath |
| CVEC5 | Refined SIMD | Shared resource optimized |
Family D — Multi-Issue / Time-Interleaved
| Core ID | Description | Purpose |
|---|---|---|
| D2X2S | 2 issues × 2 lanes | Dual issue |
| D4X2S | 2 issues × 4 lanes | Wider SIMD |
| D4X2P | 2 issues × 4 lanes + pipeline | Improved Fmax |
| D4X4S | 4 issues × 4 lanes | High concurrency |
Toolchain
| Tool | Role |
|---|---|
| Verilog | RTL design |
| SVA | Formal property specification |
| SymbiYosys | Formal verification engine |
| Yices2 | SMT backend |
| Icarus Verilog | Simulation |
| Python | LUT generation & parameter sweeps |
| FuseSoC | Packaging & integration |