A fully verified, synthesizable hardware CRC engine implementing three industry-standard CRC variants in a single parameterized RTL design. Verified through simulation, formal methods, and physical implementation on the SKY130A process node.
- CRC-8 (poly=0x07, seed=0x00, non-reflected)
- CRC-16/CCITT (poly=0x1021, seed=0xFFFF, non-reflected)
- CRC-32 (poly=0xEDB88320, seed=0xFFFFFFFF, reflected I/O, final XOR=0xFFFFFFFF)
- Byte-serial interface with
start/data_valid/crc_validhandshake - 3-state FSM: IDLE → PROCESSING → DONE
- Back-to-back transaction support
- Mid-stream restart via
startsignal - Fully synchronous design with asynchronous active-low reset
crc_engine/
├── rtl/
│ ├── crc8_core.v # CRC-8 parallel XOR core
│ ├── crc16_core.v # CRC-16/CCITT parallel XOR core
│ ├── crc32_core.v # CRC-32 parallel XOR core (reflected)
│ └── crc_engine.v # Top-level FSM + datapath wrapper
├── tb/
│ ├── crc_engine_tb.v # Self-checking simulation testbench
│ ├── crc_engine_sva.sv # SVA formal assertions
│ ├── crc_formal_top.sv # Formal verification wrapper
│ ├── crc_formal.sby # SymbiYosys configuration
│ ├── gen_vectors.py # Python CRC reference generator
│ ├── gen_crc_rtl.py # CRC-8/16 equation generator
│ └── gen_crc32_v2.py # CRC-32 bit-matrix equation generator
├── synth/
│ └── yosys_synth.log # Yosys synthesis report
└── docs/
└── waveform.png # GTKWave simulation screenshot
Each CRC standard is implemented as a combinational parallel XOR core. For an N-bit CRC with 8-bit input data, each output bit is a Boolean function of the 8 input bits and N current CRC bits. The functions were derived using symbolic bit manipulation (CRC-8/16) and the bit-matrix method (CRC-32).
start
IDLE ─────────► PROCESSING
▲ │
│ │ last_valid & !data_valid
│ ▼
└──── start ── DONE (crc_valid asserted)
The last_valid register (1-cycle delayed data_valid) ensures the final byte's registered CRC update completes before the FSM transitions to DONE.
| Port | Direction | Width | Description |
|---|---|---|---|
clk |
input | 1 | Clock |
rst_n |
input | 1 | Active-low async reset |
crc_sel |
input | 2 | 00=CRC8, 01=CRC16, 10=CRC32 |
start |
input | 1 | Begin new CRC transaction |
data_in |
input | 8 | Input data byte |
data_valid |
input | 1 | Input data valid strobe |
crc_out |
output | 32 | Computed CRC result |
crc_valid |
output | 1 | CRC result valid |
19 test vectors across all three CRC standards using Icarus Verilog:
| Category | Tests | Result |
|---|---|---|
| CRC-8 standard vectors | 2 | PASS |
| CRC-16 standard vectors | 2 | PASS |
| CRC-32 standard vectors | 2 | PASS |
| Single-byte edge cases (0x00, 0xFF) | 6 | PASS |
| Back-to-back transactions | 2 | PASS |
| Mode switch between standards | 2 | PASS |
| FSM control (crc_valid deassertion) | 1 | PASS |
| Mid-stream stall and restart | 1 | PASS |
| Total | 19 | 19/19 PASS |
Run simulation:
iverilog -o sim/crc_sim rtl/crc8_core.v rtl/crc16_core.v rtl/crc32_core.v rtl/crc_engine.v tb/crc_engine_tb.v
vvp sim/crc_simFSM properties proven using SymbiYosys with Z3 SMT solver (k-induction, depth=20):
a_no_valid_in_idle—crc_validnever asserts in IDLE statea_valid_clears_on_start—crc_validcorrectly deasserts whenstartfires
Result: PASS — successful proof by k-induction
sby -f tb/crc_formal.sby| Standard | Input | Expected CRC |
|---|---|---|
| CRC-8 | 123456789 |
0xF4 |
| CRC-16/CCITT | 123456789 |
0x29B1 |
| CRC-32 | 123456789 |
0xCBF43926 |
| Module | Cells | Key primitives |
|---|---|---|
crc8_core |
45 | 34× XOR, 9× XNOR |
crc16_core |
57 | 41× XOR, 12× XNOR |
crc32_core |
203 | 180× XOR, 17× XNOR |
crc_engine (FSM+datapath) |
294 | 70× DFF, 97× MUX |
| Total | 596 |
| Metric | Value |
|---|---|
| Floorplan | 121.9 × 119.68 µm |
| Standard cell library | sky130_fd_sc_hd |
| DRC violations | 0 |
| LVS result | PASS |
| Setup violations | 0 |
| Hold violations | 0 |
| Clock period | 10 ns (100 MHz target) |
| Tool | Version | Purpose |
|---|---|---|
| Icarus Verilog | 12.0 | RTL simulation |
| GTKWave | — | Waveform viewer |
| SymbiYosys | v0.63 | Formal verification |
| Z3 | 4.8.12 | SMT solver |
| Yosys | 0.33 | Synthesis |
| OpenLane | v1.0.2 | RTL-to-GDS flow |
| SKY130A PDK | 0fe599b2 | Process design kit |
| Standard | Polynomial | Seed | Reflected | Final XOR | Check Value |
|---|---|---|---|---|---|
| CRC-8 | 0x07 | 0x00 | No | 0x00 | 0xF4 |
| CRC-16/CCITT | 0x1021 | 0xFFFF | No | 0x00 | 0x29B1 |
| CRC-32 | 0xEDB88320 | 0xFFFFFFFF | Yes | 0xFFFFFFFF | 0xCBF43926 |
Gautam Suresh
B.E. Electronics Engineering — VLSI Design and Technology
Chennai Institute of Technology