---
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 repository provides the exact input-only `gen_sync` prompt in two forms:

- [`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.

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.

### Stricter Coverage-Gain Audit

The release checkpoint was also evaluated under a stricter matched DC/TMAX protocol in which a pass requires a positive coverage delta:

| Designs | Rollouts/design | Coverage-gain Pass@1 | Coverage-gain Pass@5 |
|---:|---:|---:|---:|
| 116 | 5 | 45.7% | 61.2% |

Among 346 candidates that passed strict static checks and had comparable EDA reports, 72.0% improved test coverage. Their mean coverage delta was +0.97 percentage points. This stricter metric is different from the paper's task-validity P@5 and should not be compared as if they were the same denominator or pass condition.

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