edu.fpga.camp

Two-flop CDC synchronizer

A CDC task: implement a safe 2FF synchronizer, check reset assumptions, and record proof limitations.

30-second task brief

Required tools
verilator, symbiyosys
What to download
Challenge package
What to run
make check
Success condition
At least 80/100 and no blocking report errors.

Challenge parameters

D3CDCCC-BY-4.0verilatorsymbiyosys
HDL languages
SystemVerilog
Vendor family
Estimated time
50-110 min
Score
pass 80 / max 100
Authors
FPGA.camp
Updated
2026-05-19

Learning outcomes

  • Explain that a 2FF synchronizer only addresses single-bit CDC.
  • Record reset assumptions separately from datapath behavior.
  • Separate a formal interface proof from an MTBF estimate.

Prerequisites

  • Basic clock-domain-crossing concepts.
  • Understanding of nonblocking assignments in SystemVerilog.

Files

  • challenge.yaml
  • rtl/sync_2ff.sv
  • formal/sync_2ff.sby
  • checks/run.sh

How to run

Lint and smoke simulation

make lint sim

SymbiYosys proof

make formal

CDC report.json

make check

Scoring rubric

idcriterionpointsrequiredevidence_path
structureTwo sequential stages are used35yeschecks.structure
reset-assumptionsReset assumptions are checked explicitly25yeschecks.reset_assumptions
scope-limitsCDC solution limits are recorded in the report40yeschecks.scope_limits

Common mistakes

  • Synchronizing a multi-bit bus without a handshake.
  • Letting reset cross a clock domain without separate analysis.
  • Claiming MTBF without source frequencies and tau parameters.

Challenge package

version
1.0.0
size
292 bytes
sha256
707ee5daa8f291bd990e5ee37ad6b2d7e32f81f73e5f4a69f0bf3a37c5fafc7b
Download package

Validate report.json

Upload the report produced by the local runner. The server validates only normalized JSON and never runs HDL, Tcl, shell scripts, or EDA tools.

  • Accepted: one report.json file, maximum 512 KB.
  • Rejected: HDL, Tcl, zip archives, waveforms, full logs, absolute paths, and embedded source code.

Contribute / fix