GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
Jalik
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Run this model inference with full control and performance in your environment.
Model Details
Model Provider
Jalik
Model Tree
Qwen/Qwen3-8B
Input Modalities
Output Modalities
Supported Functionality
Trained with the qwen3 chat template. The user turn contains the testbench
module (including a tb_reset wire and a // TODO: ASSERTION marker) followed
by Question: and the property description.
python
from transformers import AutoModelForCausalLM, AutoTokenizermodel_id = "Jalik/qwen3-8b-codev-sva-ol-dfs-think"tok = AutoTokenizer.from_pretrained(model_id)model = AutoModelForCausalLM.from_pretrained(model_id, torch_dtype="bfloat16", device_map="auto")messages = [{"role": "system", "content":"You are an AI assistant tasked with formal verification of register ""transfer level (RTL) designs.\nYour job is to translate a description ""of an assertion to concrete SystemVerilog Assertion (SVA) implementation."},{"role": "user", "content": """Here is the testbench to perform your translation:module example(input clk, input rst_n, output valid, output fail);// ... design body ...wire tb_reset;assign tb_reset = (rst_n == 1'b0);// TODO: ASSERTIONendmoduleQuestion: Create a SVA assertion that checks: The valid and fail signals must never be active at the same time. Use the signals 'fail' and 'valid'.You should use `tb_reset` as the disable condition signal. Do not add code to output an error message string.Enclose your SVA code with ```systemverilog and ```. Only output the code snippet and do NOT output anything else.Answer:"""},]text = tok.apply_chat_template(messages, tokenize=False, add_generation_prompt=True,enable_thinking=True)out = model.generate(**tok(text, return_tensors="pt").to(model.device), max_new_tokens=2048)print(tok.decode(out[0], skip_special_tokens=True))
enable_thinking=True matters: the model was trained with the reasoning block
present and loss computed over it. Disabling it diverges from training.
markdown
<think>OL NL: valid and fail must never be true at the same time.***nl-decomposition tree***operator: !natural language piece: valid and fail must never be true at the same time.reason: The logical NOT (!) negates the conjunction (valid && fail), ...└── operator: &&├── operator: null (leaf: valid)└── operator: null (leaf: fail)***operator-merge-sva tree***T1 = failT2 = validT3 = T2 && T1 [ = valid && fail ]T4 = !(T3) [ = !(valid && fail) ]Final assertion (T4): !(valid && fail)</think>```systemverilogasrt_valid_fail_mutex: assert property (@(posedge clk) disable iff (tb_reset)!(valid && fail));
markdown
The answer is always the final fenced `systemverilog` block, so downstreamextractors that take the *last* such fence work unchanged.## Training data5,000 records sampled from[`wyt2000/CodeV-SVA-datasets`](https://huggingface.co/datasets/wyt2000/CodeV-SVA-datasets)(83,195 records), filtered to those whose answer is a single `assert property`parseable into an operator/signal tree.The reasoning was generated, not hand-written, and — importantly — **formallyvalidated**. For each record an OL-NL statement was produced, a *candidate* SVAwas regenerated from that statement alone, and the candidate was checked againstthe golden assertion with JasperGold. Only a **`Full equivalence`** result wasaccepted; anything weaker (including one-directional implication) was rejectedand the record retried or replaced. So each retained OL-NL statement is known tobe a semantically exact restatement of its assertion, not merely a plausible one.System and user turns are byte-identical to the source dataset; only theassistant turn was replaced.## Training| | ||---|---|| Base | `Qwen/Qwen3-8B` (36 layers, hidden 4096, bf16) || Method | Full-parameter SFT (not LoRA) || Framework | LLaMA-Factory 0.9.3.dev0, DeepSpeed ZeRO-3 || Hardware | 4 × NVIDIA H200 || Epochs | 3 (1,875 steps) || LR | 1e-5, cosine, warmup ratio 0.1 || Effective batch | 8 (1 × 2 grad-accum × 4 GPUs) || Max sequence | 16,384 tokens || Precision | bfloat16 || Final train loss | **0.1725** || Runtime | 68 min |Loss fell from ~1.76 to ~0.12 with gradient norm settling from ~35 to ~0.5.## Limitations- **Convention-bound.** Training data consistently uses `tb_reset` as the`disable iff` condition and a testbench with a `// TODO: ASSERTION` marker.Prompts departing from that shape may degrade.- **Single-assertion scope.** Trained only on examples whose answer is exactlyone `assert property`. Multi-assertion or multi-clock requests are out ofdistribution.- **Not verified end-to-end here.** Training loss is not correctness. Thereasoning traces in the *training data* were JasperGold-verified, but thismodel card reports no benchmark score for the fine-tuned model itself — treatgenerated assertions as proposals to be formally checked, not as correct byconstruction.- **Reasoning is generated.** The decomposition trees come from an LLM pipeline;the operator structure is mechanical, but the natural-language justificationsin the `reason:` fields were not individually reviewed.## LicenseReleased under Apache-2.0, matching the `Qwen/Qwen3-8B` base model. Training dataderives from `wyt2000/CodeV-SVA-datasets`; consult that dataset for its own terms.