Free and Open Source Silicon Foundation

Mentors: Student: Xuhai Chang

Booting Linux in OpenPiton's Verilator RTL simulation takes days. This project builds a checkpoint/restore pipeline: boot Linux in QEMU (minutes), extract machine state, convert it to OpenPiton's `mem.image` format, and resume execution in RTL simulation with Linux already running.

Mentors: Student: Seongwon Jo

This project aims to bring Ariane+OpenPiton closer to RISC-V RVA23 compliance by adding support for the Svadu extension. By enabling hardware-managed Accessed and Dirty bit updates, Svadu eliminates unnecessary software-managed page faults and improves virtual-memory efficiency. I will implement the required changes across the PTW, TLBs, LSU-side update path, and a new hardware unit, Page Table Entry Updating Engine (PUE), while building a robust verification framework based on Spike, Verilator, and handwritten assembly tests. In addition to a complete Svadu implementation, the project will deliver evaluation results, reusable verification infrastructure, and upstream-ready contributions for future RISC-V MMU-related RVA23/RVB23 extensions.

Mentors: Student: Muhammad Rayyan Khan

Millions of lines of open-source Verilog exist but remain verbose and hard to maintain. TL-Verilog offers a cleaner abstraction, but almost none of this codebase has been converted. This project strengthens the LLM-driven conversion pipeline in the conversion-to-TLV repository by improving error recovery, refining prompt recipes for complex Verilog patterns (FSMs, parameterized modules, arithmetic pipelines), and applying the flow to real open-source modules including RISC-V components. All conversions are formally verified using SymbiYosys and EQY, generating high-quality training data for future LLM improvement. Deliverables include a fast working failure-classification system, improved prompts.json recipes, 10+ converted and verified modules, and structured training data registered in the project repository.

Mentors: Student: Shri Vishakh Devanand

circt-bmc can already prove when an assertion is falsifiable, but it does not yet produce the counterexample trace format hardware developers rely on for debugging. Today, users get a SAT/UNSAT result without a practical cycle-by-cycle waveform showing how the design reached failure. This project adds that missing debugging path. I will preserve meaningful signal identities before lowering, track the corresponding solver expressions across BMC timesteps, and evaluate those expressions against the first satisfying Z3 model. The implementation is intentionally staged: first a readable text counterexample for the failing prefix, then VCD waveform generation from the same trace data. The focus is the first-failure prefix (cycle 0 to the violating step), which delivers high user value with low integration risk and clean upstreamability. Deliverables: 1. Signal tracking and naming pipeline for user-relevant values (ports, externalized registers, selected internals where remapping is reliable). 2. A BMC trace runtime component that records per-step solver ASTs and supports model-driven trace emission. 3. Midterm milestone: first-failure text counterexample dump. 4. Final milestone: VCD waveform output for the same counterexample path, exposed through circt-bmc CLI flags. 5. Upstream-quality tests and documentation (IR-level + end-to-end regressions, including failing and no-violation cases).

Mentors: Student: Kutikuppala Deekshita

This proposal focuses on enhancing the Surfer waveform viewer by adding support for memory and wide array visualization. Current waveform views are effective for scalar signals but become inefficient when dealing with large arrays or memory structures. This project introduces a structured table based visualization for memory contents along with intelligent change highlighting across timestamps. The implementation will improve debugging efficiency by allowing users to inspect memory elements individually rather than scanning entire waveforms. The solution integrates seamlessly with Surfer existing architecture and maintains performance for large datasets.