Text Generation
PEFT
Safetensors
English
lora
qwen2.5-coder
verilog
eda
dft
test-point-insertion
reinforcement-learning
grpo
conversational
Instructions to use SKLP-EDA-LAB/Tesla-Pro-TPI with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- PEFT
How to use SKLP-EDA-LAB/Tesla-Pro-TPI with PEFT:
from peft import PeftModel from transformers import AutoModelForCausalLM base_model = AutoModelForCausalLM.from_pretrained("Qwen/Qwen2.5-Coder-7B-Instruct") model = PeftModel.from_pretrained(base_model, "SKLP-EDA-LAB/Tesla-Pro-TPI") - Notebooks
- Google Colab
- Kaggle
File size: 26,051 Bytes
b133449 100c906 b133449 8bde04c 100c906 8bde04c 100c906 b133449 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 2edd069 100c906 8bde04c 2edd069 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 8bde04c 100c906 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 | ---
language:
- en
license: apache-2.0
library_name: peft
base_model: Qwen/Qwen2.5-Coder-7B-Instruct
pipeline_tag: text-generation
tags:
- peft
- lora
- qwen2.5-coder
- verilog
- eda
- dft
- test-point-insertion
- reinforcement-learning
- grpo
---
# TESLA-Pro-TPI
TESLA-Pro-TPI is the RTL test point insertion model from **TESLA-Pro: Testability Enhancement for Shift Left Automation via GRPO-aligned LLMs**. Given complete Verilog RTL, the scan-cell bits selected by PSS, an exact TPI budget, and the insertion contract, it selects legal nonscan register bits and emits the complete TPI-modified RTL.
This repository contains a PEFT LoRA adapter and tokenizer files. It does not contain a merged copy of the base model.
## Model Details
| Item | Value |
|---|---|
| Developer | SKLP-EDA-LAB |
| Base model | [Qwen/Qwen2.5-Coder-7B-Instruct](https://huggingface.co/Qwen/Qwen2.5-Coder-7B-Instruct) |
| Task | RTL test point insertion (TPI) |
| Training stages | SFT, static legality/budget GRPO, and DC/TMAX coverage-aware GRPO |
| Adapter | LoRA, rank 16, alpha 32, dropout 0.10 |
| Release checkpoint | `grpo_model_tmax_coverage_from_budgetaware_ckpt237_5gpu_full_e1/checkpoint-2656` |
| Input | Complete RTL, exact PSS scan-cell list, exact TPI bit budget, and insertion rules |
| Output | `<think>` reasoning and complete modified RTL inside `<total_design>` |
| Upstream model | [TESLA-Pro-PSS](https://huggingface.co/SKLP-EDA-LAB/Tesla-Pro-PSS) |
## Intended Use
TESLA-Pro-TPI is intended for research on shift-left DFT and RTL-level testability optimization. It supports control points (CP), observation points (OP), and CP+OP, subject to the published prompt contract.
Each intervention site is counted at the physical register-bit level. Every selected bit must be a real nonscan register bit; the PSS scan-cell list is a strict forbidden set. The complete generated design must preserve the original top module and functional RTL except for the required TPI additions.
Generated RTL is a candidate, not sign-off output. Static checks, synthesis, and ATPG remain mandatory.
## Required Prompt Format
**Do not send raw RTL or an informal request such as "insert three test points."** The model was fine-tuned with a fixed prompt that defines scan-cell exclusion, register-name normalization, exact intervention-site counting, CP/OP syntax, port style, complete-RTL preservation, and output tags. Omitting this contract changes the task distribution and can make paper results unreproducible.
The complete input-only `gen_sync` prompt is embedded directly in this model
card. The same content is also provided as files for programmatic loading:
- [`examples/gen_sync_messages.json`](examples/gen_sync_messages.json): system/user messages ready for `apply_chat_template`;
- [`examples/gen_sync_prompt.txt`](examples/gen_sync_prompt.txt): the same complete prompt in human-readable form;
- [`examples/gen_sync.v`](examples/gen_sync.v): the original circuit by itself.
### Complete `gen_sync` Prompt
<details>
<summary>Expand the exact TPI system and user prompt</summary>
```text
===== SYSTEM =====
Respond in the following format:
<think>
...
</think>
<total_design>
...
</total_design>
===== USER =====
## RULE #1: KEEP EVERY LINE OF THE ORIGINAL RTL
This is the most important rule. The #RTL CODE# section below contains the complete RTL.
You MUST output the FULL module -- every line stays exactly as it is, except for additions required by the chosen TPI mode:
(a) CP or CP+OP: add `cp_en` using the same port declaration style as the original RTL. OP-only: do NOT add `cp_en`.
(b) OP or CP+OP: add `tp_xxx` ports using the same port declaration style as the original RTL. CP-only: no `tp_*` port is required for that bit.
(c) CP or CP+OP: add CP function definitions at the TOP of the module body.
(d) CP or CP+OP: modify the target register assignment inside always blocks by wrapping the next value with the CP function call.
(e) OP or CP+OP: add OP instantiations inside the module body (before `endmodule`).
(f) OP or CP+OP: add only the required TestPointOBType_* module definitions AFTER the top module's `endmodule`.
DO NOT remove, rewrite, reformat, or regenerate any original RTL code.
DO NOT touch the module name, port list (except adding required cp_en/tp_* ports), parameters, reg/wire declarations,
always blocks, assign statements, or any other original code.
PORT STYLE: The original RTL uses ANSI-style ports.
- Add new ports directly in the module port list with direction/type.
- CP/CP+OP example: `input wire cp_en, output wire tp_sig1`.
- OP-only example: `output wire tp_sig1`.
- Do NOT add separate `input cp_en;` / `output tp_sig1;` declarations in the module body.
## ACTUAL TASK INPUT SUMMARY (READ THIS BEFORE ANY TESTABILITY SCORING)
#Required TPI Count#: 3
#Forbidden Scan Cell Bits for THIS sample#:
counter[0]
Legality equation for this sample:
chosen_tpi_bits ∩ forbidden_scan_bits MUST be empty.
If even one chosen CP-only, OP-only, or CP+OP bit is in the forbidden list, the answer is invalid.
CRITICAL LOW-BIT WARNING for this sample:
The following attractive low-order bits are FORBIDDEN here: counter[0]
Do not choose them even if they toggle frequently. Start scoring only after removing them.
How to derive legal non-scan candidates from the RTL and scan-cell list:
1) Parse the ORIGINAL RTL declarations and sequential assignments to identify real register bits only.
Legal targets must be declared as `reg`, `output reg`, or be assigned in a clocked always block.
Do NOT choose plain `wire`, `input`, combinational temporary wires, or invented signal names.
2) Expand vectors bit-by-bit. Example: `reg [7:0] data_reg;` creates `data_reg[7]` ... `data_reg[0]`.
Scalar registers keep their exact scalar name unless the RTL itself uses an indexed form.
Unpacked register arrays are allowed only with exact static indices: `reg [31:0] stack [7:0];` creates
bits such as `stack[7][8]`. Do NOT select dynamic elements such as `stack[write_ptr]`.
3) Normalize scan-cell names conservatively: remove a leading backslash, remove ONLY the final `_reg` suffix,
keep every other part of the RTL name, and keep the bit index.
Example: `\data_reg_reg[8]` -> `data_reg[8]`, NOT `data[8]`.
Example: `\cc_reg[31]` -> `cc[31]`.
4) Compute: legal_non_scan_register_bits = RTL_declared_register_bits - normalized_forbidden_scan_bits.
5) Choose TPI bits only from legal_non_scan_register_bits. If a chosen name is not an exact RTL register bit,
the answer is invalid even if the name looks semantically reasonable.
Your first reasoning step must remove these exact forbidden bits from consideration.
Never say the scan-cell list is empty unless the list above is literally empty.
## MANDATORY RULES
1. SCAN-CELL EXCLUSION CONSTRAINT (HIGHEST PRIORITY after Rule #1)
#Scan Cell Bits# are scan cells selected by AutoPSS.
These bits are already scan-controllable/observable and MUST NOT be selected for TPI.
Treat #Scan Cell Bits# as an exact FORBIDDEN bit list, not as a recommendation.
All test points MUST be inserted on non-scan register bits, i.e. register bits NOT listed in #Scan Cell Bits#.
If a vector is partially scanned, legality is bit-specific: if cnt[0], cnt[1], cnt[2], cnt[3] are scan cells, then cnt[4] may be legal but cnt[0]..cnt[3] are forbidden.
Low-order bits such as cnt[0], Q[0], state[0], filter[0], data[0] are often attractive because they toggle frequently, but they are STILL ILLEGAL if listed in #Scan Cell Bits#.
Do not select a scan bit for CP-only, OP-only, or CP+OP under any circumstance.
WRONG: Selecting a register bit that appears in #Scan Cell Bits#, even if it has high activity or strong testability.
RIGHT: First remove every scan-cell bit from the candidate set, then choose TPI only from the remaining non-scan bits.
1b. RTL REGISTER-BIT GROUNDING CONSTRAINT
Before selecting TPI, explicitly derive legal candidates as:
RTL_declared_register_bits - normalized_forbidden_scan_bits.
Use the exact RTL signal name. Do not shorten, singularize, or rename registers.
WRONG: RTL declares `data_reg`; selecting `data`.
WRONG: scan cell `\data_reg_reg[8]` is normalized to `data[8]`.
RIGHT: scan cell `\data_reg_reg[8]` is normalized to `data_reg[8]` because only the final `_reg` is removed.
If the RTL declares `state`, do not select `state_reg` unless that exact register exists in the RTL.
Every selected bit must be visible in the original RTL declaration or clocked assignment.
Register arrays/memories are legal only when the target is bit-precise and statically indexed.
RIGHT: `stack[7][8]` if RTL declares `reg [31:0] stack [7:0];`.
WRONG: `stack[write_ptr]`, `stack[7]` as a whole row when the budget is for single bits, or any dynamic index.
2. TPI Counting (IS = Intervention Site = 1 bit)
- 1-bit CP-only = 1 IS | 1-bit OP-only = 1 IS | 1-bit CP+OP = 1 IS
- N-bit OP = N IS (must use `TestPointOBType_Nbit`)
- `output [7:0] tp_a;` = 8 IS. You CANNOT pack multiple IS into one vector.
- Total IS MUST equal exactly 3.
Counting EXAMPLES (CRITICAL -- same bit shared by CP+OP counts as 1 IS):
Ex-A: cnt[3:0] OP (4 IS) + cnt[2] CP+OP (same bit, already counted) = 4 IS total (NOT 5!)
Ex-B: result[15:0] OP (16 IS) + result[0] CP (same bit) = 16 IS total
Ex-C: state[1] CP-only (1 IS) + state[0] OP-only (1 IS) = 2 IS total
3. Port Declaration: Match the original RTL style exactly
Add `cp_en` only if at least one selected bit uses CP or CP+OP.
OP-only designs must not add `cp_en`.
ANSI-style original: add directed ports in the module header, e.g. `input wire cp_en, output wire tp_sig1`.
Non-ANSI-style original: add bare names in the port list and add `input cp_en;` / `output tp_sig1;` declarations in the body.
Never mix ANSI declarations into a non-ANSI port list.
4. CP Function: Use only for CP or CP+OP. Define at TOP of module body, call inside always-block with <=
WRONG: CP on wire/assign. WRONG: function outside module.
WRONG: `assign sig = sig_in & ~cp_en;` (never use assign for CP)
WRONG: `sig = InsertCP_1bit(sig, cp_en);` (forgot <=)
WRONG: `InsertCP_8bit = sig_in & {8{~cp_en}};` when only some bits are selected (this zeroes ALL bits!)
CORRECT: `reg <= InsertCP_1bit(sig_next, cp_en);` (inside always block)
CP Semantics: cp_en=0 means NORMAL (pass-through), cp_en=1 means FORCE-0.
Partial mask (RECOMMENDED): `InsertCP_8bit = {sig_in[7:1], sig_in[0] & ~cp_en};`
Full-vector mask is allowed only when EVERY bit of that vector is selected for CP.
5. OP Instantiation: Use only for OP or CP+OP. Inside module body (before endmodule). NEVER use assign.
CORRECT: `TestPointOBType_1bit op_sig1 (.funcin(signal1[0]), .tp_out(tp_sig1));`
CORRECT: `TestPointOBType_8bit op_sig8 (.funcin(signal[7:0]), .tp_out(tp_sig8));`
Width MUST match: N-bit signal -> `TestPointOBType_Nbit`
6. Module Definition Order:
(a) Original ports + required new ports (`cp_en` only for CP/CP+OP, `tp_*` only for OP/CP+OP)
(b) CP function definitions only if CP/CP+OP exists (at TOP, before always blocks)
(c) OP instantiations only if OP/CP+OP exists (before endmodule)
(d) Original always/assign blocks (UNCHANGED except CP wrapping)
(e) endmodule
(f) `module TestPointOBType_* ... endmodule` definitions only for used OP widths
7. Comments: Do not add new comments. Preserve comments that already exist in the original RTL.
8. Directives: Do not add new `timescale or `include directives. Preserve directives that already exist in the original RTL.
9. Chain-of-Thought (inside <think>):
Step 1: Circuit Analysis + Scan-Cell Exclusion Filtering
- Explicitly identify the scan-cell bits as FORBIDDEN.
- List the real RTL register bits or register-bit groups that can be considered.
- Normalize the scan-cell list using the rule above.
- Build the legal candidate set by computing RTL_declared_register_bits - normalized_forbidden_scan_bits before scoring testability.
- Never justify choosing a forbidden scan bit because it toggles often or looks useful.
Step 2: Testability Scoring for non-scan register bits
Step 3: Budget Allocation and mode choice (CP-only, OP-only, or CP+OP; prove sum of bits = 3)
- Include a compact allocation table: bit | mode | count contribution | implementation line.
- The table must use the exact RTL bit names that will appear in <total_design>.
Step 4: Syntax Pre-simulation
Step 5: Final Engineering Check
- Every bit listed in your allocation table MUST be physically implemented in <total_design>.
- Do not claim a bit such as filter[2] in <think> and then omit its CP/OP construct in RTL.
- Recount physical RTL bits from actual InsertCP/TestPointOBType constructs, not from the prose table.
- Write this exact legality check in words: `chosen_tpi_bits ∩ forbidden_scan_bits = empty`.
- If the intersection is non-empty, you MUST replace the offending bit before writing <total_design>.
- This is especially important for state[0], cnt[0], Q[0], filter[0], received[2], and other attractive low bits.
Inside <total_design>: ONLY modified RTL. No markdown fences, no text.
Stop immediately after </total_design>. Nothing after it.
## STYLE EXAMPLE (follow the syntax style; choose CP/OP/CP+OP according to the actual design)
Example input RTL -- simple state machine with 2 test points:
`timescale 1ns/1ps
module fsm_example #(parameter WIDTH=8) (
input wire clk, rst_n,
input wire [WIDTH-1:0] data_in,
output reg [WIDTH-1:0] data_out,
output wire ready
);
localparam IDLE=2'b00, WORK=2'b01, DONE=2'b10;
reg [1:0] state, next_state;
reg [WIDTH-1:0] buffer;
assign ready = (state == DONE);
always @(posedge clk or negedge rst_n)
if (!rst_n) state <= IDLE;
else state <= next_state;
always @* begin
next_state = state;
case (state)
IDLE: if (data_in[0]) next_state = WORK;
WORK: next_state = DONE;
DONE: next_state = IDLE;
endcase
end
always @(posedge clk or negedge rst_n)
if (!rst_n) buffer <= {WIDTH{1'b0}};
else if (state == WORK) buffer <= data_in;
always @(posedge clk or negedge rst_n)
if (!rst_n) data_out <= {WIDTH{1'b0}};
else data_out <= buffer;
endmodule
CORRECT output -- original RTL fully preserved, CP+OP example added:
`timescale 1ns/1ps
module fsm_example #(parameter WIDTH=8) (
input wire clk, rst_n,
input wire [WIDTH-1:0] data_in,
output reg [WIDTH-1:0] data_out,
output wire ready,
input wire cp_en,
output wire tp_state_1,
output wire tp_buffer_7
);
localparam IDLE=2'b00, WORK=2'b01, DONE=2'b10;
reg [1:0] state, next_state;
reg [WIDTH-1:0] buffer;
assign ready = (state == DONE);
function [1:0] InsertCP_2bit_state;
input [1:0] sig_in;
input cp_en;
begin
InsertCP_2bit_state = {sig_in[1] & ~cp_en, sig_in[0]};
end
endfunction
function [WIDTH-1:0] InsertCP_Wbit_buffer;
input [WIDTH-1:0] sig_in;
input cp_en;
begin
InsertCP_Wbit_buffer = {sig_in[WIDTH-1:8], sig_in[7] & ~cp_en, sig_in[6:0]};
end
endfunction
TestPointOBType_1bit op_state_1 (.funcin(state[1]), .tp_out(tp_state_1));
TestPointOBType_1bit op_buffer_7 (.funcin(buffer[7]), .tp_out(tp_buffer_7));
always @(posedge clk or negedge rst_n)
if (!rst_n) state <= IDLE;
else state <= InsertCP_2bit_state(next_state, cp_en);
always @* begin
next_state = state;
case (state)
IDLE: if (data_in[0]) next_state = WORK;
WORK: next_state = DONE;
DONE: next_state = IDLE;
endcase
end
always @(posedge clk or negedge rst_n)
if (!rst_n) buffer <= {WIDTH{1'b0}};
else if (state == WORK) buffer <= InsertCP_Wbit_buffer(data_in, cp_en);
always @(posedge clk or negedge rst_n)
if (!rst_n) data_out <= {WIDTH{1'b0}};
else data_out <= buffer;
endmodule
module TestPointOBType_1bit (input funcin, output tp_out);
assign tp_out = funcin;
endmodule
module TestPointOBType_2bit (input [1:0] funcin, output [1:0] tp_out);
assign tp_out = funcin;
endmodule
## CP/OP SYNTAX REFERENCE
Use only the syntax needed by your selected modes. OP-only samples do not need `cp_en` or CP functions.
### CP Function (ONLY for CP or CP+OP; AND-type: cp_en=0=normal/pass-through, cp_en=1=force target bit to 0)
The key principle: only the masked bits are forced to 0; ALL other bits PASS THROUGH unchanged.
Mode A -- Single bit CP (most common):
function InsertCP_1bit;
input sig_in; input cp_en;
begin InsertCP_1bit = sig_in & ~cp_en; end
endfunction
Mode B -- Multi-bit, only bit[0] controlled, rest PASS THROUGH:
function [7:0] InsertCP_8bit_bit0;
input [7:0] sig_in; input cp_en;
begin
InsertCP_8bit_bit0 = {sig_in[7:1], sig_in[0] & ~cp_en};
end
endfunction
Mode C -- Multi-bit, specific bits controlled (bit[7] + bit[3]), rest PASS THROUGH:
function [7:0] InsertCP_8bit_bit73;
input [7:0] sig_in; input cp_en;
begin
InsertCP_8bit_bit73 = {
sig_in[7] & ~cp_en, sig_in[6:4],
sig_in[3] & ~cp_en, sig_in[2:0]
};
end
endfunction
Mode D -- Full-vector mask is usually wrong:
Do NOT write `sig_in & {N{~cp_en}}` unless all N bits are selected for CP.
### CP Usage (inside always block, use <= non-blocking)
reg <= InsertCP_1bit(reg_next, cp_en);
reg <= InsertCP_8bit_bit0(reg_next, cp_en);
reg <= InsertCP_8bit_bit73(reg_next, cp_en);
Full-vector mask is rarely correct -- it zeroes every bit of the vector!
### OP Instantiation
TestPointOBType_1bit op_sig1 (.funcin(signal1), .tp_out(tp_sig1));
TestPointOBType_8bit op_sig8 (.funcin(signal[7:0]), .tp_out(tp_sig8));
For unpacked register arrays, use exact static bit indices:
TestPointOBType_1bit op_stack_7_8 (.funcin(stack[7][8]), .tp_out(tp_stack_7_8));
Do not use dynamic array indices for TPI targets.
### Port Declaration
Preserve the original port declaration style.
ANSI original: add directed ports in the header.
Non-ANSI original: add bare names in the header and declarations in the body.
`cp_en` is only for CP or CP+OP. `tp_*` is only for OP or CP+OP.
### Module Definition Order
1) Original ports + required added ports
2) CP function definitions, only if CP/CP+OP exists (at TOP of module body)
3) OP instantiations, only if OP/CP+OP exists (before endmodule)
4) Original logic (unchanged)
5) endmodule
6) TestPointOBType_* module definitions, only for used OP widths
#RTL CODE#:
module gen_sync ( input clock,input reset,input enable,input [7:0] rate,output wire sync );
reg [7:0] counter;
assign sync = |(((rate+1)>>1)& counter);
always @(posedge clock)
if(reset || ~enable)
counter <= #1 0;
else if(counter == rate)
counter <= #1 0;
else
counter <= #1 counter + 8'd1;
endmodule
#Scan Cell Bits (DO NOT select):
counter[0]
#Required TPI Count: 3
```
</details>
For a new design, retain all fixed rules and replace only:
- `#Required TPI Count#` and its repeated budget references;
- `#Forbidden Scan Cell Bits#` / `#Scan Cell Bits#` with the exact PSS output;
- `#RTL CODE#` with the complete target RTL;
- the declared RTL port-style statement when the target is non-ANSI.
The output contract is:
```text
<think>
scan exclusion, legal candidate derivation, testability scoring,
budget/mode allocation, and implementation checks
</think>
<total_design>
complete TPI-modified Verilog RTL only
</total_design>
```
## Input-Only Circuit Example
The published example receives `counter[0]` from PSS as a forbidden scan-cell bit and requests **three** TPI bits. No reference TPI response is included.
```text
Required TPI Count: 3
Forbidden Scan Cell Bits:
counter[0]
```
```verilog
module gen_sync ( input clock,input reset,input enable,input [7:0] rate,output wire sync );
reg [7:0] counter;
assign sync = |(((rate+1)>>1)& counter);
always @(posedge clock)
if(reset || ~enable)
counter <= #1 0;
else if(counter == rate)
counter <= #1 0;
else
counter <= #1 counter + 8'd1;
endmodule
```
The full fixed prompt is intentionally preserved in [`examples/gen_sync_messages.json`](examples/gen_sync_messages.json). It includes the bit-normalization rule that removes only the final synthesized `_reg` suffix, the CP/OP templates, and the exact scan-bit exclusion contract.
## Quickstart
Install recent versions of the required libraries:
```bash
pip install "transformers>=4.37" peft accelerate huggingface_hub
```
Run the exact input-only example:
```python
import json
import torch
from huggingface_hub import hf_hub_download
from peft import AutoPeftModelForCausalLM
from transformers import AutoTokenizer
model_id = "SKLP-EDA-LAB/Tesla-Pro-TPI"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoPeftModelForCausalLM.from_pretrained(
model_id,
torch_dtype="auto",
device_map="auto",
)
model.eval()
messages_path = hf_hub_download(
repo_id=model_id,
filename="examples/gen_sync_messages.json",
)
with open(messages_path, encoding="utf-8") as f:
messages = json.load(f)
text = tokenizer.apply_chat_template(
messages,
tokenize=False,
add_generation_prompt=True,
)
inputs = tokenizer(text, return_tensors="pt").to(model.device)
with torch.inference_mode():
generated = model.generate(
**inputs,
max_new_tokens=8192,
do_sample=True,
temperature=0.25,
top_p=0.90,
)
new_tokens = generated[:, inputs.input_ids.shape[1]:]
print(tokenizer.decode(new_tokens[0], skip_special_tokens=True))
```
For Pass@5-style evaluation, sample five independent completions with the same prompt, then parse and validate each generated `<total_design>` separately.
## Evaluation
### Paper Results
The paper evaluates five sampled outputs per circuit. For TPI, a sample passes when it inserts the requested number of test points and completes synthesis and equivalence checking successfully. The best valid rollout per circuit is then used for TC, PC, and DAT comparison.
| Model | P@5 (%) | Best in TC Imp. (%) | Best in PC (%) | Best in DAT (%) |
|---|---:|---:|---:|---:|
| **TESLA-Pro-TPI** | **94.3** | **65.0** | **64.0** | **71.0** |
| TESLA (SFT + DPO) | 89.8 | 49.5 | 55.5 | 66.5 |
| Qwen2.5-Coder-7B | 7.5 | 1.25 | 6.25 | 6.25 |
`TC Imp.` is test-coverage improvement, `PC` is ATPG pattern count, and `DAT` is data arrival time. These results depend on the paper's prompt, output parser, synthesis libraries, equivalence flow, constraints, and ATPG setup.
### Input-Only Case Validation
For the held-out `gen_sync` example bundled here:
- the PSS-to-TPI handoff supplied `counter[0]` as the exact forbidden scan bit;
- strict TPI static validation passed;
- DC and TMAX completed under stuck-at, full-sequential ATPG;
- baseline coverage was 9.41%, and TPI coverage was 9.73% (+0.32 percentage points);
- pattern count decreased from 7 to 5.
The reference TPI RTL was not supplied to the model. The example was checked against the TPI training inputs by normalized RTL hash; no matching training input was found.
## Training
The manuscript reports the following common experimental recipe:
- base model: Qwen2.5-Coder-7B-Instruct (7.61B parameters);
- LoRA fine-tuning;
- learning rate: `5e-6`;
- batch size: `8`;
- instruction-tuning bootstrap: 3 epochs;
- GRPO: 2 epochs, group size `G=7`, KL coefficient `beta=0.02`, clipping range `epsilon=0.2`;
- software: PyTorch, Transformers, and TRL;
- hardware: 8 NVIDIA A100 80 GB GPUs connected with NVLink.
The paper reports a corpus of 7,842 single-module RTL samples, with 800 selected complex samples transformed for TPI supervision. PSS outputs are supplied as scan-cell constraints to AutoTPI-Pro, and the data are split 7:2:1 for training, validation, and testing.
GRPO combines structural feedback for syntax, budget, and legal register selection with functional feedback from synthesis and ATPG metrics. Test coverage is prioritized, followed by pattern count and data arrival time.
The adapter configuration shipped in this repository is authoritative for LoRA structure; the manuscript describes the paper-level training setup.
## Validation Requirements
Before accepting generated RTL, at minimum:
1. extract exactly one `<total_design>` block and parse the Verilog;
2. verify the original top module and all original functional logic are retained;
3. derive actual CP/OP target bits from RTL constructs, not from reasoning text;
4. normalize identifiers conservatively and reject every PSS scan-cell intersection;
5. require the unique physical intervention-site count to equal the budget;
6. check CP active-high force-0 semantics and OP width/port consistency;
7. run synthesis, equivalence checking, and ATPG against a matched baseline.
## Limitations
- The model can produce malformed, truncated, or functionally incorrect RTL.
- A legal candidate does not guarantee positive coverage improvement on every rollout.
- Hierarchical RTL, escaped identifiers, arrays, generated logic, and synthesis renaming require careful handling.
- Coverage and timing depend on the cell library, constraints, fault model, ATPG mode/depth, reset protocol, and timeout policy.
- Generated reasoning is not a formal proof. Parsed RTL and EDA reports are the source of truth.
- This research model is not suitable for unattended production sign-off.
## Citation
```bibtex
@misc{chao2026teslapro,
title = {TESLA-Pro: Testability Enhancement for Shift Left Automation via GRPO-aligned LLMs},
author = {Zhiteng Chao and Jingjie Xia and Rengang Zhang and Feng Gu and Hongqin Lyu and Bin Sun and Wenxing Li and Jianan Mu and Zizhen Liu and Jing Ye and Xiaowei Li and Huawei Li},
year = {2026},
note = {Manuscript}
}
```
## License
The adapter files in this repository are released under the Apache License 2.0. Use of the base model is also subject to its own repository terms.
|