AutoVeriFix+: High-Correctness RTL Generation via Trace-Aware Causal Fix and Semantic Redundancy Pruning

This set of papers advances correctness and testing for hardware, runtime monitoring, and formal tools with implications for system safety and trust. AutoVeriFix+ is a three-stage LLM-driven RTL-generation and repair pipeline that (1) creates Python reference models, (2) generates and iteratively fixes Verilog RTL, and (3) uses a concolic testing engine with cycle-accurate traces to expose sequential corner cases and enable trace-aware semantic pruning (reports >80% functional correctness and ~25% redundant-logic elimination). A separate paper presents Once4All, an LLM-assisted SMT-solver fuzz