I work on RISC-V compiler toolchains, and on proving that low-level systems do what their specifications say. That runs in both directions: upstream patches to LLVM and GCC, RTL I have written and verified myself, and correctness findings in a real RISC-V core, each reproduced in simulation before I file it.

Everything here is reproducible from a single command. I document the tests that fail instead of tuning them away, I report the measurements that contradicted what I expected, and I defer performance claims to real hardware rather than dressing up emulator timings as throughput.

LLVM, RISC-V backend · llvm-project#202201

Fixed an assertion in the RISC-V codegen combine (combineBinOpOfExtractToReduceTree) that crashed on a <1 x i1> operation under zve32x. Found by fuzzing the backend with llvm-stress, reduced with llvm-reduce, diagnosed as a combine asserting where it should have declined. Regression test added, full RISC-V codegen suite passing. Reviewed and approved by a RISC-V LLVM maintainer, and merged

GCC, loop vectorizer · PR tree-optimization/116338

Taught the vectorizer to handle chained first-order recurrences, a missed optimization that left TSVC s255 scalar in GCC while clang vectorized it. Adds a chain-detection function with cycle and value-cycle rejection, and fixes the permute insertion point for chained recurrences. Three new testcases. Bootstrapped and regression tested on x86_64 with no regressions, verified on riscv64 under QEMU with bit-exact output, and confirmed newly vectorizing on aarch64 and armv8l by the Linaro precommit CI.

riscv-dfi. DFI for RISC-V, from the compiler down.

An LLVM 18 pass that instruments every store with a SETDEF and every load with a CHECKDEF against a shadow reaching-definition table. It catches a non-control-data memory corruption that Control-Flow Integrity structurally cannot see, and does not false-positive on legitimate same-object access. Ships with a file-level map for porting the matching hardware extension onto the BSC Sargantana core: decode, check unit at the load-store unit, enforcement at retire, CSR state and fault path, with verified file and line references, and an explicit list of the design decisions it deliberately leaves open. Reproduced on two machines; CI asserts the demo actually traps.

count-mem-ops is the pass that preceded it, counting load and store instructions per function. CI re-derives the expected counts from the raw IR and fails on mismatch.

cam. A parameterised content-addressable memory in SystemVerilog, with the verification it would need before anyone trusted it.

Four entries, 32-bit keys, one comparator per entry. Duplicate keys are resolved deterministically and reported on a status output rather than declared illegal and left undefined, because in a metadata table a duplicate address means the allocator has gone wrong and that is worth surfacing. Five concurrent assertions live in the design rather than in the testbench, so they hold for any instantiation.

Verified three ways, all of it from ./run.sh, all of it on packages you can apt-get install, none of it needing a commercial licence.

Simulation. A reference model written in a deliberately different style from the design, eight directed cases at the corners a CAM actually gets wrong, then 20,000 randomised cycles compared every cycle. 20,020 checks, 0 errors, and thirteen functional coverage bins where the run fails if any bin was never exercised. Identical results under Verilator and Icarus, which are independent implementations, so agreement between them says more than a pass on either alone.

Formal. Every assertion proved for all reachable states by temporal induction, in four configurations, on the SAT engine built into Yosys. That includes the property simulation is worst at reaching, which is completeness: if any valid entry holds the searched key, the CAM must report a hit. A CAM that silently misses is the dangerous failure, not one that over-reports. The proof is also mutation tested, because a proof nothing can falsify proves nothing: five one-line bugs are injected one at a time and the run fails if any of them survives.

Synthesis. A sweep across depth, key width and the output-register setting, reporting cell count and logic depth on two Yosys versions, honest that without a PDK these are not areas in square micrometres. Two negative results are kept in the README rather than quietly removed: the output register did not shorten the measured critical path, and the cleverer priority encoder I tried was worse on both axes because I had replaced one carry chain with another.

Written as the hardware coding challenge for the Sargantana tightly-coupled DFI project, since an associative lookup from an address to the identifier of the instruction that last wrote it is exactly the structure a DFI metadata table is.

Seven findings in the Sargantana core and its CSR module. Six are filed as a paired issue and pull request, and every one was reproduced on the core_tile Verilator simulator, with before-and-after output, before I filed it.

The maintainer has marked three of these for the next release: the Zvbb fix outright, and the two alignment fixes once I added an overlap guard he asked for, which is now in both pull requests and verified at fractional LMUL against the reference model, with the full 315-test ISA suite re-run unchanged.

The last row is not a bug, and that is the point. A randomised differential fuzzer I wrote, which generates RVV programs and compares the core against the spike model the repository already vendors, flagged widening operations raising an illegal instruction above vl = VLMAX/2. The reproducer was minimal and it looked like a defect. Before filing I traced the limit through vset_module.sv:98 into every widening guard in the decoder and concluded BSC had done it deliberately, so the issue says so in its title, asks for a documentation note instead of a fix, and explains the consequence: vsetvli for VLMAX followed by vwadd is what an autovectorizer emits, and it traps.

A portfolio of HPC, scientific, and ML software cross-compiled and forensically verified for riscv64, built on x86_64 with riscv64-linux-gnu-gcc 15.2 and run under qemu-riscv64.

Tooling: verify-rvv-port.sh, a forensic verifier I wrote that statically checks whether a binary's hot path is genuinely vectorized, rather than silently falling back to scalar. It caught an incorrect figure in my own published results before I shipped them, which is exactly why it exists.

Also merged upstream: RuyiSDK packages-index #195 (OpenCV manifest).

6-class CNN for groundnut leaf disease detection. Gold Medal, First Place at Sci Quest 2025, MIT-WPU, against students from all branches and years. Trained, optimized for inference, and deployed live. Try the demo

The INT8-quantized version of this model is what later ran inference on RISC-V via TF Lite, which is how the ML work and the systems work connect.