Generate Counter Examples for Bounded Model Checks in CIRCT

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).