Two-flop CDC synchronizer
A CDC task: implement a safe 2FF synchronizer, check reset assumptions, and record proof limitations.
D3 · 50–110 min · verilator, symbiyosys
How results are checked
Run this challenge on your computer. The site validates the structure of report.json. A submitted report alone does not prove that the task was completed.
Goal and prerequisites
- 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.
- Basic clock-domain-crossing concepts.
- Understanding of nonblocking assignments in SystemVerilog.
Challenge package
Version, licence and checksum
CC-BY-4.0 · MIT · FPGA.camp
- version
- 1.0.0
- size
- 292 bytes
- sha256
- 707ee5daa8f291bd990e5ee37ad6b2d7e32f81f73e5f4a69f0bf3a37c5fafc7b
Run locally
Lint and smoke simulation
make lint sim
SymbiYosys proof
make formal
CDC report.json
make check
Criteria and common mistakes
Scoring rubric
| id | criterion | points | required | evidence_path |
|---|---|---|---|---|
| structure | Two sequential stages are used | 35 | yes | checks.structure |
| reset-assumptions | Reset assumptions are checked explicitly | 25 | yes | checks.reset_assumptions |
| scope-limits | CDC solution limits are recorded in the report | 40 | yes | checks.scope_limits |
- 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.
Validate report.json
Choose a local check report, up to 512 KB. Source code and archives are not needed.