nextvertex

is a streaming BFS frontier expander for unweighted graphs. Given the current frontier $$F_t$$ and a global visited bitset, it reads neighbors, atomically test-and-sets visited[v], and emits a vertex precisely once. The core is a fixed-II=1 pipeline that sustains one neighbor per cycle after fill, with deterministic latency and no duplicates.

Suggested reading

1. Dr. BFS: Data Centric Breadth-First Search on FPGAs
2. Direction-Optimizing Breadth-First Search
3. SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
4. Refinement Types for Haskell
5. FPGP: Graph Processing Framework on FPGA
6. Boosting the Performance of FPGA-based Graph Processor using Hybrid Memory Cube: A Case for Breadth First Search
7. Under the hood of Formal Verification
8. ThunderGP: HLS-based Graph Processing Framework on FPGAs
9. Graph Processing on FPGAs: Taxonomy, Survey, Challenges