Hardware Generation on RTLLM 50 problems
96Compile Success RateCKTFORMALIZER (synth)
Evaluation results
| Method | Links | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| CKTFORMALIZER (synth)loop type=iterative compile-fix with Lean type checking, synthesis feedback=Yosys synthesis in agent loop2026.05 | 96 | 54 | 56.3 | 96 | 96 | 96 | 96 | 52 | 52 | 96 | |
| CKTFORMALIZERloop type=iterative compile-fix with Lean type checking2026.05 | 94 | 40 | 42.6 | 94 | 90 | 90 | 90 | 52 | 50 | 91 | |
| Direct SVmode=single LLM call2026.05 | 92 | 60 | 65.2 | 56 | 56 | 56 | 56 | 46 | 48 | 56 | |
| CodeVmode=instruction-tuned2026.05 | 80 | 32 | 40 | 32 | 30 | 30 | 30 | 26 | 26 | 30.5 | |
| RTLCodermodel size=7B, mode=fine-tuned2026.05 | 70 | 22 | 31.4 | 20 | 20 | 20 | 20 | 18 | 18 | 20 |