TESLA-Pro-PSS is the partial scan selection model from TESLA-Pro: Testability Enhancement for Shift Left Automation via GRPO-aligned LLMs. Given Verilog RTL and an exact scan-cell budget, it reasons over clocked state and returns a bit-precise list of registers for partial-scan insertion.

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
Task	RTL partial scan selection (PSS)
Training stages	Supervised fine-tuning followed by structural- and EDA-aware GRPO
Adapter	LoRA, rank 16, alpha 32, dropout 0.05
Release checkpoint	`pss_stage2_coverage_from_stage1_8gpu_e1_20260717/checkpoint-175`
Input	Complete Verilog RTL and an exact PSS bit budget
Output	`<think>` reasoning and `<answer>` containing one unique RTL register bit per line
Downstream model	TESLA-Pro-TPI

Intended Use

TESLA-Pro-PSS is intended for research on shift-left DFT and RTL-level partial scan exploration. A valid selection must:

contain exactly the requested number of unique bits;
use exact names and in-range indices from the RTL;
select only state-holding variables assigned in edge-triggered blocks; and
exclude ports, wires, constants, parameters, combinational temporaries, and invented signals.

The selected bits are candidates, not sign-off results. They must be realized and checked with synthesis and ATPG.

Required Prompt Format

Do not send raw RTL alone. The model was fine-tuned with a fixed task prompt that defines bit-level legality, exact budget accounting, and the required output tags. Changing or omitting this contract can substantially reduce reproducibility.

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: system/user messages ready for apply_chat_template;
examples/gen_sync_prompt.txt: the same prompt in human-readable form;
examples/gen_sync.v: the original circuit by itself.

Complete `gen_sync` Prompt

Expand the exact PSS system and user prompt

text

===== SYSTEM =====
Respond in the following format:

<think>
...
</think>
<answer>
...
</answer>

===== USER =====
You are a DFT engineer specializing in partial scan design. Analyze the RTL code and select register bits as scan cells using budgeted allocation. Track your remaining budget after each selection. Select exactly 1 bits.

Rules:
- Only select bits from reg variables within their declared width
- Wire variables cannot be scan cells
- Select only state-holding variables assigned in edge-triggered clocked always blocks
- Do not select input ports, clocks, resets, wires, constants, parameters, localparams, integers, genvars, or combinational/next-state temporary signals
- An output is selectable only when it is a real clocked state-holding variable
- Copy every selected name exactly from the RTL; never invent, rename, abbreviate, or add/remove suffixes
- For a vector, select explicit in-range bits such as state[2]; do not output a slice or a whole multi-bit vector name
- If a candidate is uncertain, skip it and choose another clearly clocked state-holding bit
- Use format 'RegisterName[bit_index]' for multi-bit registers
- Use 'RegisterName' for single-bit registers
- The final answer must be placed in <answer> tags after </think>
- Answer must contain exactly 1 lines (one register bit per line) in the <answer> section

Place your step-by-step reasoning with budget tracking between <think> and </think>.
Key requirements:
- Start with budget: 'I have 1 bits to allocate'
- Allocation strategy (choose based on the number of bits to select):
  * For small selections (<=20 bits): Select bits one by one or in very small groups (<=5), stating the running budget after every single addition
  * For large selections (>20 bits): You may group selections into logical categories (e.g., FSM state bits, counters, synchronizers, data-path registers). For each group, first justify the group, then list the exact bits in that group. After every group, immediately state: 'This group contributes X bits. Current total: N/1, remaining budget: M'. When the remaining budget <=12, switch back to selecting one bit at a time with per-bit justification and running count
- Track budget after each selection or group: 'Allocate X bits to RegisterName[bit], remaining Y bits' or 'This group contributes X bits. Current total: N/1, remaining budget: M'
- Focus on BIT-LEVEL selection: Explain why specific bits (e.g., Volume[3]) were chosen, not just register names
- Do NOT enumerate all registers upfront. Mention registers only as you allocate them
- Never repeat allocations. If repeating patterns appear, STOP and verify budget
- If budget becomes negative, you must immediately stop and re-select fewer bits. Do NOT continue repeating the same selection
- Verify at the end: 'Total = 1 bits; budget = 0'
- Before writing <answer>, extract exactly 1 register bits from your reasoning that match your budget tracking. The <answer> section must contain exactly 1 lines, one register bit per line.

#QUESTION#: Which 1 register bits were selected as the most suitable scan cells?
#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

For a new design, retain all prompt rules and replace only:

the requested budget in the instruction and question;
#RTL CODE# with the complete target RTL.

The output contract is:

text

<think>
step-by-step register legality and budget reasoning
</think>
<answer>
one exact register bit per line
</answer>

Input-Only Circuit Example

The published example requests one scan-cell bit. No reference response is included.

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

Use the complete fixed prompt from examples/gen_sync_messages.json, rather than wrapping this RTL in an unrelated generic coding prompt.

Quickstart

Install recent versions of the required libraries:

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-PSS"

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=2048,
        do_sample=True,
        temperature=0.7,
        top_p=0.95,
    )

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 and validate each completion separately.

Evaluation

Paper Results

The paper evaluates five sampled outputs per circuit. For PSS, a sample passes when it contains the user-requested number of single-bit registers and completes partial-scan synthesis 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-PSS	95.3	70.7	68.3	76.1
TESLA (SFT + DPO)	94.3	69.2	66.9	75.8
Qwen2.5-Coder-7B	11.7	4.1	9.4	9.8

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, constraints, and ATPG setup.

Input-Only Case Validation

For the held-out gen_sync example bundled here:

all 5 sampled outputs passed format and static legality checks;
synthesis realized the requested scan length of 1;
the post-synthesis design contained 8 DFFs, including 7 nonscan DFFs;
TMAX completed under the case-study configuration.

The example was checked against the PSS SFT and GRPO 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, split 7:2:1 for training, validation, and testing. PSS supervision was produced by back-annotating validated netlist-level scan selections to RTL.

The adapter configuration shipped in this repository is authoritative for LoRA structure; the manuscript describes the paper-level training setup.

Validation Requirements

Before using a generated selection, at minimum:

parse <answer> rather than counting text lines heuristically;
deduplicate selected bits;
verify exact RTL declaration and index bounds;
verify edge-triggered state ownership;
require the unique legal bit count to equal the budget;
run partial-scan synthesis and ATPG with matched constraints.

Limitations

The model does not guarantee that a legal selection improves coverage or pattern count.
Hierarchical names, escaped identifiers, register renaming, memories, and synthesis optimization require careful normalization.
Results vary with the standard-cell library, clock/reset constraints, scan realization, fault model, ATPG mode, and timeout policy.
Generated reasoning is not a formal proof. The parsed selection 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.

SKLP-EDA-LAB/Tesla-Pro-PSS

TESLA-Pro-PSS