Jalik/qwen3-8b-codev-sva-ol-dfs-think

TEXT GENERATIONPricing:Input $0.468 / Output $1.82Concurrent Unit Cost:1Model Size:8BQuant:FP8Context Size:32kTool Calling:SupportedPublished:Aug 10, 2026License:apache-2.0Architecture:Transformer Open Weights Featherless Exclusive Cold

Jalik/qwen3-8b-codev-sva-ol-dfs-think is an 8 billion parameter Qwen3-based language model fine-tuned for translating natural language design properties into SystemVerilog Assertions (SVA). It uniquely generates an explicit, structured derivation within a block, detailing operator-level natural language, a natural language decomposition tree, and an operator-merge-SVA tree. This model excels at generating formally validated SVA code for hardware verification, providing a transparent reasoning process for each assertion.

Loading preview...

Model Overview

Jalik/qwen3-8b-codev-sva-ol-dfs-think is an 8 billion parameter model built on the Qwen3 architecture, specifically fine-tuned for Natural Language to SystemVerilog Assertion (NL2SVA) translation. Its core innovation lies in generating a detailed, structured reasoning process alongside the final SVA code, enclosed within <think>...</think> tags.

Key Capabilities & Features

  • Structured Reasoning: The model provides a three-part reasoning structure for each SVA: an operator-level natural language (OL NL) restatement, a natural language decomposition tree, and an operator-merge-SVA tree for symbolic derivation.
  • Formally Validated Training Data: The reasoning traces in the training data were rigorously validated using JasperGold, ensuring semantic equivalence between the OL-NL statements and their corresponding assertions.
  • SVA Generation: Translates natural language descriptions of design properties into concrete SystemVerilog Assertions.
  • Fixed Prompt Format: Optimized for the qwen3 chat template, expecting a testbench module and a specific question format.

Training Details

  • Base Model: Qwen/Qwen3-8B (36 layers, 4096 hidden size).
  • Method: Full-parameter Supervised Fine-Tuning (SFT) using LLaMA-Factory and DeepSpeed ZeRO-3.
  • Data: Fine-tuned on 5,000 records from the wyt2000/CodeV-SVA-datasets, filtered for single assert property statements.

Limitations

  • Convention-bound: Performance may degrade if prompts deviate from the expected tb_reset and // TODO: ASSERTION conventions.
  • Single-assertion Scope: Primarily trained for generating single assert property statements; multi-assertion or multi-clock requests are out of distribution.
  • No End-to-End Verification Score: While training data reasoning was validated, the fine-tuned model's output requires formal checking.
  • Generated Reasoning: The natural-language justifications within the reasoning fields were not individually reviewed.

Finetunes
1 models