|
1 | 1 | # Competitive Positioning: IGLA CODER and IGLA RACE |
2 | 2 |
|
3 | | -**Date:** 2026-06-16 |
| 3 | +**Date:** 2026-06-17 |
4 | 4 | **Scope:** Sub-1B code generation LLMs and formally verified RTL/hardware generation |
5 | 5 | **Status:** Active surveillance and differentiation analysis |
6 | 6 |
|
|
17 | 17 | | **OUROBOROS Kernel Mint** (June 2026) | 1B (MiniCPM5) | MIT | Triton GPU kernels | GPU edge | Referee architecture (compile+correctness+benchmark); limited to GPU kernels, not general code | |
18 | 18 | | **CodeAlchemy** (arXiv:2606.10087) | Various teachers | Unknown | 976.6B tokens verified | No (training corpus) | Execution-verified synthetic data; not a deployable model | |
19 | 19 | | **EdgeRazor** (arXiv:2605.04062, May 2026) | 1.88-bit mixed-precision | Unknown | Qwen3 / MobileLLM compression | Yes (up to 7.03×) | Mixed-precision quantization-aware distillation; not code-specific but erodes edge advantage | |
| 20 | +| **EffiSkel** (arXiv:2606.06821, June 2026) | 770M–1.5B | Unknown | Efficiency skeleton supervision (AST + profiler) | No | Structural supervision for efficiency-critical code; no sacred/hardware awareness | |
| 21 | +| **RLVR** (arXiv:2605.30478, Mar 2026) | 0.6B–1B | Unknown | RL with unit-test + static-analysis feedback | Yes | +13pp MBPP Pass@1 on Qwen3-0.6B; no hardware focus | |
| 22 | +| **LLM4RTL** (arXiv:2606.15500, June 2026) | Various | Unknown | Tool-assisted RTL (JRCRC pipeline + Karnaugh maps) | No | Tabular-data preprocessing for RTL LLMs; no formal verification | |
20 | 23 | | **EfficientLLM** (arXiv:2502.06663) | 100M-1B | Unknown | General edge LLM | Yes | Pruning-aware pretraining; not code-specific | |
21 | 24 |
|
22 | 25 | ### Key Threat Assessment |
|
27 | 30 |
|
28 | 31 | **HIGH:** OUROBOROS Kernel Mint demonstrates that a 1B model can beat `torch.compile` with an execution-verified referee. This validates the "referee is the product" approach but is limited to Triton GPU kernels. |
29 | 32 |
|
| 33 | +**HIGH:** EffiSkel (June 2026) extracts efficiency skeletons (lexical, AST, profiler-based) to supervise multi-task learning on CodeT5-770M and Qwen2.5-Coder-1.5B, improving both Pass@1 and runtime efficiency. Demonstrates that structural supervision pushes sub-1B models toward larger-model performance. |
| 34 | + |
| 35 | +**HIGH:** RLVR (March 2026) applies Reinforcement Learning with Verifiable Rewards to Qwen3-0.6B and Llama3.2-1B using unit-test and static-analysis feedback, achieving +13 percentage points on MBPP Pass@1. Shows sub-1B models can be dramatically improved with execution-aware RL. |
| 36 | + |
| 37 | +**HIGH:** LLM4RTL (June 2026) introduces a JRCRC pipeline and tabular-data preprocessing (waveforms, truth tables, Karnaugh maps) to help LLMs infer logical relations for RTL generation. Expands the tool-assisted RTL generation space. |
| 38 | + |
30 | 39 | **MEDIUM:** DebateCoder shows multi-agent collaboration improves small models, but no hardware integration. |
31 | 40 |
|
32 | 41 | ### Trinity Differentiation Strategy |
33 | 42 |
|
34 | 43 | 1. **Sacred Opcode Embedding:** IGLA-Coder embeds awareness of the IGLA RACE hardware alphabet (OP_LOAD_PHYSICS_CONST ... OP_AVS_RECONF) into token embeddings. No competitor has hardware-software co-design at the model architecture level. |
35 | | -2. **Formal Verification Pipeline:** Generated code is checked against Coq/Rocq proof obligations for RTL and Rust `unsafe`-free guarantees. MiniCPM5-1B has zero formal verification. |
36 | | -3. **R-SI-1 Compliance:** For Verilog/VHDL generation, IGLA-Coder enforces multiplier-free RTL (no `*` in assignments) via constrained decoding. No competitor enforces hardware constraints at generation time. |
37 | | -4. **Spec-First Corpus:** Training data follows `.t27` specification-first taxonomy (CodeAlchemy 5-strategy + sacred opcode augmentation). Competitors use generic web-scale corpora. |
| 44 | +2. **Process Reward Model (PRM):** `specs/igla/coder/prm.t27` defines step-level verifiable rewards (syntax, lint, sacred compliance, simulation, synthesis) with phi-weighted scoring. Unlike StepPRM-RTL's sparse outcome rewards, Trinity's PRM provides dense per-step feedback with sacred-geometry weighting. |
| 45 | +3. **Formal Verification Pipeline:** Generated code is checked against Coq/Rocq proof obligations for RTL and Rust `unsafe`-free guarantees. MiniCPM5-1B has zero formal verification. |
| 46 | +4. **R-SI-1 Compliance:** For Verilog/VHDL generation, IGLA-Coder enforces multiplier-free RTL (no `*` in assignments) via constrained decoding. No competitor enforces hardware constraints at generation time. |
| 47 | +5. **Spec-First Corpus:** Training data follows `.t27` specification-first taxonomy (CodeAlchemy 5-strategy + sacred opcode augmentation). Competitors use generic web-scale corpora. |
38 | 48 |
|
39 | 49 | --- |
40 | 50 |
|
|
51 | 61 | | **StepPRM-RTL** (arXiv:2606.04246, June 2026) | IBM Research | Step-level PRM + MCTS + RAFT | Verilog, VHDL | 0.857 Pass@1 on VerilogEval-v2-EXT | **HIGH** | |
52 | 62 | | **Alpha-RTL** (arXiv:2606.05253, June 2026) | PUCT search | Test-time training + EDA-in-the-loop | Verilog | 65.1% geometric-mean PPA reduction | **HIGH** | |
53 | 63 | | **Veri-Sure** (arXiv:2601.19747, Jan 2026) | Multi-agent | Temporal tracing + SymbiYosys/Z3 equivalence | Verilog | 93.3% functional pass on VerilogEval-v2-EXT | **HIGH** | |
| 64 | +| **Interaction Tree Semantics for RISC-V** (arXiv:2605.04933, May 2026) | Rocq/Coq | Interaction Trees (ITrees) + cross-level bisimulation | Verilog | RV32/64I+M+F+A+Zicsr + Sv32/39/48/57; 131 correctness lemmas; passes official RISC-V test suite | **HIGH** | |
54 | 65 | | **GLSVLSI 2026** (arXiv:2603.11287) | Yosys + Nangate45 | Synthesis-in-the-loop evaluation | Verilog | None (benchmark paper) | **MEDIUM** (meta-threat) | |
55 | 66 |
|
56 | 67 | ### Key Threat Assessment |
|
69 | 80 |
|
70 | 81 | **HIGH:** Veri-Sure (January 2026) is a contract-aware multi-agent framework with Boolean equivalence proofs via SymbiYosys/Z3 and dependency-slicing-guided patching. Achieves 93.3% functional pass on VerilogEval-v2-EXT. Strong alternative to IGLA RACE's verification pipeline. |
71 | 82 |
|
| 83 | +**HIGH:** Interaction Tree Semantics for RISC-V (May 2026) provides machine-checked formal semantics of the full RISC-V ISA (RV32/64I+M+F+A+Zicsr + virtual memory) in Rocq using ITrees. 131 correctness lemmas, cross-level bisimulation with Vellvm (LLVM IR), and hardware refinement proof for a Kôika ALU. Extracted OCaml simulator passes the official RISC-V test suite (172 files, 3,228 cases). Represents a mature, native Rocq formalization competing directly in the verified CPU/processor space. |
| 84 | + |
72 | 85 | **META-THREAT:** GLSVLSI 2026 shows that simulation pass rate overstates hardware readiness by 7.5 HQI points on average. Best-of-5 capability vs single-attempt quality gap is 3.7-22.1 points. This means any LLM-generated RTL (including IGLA-Coder) must pass synthesis-in-the-loop validation, not just simulation. |
73 | 86 |
|
74 | 87 | ### Trinity Differentiation Strategy |
|
0 commit comments