vxkyyy commited on
Commit
ea63a7a
·
1 Parent(s): 81fa1c9

Update source files and scripts

Browse files
.gitignore CHANGED
@@ -32,6 +32,10 @@ runs/
32
  work/
33
  transcript
34
 
 
 
 
 
35
  # System
36
  .DS_Store
37
  Thumbs.db
 
32
  work/
33
  transcript
34
 
35
+ # OSS CAD Suite (large binary toolchain - download separately)
36
+ oss-cad-suite/
37
+ oss-cad-suite-*.tgz
38
+
39
  # System
40
  .DS_Store
41
  Thumbs.db
requirements.txt CHANGED
@@ -3,6 +3,7 @@ crewai-tools
3
  langchain_openai
4
  typer
5
  rich
 
6
  streamlit
7
  pandas
8
  streamlit-option-menu
 
3
  langchain_openai
4
  typer
5
  rich
6
+ python-dotenv
7
  streamlit
8
  pandas
9
  streamlit-option-menu
scripts/setup_env.sh ADDED
@@ -0,0 +1,18 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ #!/bin/bash
2
+ # Setup environment for AgentIC and OSS CAD Suite
3
+
4
+ export OSS_CAD_SUITE_HOME="$HOME/AgentIC/oss-cad-suite"
5
+ if [ -d "$OSS_CAD_SUITE_HOME" ]; then
6
+ export PATH="$OSS_CAD_SUITE_HOME/bin:$PATH"
7
+ echo "✅ OSS CAD Suite added to PATH"
8
+ else
9
+ echo "⚠ OSS CAD Suite not found at $OSS_CAD_SUITE_HOME"
10
+ echo " Please wait for the installation to finish."
11
+ fi
12
+
13
+ # Verify tools
14
+ if command -v sby &> /dev/null; then
15
+ echo "✅ SymbiYosys (sby) is available."
16
+ else
17
+ echo "❌ SymbiYosys (sby) NOT found."
18
+ fi
scripts/verify_design.sh CHANGED
@@ -7,6 +7,12 @@ if [ -z "$1" ]; then
7
  exit 1
8
  fi
9
 
 
 
 
 
 
 
10
  DESIGN=$1
11
  OPENLANE_ROOT="${OPENLANE_ROOT:-$HOME/OpenLane}"
12
  DESIGN_DIR=$OPENLANE_ROOT/designs/$DESIGN
@@ -87,5 +93,28 @@ else
87
  fi
88
  fi
89
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
90
  echo "========================================"
91
  echo "Verification Complete."
 
7
  exit 1
8
  fi
9
 
10
+ # Auto-load environment
11
+ SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
12
+ if [ -f "$SCRIPT_DIR/setup_env.sh" ]; then
13
+ source "$SCRIPT_DIR/setup_env.sh" > /dev/null
14
+ fi
15
+
16
  DESIGN=$1
17
  OPENLANE_ROOT="${OPENLANE_ROOT:-$HOME/OpenLane}"
18
  DESIGN_DIR=$OPENLANE_ROOT/designs/$DESIGN
 
93
  fi
94
  fi
95
 
96
+ echo ""
97
+ echo "========================================"
98
+
99
+ # 3. Formal Verification (SymbiYosys)
100
+ echo "[3] Formal Verification (SymbiYosys)"
101
+ if [ -f "$DESIGN_DIR/src/${DESIGN}.sby" ]; then
102
+ echo " Found SBY Config: ${DESIGN}.sby"
103
+ cd $DESIGN_DIR/src
104
+ if command -v sby &> /dev/null; then
105
+ sby -f ${DESIGN}.sby
106
+ if [ $? -eq 0 ]; then
107
+ echo " [PASS] Formal Proof Successful."
108
+ else
109
+ echo " [FAIL] Formal Proof Failed."
110
+ fi
111
+ else
112
+ echo " [WARNING] 'sby' command not found. Skipping Formal Verification."
113
+ fi
114
+ cd $OPENLANE_ROOT
115
+ else
116
+ echo " [INFO] No SBY config found. Skipping."
117
+ fi
118
+
119
  echo "========================================"
120
  echo "Verification Complete."
src/agentic/__init__.py CHANGED
@@ -1,4 +1,4 @@
1
  """
2
  AgentIC - AI-Driven Chip Design Framework
3
  """
4
- __version__ = "0.1.0"
 
1
  """
2
  AgentIC - AI-Driven Chip Design Framework
3
  """
4
+ __version__ = "2.0.0"
src/agentic/cli.py CHANGED
@@ -203,19 +203,24 @@ Reply with ONLY "A" or "B".''',
203
  fix_tb_logic_prompt = f'''Fix the Testbench logic/syntax. The simulation failed or generated runtime errors.
204
 
205
  CRITICAL FIXING RULES:
206
- 1. **Timing**: Ensure you `wait(done)` or `repeat(N) @(posedge clk)` before checking results.
207
- 2. **Race Conditions**: If "TEST FAILED" happens immediately, add delays (`#1`) before sampling or driving signals.
208
- 3. **Format**: Return ONLY corrected testbench code inside ```verilog fences.
 
 
 
 
 
209
 
210
  Simulation Error/Output:
211
  {sim_output_text}
212
 
213
- Current RTL (Reference):
214
  ```verilog
215
  {open(rtl_path,'r').read()}
216
  ```
217
 
218
- Current Testbench (To Fix):
219
  ```verilog
220
  {open(tb_path,'r').read()}
221
  ```
@@ -610,7 +615,7 @@ Current code:
610
  console.print(" ✓ Verilog syntax is [green]valid[/green]")
611
 
612
  # ===== STEP 2.5: Formal Assertions (SVA) =====
613
- console.print("\n[bold yellow]━━━ Step 2.5: Formal Verification (Autonomous Vendor Mode) ━━━[/bold yellow]")
614
 
615
  with open(rtl_path, 'r') as f:
616
  rtl_code = f.read()
@@ -619,37 +624,58 @@ Current code:
619
  sva_task = Task(
620
  description=f'''Analyze this RTL and generate a separate SystemVerilog Assertion (SVA) module (`{name}_sva.sv`) to formally verify behavior.
621
 
 
 
622
  Rules:
623
  - Module name: `{name}_sva`
624
  - Bind to target module using `bind {name} {name}_sva inst_sva (.*);`
625
- - Use `property` and `assert property (@(posedge clk) ...)`
 
 
 
 
626
  - Check resets, state transitions, and critical safety logic.
627
- - NO `initial` blocks, NO `$display`. use pure SVA.
628
 
629
  RTL:
630
  ```verilog
631
  {rtl_code}
632
  ```
633
  ''',
634
- expected_output='SVA module code in markdown fence',
635
  agent=verify_agent
636
  )
637
 
638
- with console.status("[cyan]AI is proving mathematical correctness (SymbiYosys)...[/cyan]"):
639
  sva_result = Crew(agents=[verify_agent], tasks=[sva_task]).kickoff()
640
  sva_raw = str(sva_result)
641
 
642
- # Save SVA file using robust cleaner
643
- write_verilog(name, sva_raw, suffix="_sva", ext=".sv")
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
644
 
645
- # Write SBY Config
646
- write_sby_config(name)
647
 
648
  # Run Formal Verification
649
  formal_success, formal_msg = run_formal_verification(name)
650
 
651
  if formal_success:
652
- console.print(f" ✓ [bold green]Mathematical Proof PASSED[/bold green]")
653
  log_thinking(formal_msg, step="Formal Verification Log")
654
  else:
655
  # Check for missing tool vs actual failure
@@ -657,8 +683,9 @@ RTL:
657
  console.print(f" [yellow]⚠ Formal Verification Skipped[/yellow]: [dim]SymbiYosys (sby) not installed.[/dim]")
658
  console.print(f" [dim]- Install: https://github.com/YosysHQ/oss-cad-suite-build[/dim]")
659
  else:
660
- console.print(f" ✗ [bold red]Formal Proof FAILED (Design is risky)[/bold red]")
661
- console.print(formal_msg)
 
662
 
663
  # ===== STEP 3: Generate Testbench (self-checking) =====
664
  console.print("\n[bold yellow]━━━ Step 4/6: Generating Testbench (Spec + RTL Analysis) ━━━[/bold yellow]")
@@ -689,14 +716,19 @@ CRITICAL VERIFICATION RULES (DO NOT VIOLATE):
689
  3. **Data Types**: Use `logic` for everything.
690
  4. **Instantiation**: Use explicit name based connection `.port(signal)`.
691
  5. **Clock/Reset**:
692
- - Clock: `initial forever #5 clk = ~clk;`
693
- - Reset: Drive `rst_n` low for 20 units, then high.
694
- 6. **Timing & Handshaking (CRITICAL)**:
695
- - **WAIT FOR RESULTS**: If the DUT has a pipeline or state machine, you MUST wait multiple clock cycles before checking outputs.
696
- - If there is a `valid_out` or `done` signal, `wait(valid_out);` or `while(!valid_out) @(posedge clk);`.
697
- - If fixed latency, use `repeat(10) @(posedge clk);` (or more) to allow data to propagate.
698
- - Do NOT check `data_out` in the same cycle you assert inputs (unless combinational).
699
- 7. **Reporting**:
 
 
 
 
 
700
  - Use `$dumpfile("{name}.vcd")` and `$dumpvars(0, {name}_tb)`.
701
  - On success: `$display("TEST PASSED");`
702
  - On failure: `$display("TEST FAILED");`
 
203
  fix_tb_logic_prompt = f'''Fix the Testbench logic/syntax. The simulation failed or generated runtime errors.
204
 
205
  CRITICAL FIXING RULES:
206
+ 1. **Timing is USUALLY THE PROBLEM**: If "TEST FAILED" appears, the testbench is checking outputs TOO EARLY.
207
+ - Count the FSM states in the RTL. Wait at least (num_states + 10) clock cycles.
208
+ - Use `repeat(25) @(posedge clk);` minimum before checking ANY output.
209
+ - If there's a `done` or `valid` signal, use `while(!done) @(posedge clk);`
210
+ 2. **Race Conditions**: Add `#1` delays after clock edges before sampling.
211
+ 3. **Reset**: Ensure reset is held for at least 4 clock cycles.
212
+ 4. **Between Tests**: Wait for FSM to return to IDLE with `repeat(10) @(posedge clk);`
213
+ 5. **Format**: Return ONLY corrected testbench code inside ```verilog fences.
214
 
215
  Simulation Error/Output:
216
  {sim_output_text}
217
 
218
+ Current RTL (Reference - count the FSM states):
219
  ```verilog
220
  {open(rtl_path,'r').read()}
221
  ```
222
 
223
+ Current Testbench (To Fix - increase wait cycles):
224
  ```verilog
225
  {open(tb_path,'r').read()}
226
  ```
 
615
  console.print(" ✓ Verilog syntax is [green]valid[/green]")
616
 
617
  # ===== STEP 2.5: Formal Assertions (SVA) =====
618
+ console.print("\n[bold yellow]━━━ Step 2.5: Formal Verification (Dual-Mode: Industry SVA + Yosys) ━━━[/bold yellow]")
619
 
620
  with open(rtl_path, 'r') as f:
621
  rtl_code = f.read()
 
624
  sva_task = Task(
625
  description=f'''Analyze this RTL and generate a separate SystemVerilog Assertion (SVA) module (`{name}_sva.sv`) to formally verify behavior.
626
 
627
+ CRITICAL: Generate INDUSTRY-STANDARD SystemVerilog Assertions using `property` and `assert property`.
628
+
629
  Rules:
630
  - Module name: `{name}_sva`
631
  - Bind to target module using `bind {name} {name}_sva inst_sva (.*);`
632
+ - Use proper SVA syntax:
633
+ - `property prop_name; @(posedge clk) antecedent |=> consequent; endproperty`
634
+ - `assert property (prop_name);`
635
+ - Use `$past(signal)` for temporal checks
636
+ - Use `disable iff (!rst_n)` for reset handling
637
  - Check resets, state transitions, and critical safety logic.
638
+ - NO `initial` blocks, NO `$display`. Use pure SVA.
639
 
640
  RTL:
641
  ```verilog
642
  {rtl_code}
643
  ```
644
  ''',
645
+ expected_output='Industry-standard SVA module code in markdown fence',
646
  agent=verify_agent
647
  )
648
 
649
+ with console.status("[cyan]AI is generating industry-standard SVA assertions...[/cyan]"):
650
  sva_result = Crew(agents=[verify_agent], tasks=[sva_task]).kickoff()
651
  sva_raw = str(sva_result)
652
 
653
+ # Save INDUSTRY-STANDARD SVA file (for commercial tools: Synopsys, Cadence, etc.)
654
+ sva_path = write_verilog(name, sva_raw, suffix="_sva", ext=".sv")
655
+ console.print(f" ✓ Industry SVA saved: [green]{name}_sva.sv[/green] (for commercial EDA)")
656
+
657
+ # Convert to Yosys-compatible format for open-source verification
658
+ from .tools.vlsi_tools import convert_sva_to_yosys
659
+ sva_content = open(sva_path, 'r').read() if os.path.exists(sva_path) else sva_raw
660
+ yosys_sva = convert_sva_to_yosys(sva_content, name)
661
+
662
+ if yosys_sva:
663
+ sby_check_path = f"{OPENLANE_ROOT}/designs/{name}/src/{name}_sby_check.sv"
664
+ with open(sby_check_path, 'w') as f:
665
+ f.write(yosys_sva)
666
+ console.print(f" ✓ Yosys SVA saved: [green]{name}_sby_check.sv[/green] (for SymbiYosys)")
667
+ else:
668
+ console.print(f" [yellow]⚠ Could not auto-convert SVA to Yosys format. Using fallback.[/yellow]")
669
+ # Fallback: just use the original (may fail on complex SVA)
670
 
671
+ # Write SBY Config (uses _sby_check.sv)
672
+ write_sby_config(name, use_sby_check=True)
673
 
674
  # Run Formal Verification
675
  formal_success, formal_msg = run_formal_verification(name)
676
 
677
  if formal_success:
678
+ console.print(f" ✓ [bold green]Mathematical Proof PASSED (k-induction)[/bold green]")
679
  log_thinking(formal_msg, step="Formal Verification Log")
680
  else:
681
  # Check for missing tool vs actual failure
 
683
  console.print(f" [yellow]⚠ Formal Verification Skipped[/yellow]: [dim]SymbiYosys (sby) not installed.[/dim]")
684
  console.print(f" [dim]- Install: https://github.com/YosysHQ/oss-cad-suite-build[/dim]")
685
  else:
686
+ console.print(f" ✗ [bold red]Formal Proof FAILED[/bold red]")
687
+ console.print(f" [dim]Note: Industry SVA ({name}_sva.sv) is preserved for commercial tools.[/dim]")
688
+ # Don't print full error, just note
689
 
690
  # ===== STEP 3: Generate Testbench (self-checking) =====
691
  console.print("\n[bold yellow]━━━ Step 4/6: Generating Testbench (Spec + RTL Analysis) ━━━[/bold yellow]")
 
716
  3. **Data Types**: Use `logic` for everything.
717
  4. **Instantiation**: Use explicit name based connection `.port(signal)`.
718
  5. **Clock/Reset**:
719
+ - Clock: `initial clk = 0; always #5 clk = ~clk;`
720
+ - Reset: Drive `rst_n` low for 4 cycles, then high.
721
+ 6. **Timing & Handshaking (CRITICAL - READ CAREFULLY)**:
722
+ - **ANALYZE THE FSM**: Count how many states the DUT has. If it has N states, wait at least N+5 cycles.
723
+ - **NEVER check outputs immediately after setting inputs** - always wait!
724
+ - If the DUT has a `valid`, `done`, or `ready` signal, use: `while(!valid) @(posedge clk);`
725
+ - If no done signal, use `repeat(25) @(posedge clk);` to allow FSM to complete.
726
+ - For pipeline designs, wait at least (pipeline_depth + 5) cycles.
727
+ - **COMMON MISTAKE**: Checking output 1 cycle after input = TEST FAILS. Wait 20+ cycles minimum for FSMs.
728
+ 7. **Test Structure**:
729
+ - After each test case, wait for DUT to return to IDLE before next test.
730
+ - Use generous timeouts: `repeat(30) @(posedge clk);` between test cases.
731
+ 8. **Reporting**:
732
  - Use `$dumpfile("{name}.vcd")` and `$dumpvars(0, {name}_tb)`.
733
  - On success: `$display("TEST PASSED");`
734
  - On failure: `$display("TEST FAILED");`
src/agentic/config.py CHANGED
@@ -60,3 +60,7 @@ LLM_API_KEY = LOCAL_CONFIG["api_key"]
60
  # Tool Settings
61
  PDK_ROOT = os.environ.get('PDK_ROOT', os.path.expanduser('~/.ciel'))
62
  OPENLANE_IMAGE = "ghcr.io/the-openroad-project/openlane:ff5509f65b17bfa4068d5336495ab1718987ff69-amd64"
 
 
 
 
 
60
  # Tool Settings
61
  PDK_ROOT = os.environ.get('PDK_ROOT', os.path.expanduser('~/.ciel'))
62
  OPENLANE_IMAGE = "ghcr.io/the-openroad-project/openlane:ff5509f65b17bfa4068d5336495ab1718987ff69-amd64"
63
+
64
+ # OSS CAD Suite (SymbiYosys, Yosys) - Self-contained within AgentIC
65
+ OSS_CAD_SUITE_ROOT = os.environ.get('OSS_CAD_SUITE_HOME', os.path.join(WORKSPACE_ROOT, 'oss-cad-suite'))
66
+ SBY_BIN = os.path.join(OSS_CAD_SUITE_ROOT, 'bin', 'sby')
src/agentic/tools/vlsi_tools.py CHANGED
@@ -3,12 +3,12 @@ import os
3
  import re
4
  import subprocess
5
  from crewai.tools import tool
6
- from ..config import OPENLANE_ROOT, SCRIPTS_DIR, PDK_ROOT, OPENLANE_IMAGE
7
 
8
- def SecurityCheck(rtl_code: str) -> bool:
9
  """
10
  Performs a static security analysis on the generated RTL.
11
- Returns True if safe, False if malicious patterns detected,
12
  """
13
  # 1. Blacklist malicious system calls in Verilog
14
  # (Though Icarus usually ignores these in synthesis, they are dangerous in sim)
@@ -23,8 +23,12 @@ def SecurityCheck(rtl_code: str) -> bool:
23
 
24
  return True, "Safe"
25
 
26
- def write_config(design_name, code):
27
  """Writes config.tcl to the OpenLane design directory."""
 
 
 
 
28
  path = f"{OPENLANE_ROOT}/designs/{design_name}/config.tcl"
29
  os.makedirs(os.path.dirname(path), exist_ok=True)
30
 
@@ -41,13 +45,24 @@ def write_config(design_name, code):
41
 
42
  # Remove "Thought:" lines
43
  clean_code = re.sub(r'^(Thought|Action|Observation):.*$', '', clean_code, flags=re.MULTILINE)
44
-
45
- with open(path, "w") as f:
46
- f.write(clean_code)
47
- return path
48
-
49
- def write_verilog(design_name, code, is_testbench=False, suffix=None, ext=".v"):
50
- """Writes Verilog code to the OpenLane design directory."""
 
 
 
 
 
 
 
 
 
 
 
51
  if suffix:
52
  file_suffix = suffix
53
  else:
@@ -141,22 +156,34 @@ def write_verilog(design_name, code, is_testbench=False, suffix=None, ext=".v"):
141
  clean_code = clean_code.replace(" begin ", " begin\n")
142
  clean_code = clean_code.replace(" end ", "\nend ")
143
 
144
- with open(path, "w") as f:
145
- f.write(clean_code)
146
- return path
 
 
 
147
 
148
- def run_syntax_check(file_path: str):
149
  """
150
  Runs iverilog syntax check on a Verilog file.
151
  Returns: (True, "OK") if clean, or (False, "Error message") if failed.
152
  """
153
- result = subprocess.run(
154
- ["iverilog", "-g2012", "-t", "null", file_path],
155
- capture_output=True, text=True
156
- )
157
- if result.returncode == 0:
158
- return True, "Syntax OK"
159
- return False, result.stderr
 
 
 
 
 
 
 
 
 
160
 
161
  @tool("Syntax Checker")
162
  def syntax_check_tool(file_path: str):
@@ -167,9 +194,147 @@ def syntax_check_tool(file_path: str):
167
  """
168
  return run_syntax_check(file_path)
169
 
170
- def write_sby_config(design_name):
171
- """Writes a default SBY config for the design."""
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
172
  path = f"{OPENLANE_ROOT}/designs/{design_name}/src/{design_name}.sby"
 
 
 
173
  config = f"""[options]
174
  mode prove
175
 
@@ -178,12 +343,12 @@ smtbmc
178
 
179
  [script]
180
  read -formal {design_name}.v
181
- read -formal {design_name}_sva.sv
182
  prep -top {design_name}
183
 
184
  [files]
185
  {design_name}.v
186
- {design_name}_sva.sv
187
  """
188
  with open(path, "w") as f:
189
  f.write(config)
@@ -197,18 +362,22 @@ def run_formal_verification(design_name):
197
  if not os.path.exists(sby_file):
198
  return False, "SBY configuration file not found."
199
 
200
- # Run SBY
 
201
  try:
202
  result = subprocess.run(
203
- ["sby", "-f", f"{design_name}.sby"],
204
  cwd=design_dir,
205
  capture_output=True,
206
- text=True
 
207
  )
208
  if result.returncode == 0:
209
- return True, f"Formal Verification PASSED.\\n{result.stdout}"
210
  else:
211
- return False, f"Formal Verification FAILED:\\n{result.stdout}\\n{result.stderr}"
 
 
212
  except FileNotFoundError:
213
  return False, "SymbiYosys (sby) tool not installed/found in path."
214
 
@@ -269,18 +438,30 @@ def check_physical_metrics(design_name):
269
  except Exception as e:
270
  return None, f"Error parsing metrics: {str(e)}"
271
 
272
- def run_simulation(design_name):
273
  """Compiles and runs the testbench simulation."""
274
  src_dir = f"{OPENLANE_ROOT}/designs/{design_name}/src"
275
  rtl_file = f"{src_dir}/{design_name}.v"
276
  tb_file = f"{src_dir}/{design_name}_tb.v"
277
  sim_out = f"{src_dir}/sim"
278
 
 
 
 
 
 
 
279
  # Compile
280
- compile_result = subprocess.run(
281
- ["iverilog", "-g2012", "-o", sim_out, rtl_file, tb_file],
282
- capture_output=True, text=True
283
- )
 
 
 
 
 
 
284
  if compile_result.returncode != 0:
285
  return False, f"Compilation failed:\n{compile_result.stderr}"
286
 
@@ -394,13 +575,33 @@ def run_openlane(design_name, background=False):
394
  error_text = (process.stdout + "\n" + error_text).strip()
395
  return False, error_text
396
 
397
- def run_verification(design_name):
398
- """Runs the verify_design.sh script."""
 
 
 
 
 
 
 
 
 
 
 
399
  script_path = os.path.join(SCRIPTS_DIR, "verify_design.sh")
400
 
401
- result = subprocess.run(
402
- ["bash", script_path, design_name],
403
- capture_output=True,
404
- text=True
405
- )
406
- return result.stdout
 
 
 
 
 
 
 
 
 
 
3
  import re
4
  import subprocess
5
  from crewai.tools import tool
6
+ from ..config import OPENLANE_ROOT, SCRIPTS_DIR, PDK_ROOT, OPENLANE_IMAGE, SBY_BIN
7
 
8
+ def SecurityCheck(rtl_code: str) -> tuple:
9
  """
10
  Performs a static security analysis on the generated RTL.
11
+ Returns (True, "Safe") if safe, or (False, "reason") if malicious patterns detected.
12
  """
13
  # 1. Blacklist malicious system calls in Verilog
14
  # (Though Icarus usually ignores these in synthesis, they are dangerous in sim)
 
23
 
24
  return True, "Safe"
25
 
26
+ def write_config(design_name: str, code: str) -> str:
27
  """Writes config.tcl to the OpenLane design directory."""
28
+ # Input validation - prevent path traversal
29
+ if not design_name or '..' in design_name or '/' in design_name:
30
+ raise ValueError(f"Invalid design name: {design_name}")
31
+
32
  path = f"{OPENLANE_ROOT}/designs/{design_name}/config.tcl"
33
  os.makedirs(os.path.dirname(path), exist_ok=True)
34
 
 
45
 
46
  # Remove "Thought:" lines
47
  clean_code = re.sub(r'^(Thought|Action|Observation):.*$', '', clean_code, flags=re.MULTILINE)
48
+
49
+ try:
50
+ with open(path, "w") as f:
51
+ f.write(clean_code)
52
+ return path
53
+ except IOError as e:
54
+ raise IOError(f"Failed to write config file {path}: {str(e)}")
55
+
56
+ def write_verilog(design_name: str, code: str, is_testbench: bool = False, suffix: str = None, ext: str = ".v") -> str:
57
+ """Writes Verilog code to the OpenLane design directory.
58
+
59
+ Returns:
60
+ str: Path to the written file, or error message string starting with 'Error:'
61
+ """
62
+ # Input validation - prevent path traversal attacks
63
+ if not design_name or '..' in design_name or '/' in design_name:
64
+ return f"Error: Invalid design name: {design_name}"
65
+
66
  if suffix:
67
  file_suffix = suffix
68
  else:
 
156
  clean_code = clean_code.replace(" begin ", " begin\n")
157
  clean_code = clean_code.replace(" end ", "\nend ")
158
 
159
+ try:
160
+ with open(path, "w") as f:
161
+ f.write(clean_code)
162
+ return path
163
+ except IOError as e:
164
+ return f"Error: Failed to write Verilog file {path}: {str(e)}"
165
 
166
+ def run_syntax_check(file_path: str) -> tuple:
167
  """
168
  Runs iverilog syntax check on a Verilog file.
169
  Returns: (True, "OK") if clean, or (False, "Error message") if failed.
170
  """
171
+ if not os.path.exists(file_path):
172
+ return False, f"File not found: {file_path}"
173
+
174
+ try:
175
+ result = subprocess.run(
176
+ ["iverilog", "-g2012", "-t", "null", file_path],
177
+ capture_output=True, text=True,
178
+ timeout=60 # 1 minute timeout for syntax check
179
+ )
180
+ if result.returncode == 0:
181
+ return True, "Syntax OK"
182
+ return False, result.stderr
183
+ except subprocess.TimeoutExpired:
184
+ return False, "Syntax check timed out (>60s). File may be too large or malformed."
185
+ except FileNotFoundError:
186
+ return False, "iverilog not found. Please install Icarus Verilog."
187
 
188
  @tool("Syntax Checker")
189
  def syntax_check_tool(file_path: str):
 
194
  """
195
  return run_syntax_check(file_path)
196
 
197
+ def convert_sva_to_yosys(sva_content: str, module_name: str) -> str:
198
+ """
199
+ Converts industry-standard SVA (property/assert property) to Yosys-compatible
200
+ immediate assertions (always @(...) assert(...)).
201
+
202
+ This allows designs to maintain industry-standard SVA files while still
203
+ being verifiable with open-source tools.
204
+
205
+ Args:
206
+ sva_content: The full SVA file content
207
+ module_name: Name of the DUT module
208
+
209
+ Returns:
210
+ str: Yosys-compatible assertion module
211
+ """
212
+ # Extract port list from the original SVA module
213
+ port_match = re.search(r'module\s+\w+_sva\s*\((.*?)\);', sva_content, re.DOTALL)
214
+ if not port_match:
215
+ return None
216
+
217
+ ports_section = port_match.group(1)
218
+
219
+ # Parse port declarations
220
+ port_lines = []
221
+ for line in ports_section.split('\n'):
222
+ line = line.strip()
223
+ if line and not line.startswith('//'):
224
+ port_lines.append(line.rstrip(','))
225
+
226
+ # Extract property assertions
227
+ # Captures: property name; <body> endproperty
228
+ # Then parse the body for @(posedge clk) condition;
229
+ raw_properties = re.findall(
230
+ r'property\s+(\w+)\s*;(.*?)endproperty',
231
+ sva_content, re.DOTALL
232
+ )
233
+
234
+ # Parse each property body
235
+ properties = []
236
+ for prop_name, body in raw_properties:
237
+ # Extract clock and condition from body
238
+ body_match = re.search(r'@\(posedge\s+(\w+)\)\s*(.+?);', body.strip(), re.DOTALL)
239
+ if body_match:
240
+ clk = body_match.group(1)
241
+ condition = body_match.group(2).strip()
242
+ properties.append((prop_name, clk, condition))
243
+
244
+ # Build Yosys-compatible module
245
+ yosys_code = f'''// AUTO-GENERATED: Yosys-compatible assertions for {module_name}
246
+ // Original industry-standard SVA is preserved in {module_name}_sva.sv
247
+ // This file is used ONLY for open-source formal verification (SymbiYosys)
248
+
249
+ module {module_name}_sby_check (
250
+ {chr(10).join(" " + p + "," for p in port_lines[:-1])}
251
+ {port_lines[-1] if port_lines else ""}
252
+ );
253
+
254
+ // Track previous values for temporal checks
255
+ reg init_done = 0;
256
+ '''
257
+
258
+ # Find all signals that need $past tracking
259
+ past_signals = set(re.findall(r'\$past\((\w+)\)', sva_content))
260
+ for sig in past_signals:
261
+ # Try to find width from port declarations
262
+ width_match = re.search(rf'\[(\d+):(\d+)\]\s*{sig}', sva_content)
263
+ if width_match:
264
+ hi, lo = width_match.groups()
265
+ yosys_code += f" reg [{hi}:{lo}] past_{sig};\n"
266
+ else:
267
+ yosys_code += f" reg past_{sig};\n"
268
+
269
+ # Add clock tracking
270
+ clk_name = "clk"
271
+ clk_match = re.search(r'@\(posedge\s+(\w+)\)', sva_content)
272
+ if clk_match:
273
+ clk_name = clk_match.group(1)
274
+
275
+ yosys_code += f'''
276
+ always @(posedge {clk_name}) begin
277
+ init_done <= 1;
278
+ '''
279
+ for sig in past_signals:
280
+ yosys_code += f" past_{sig} <= {sig};\n"
281
+ yosys_code += " end\n\n"
282
+
283
+ # Convert each property to immediate assertion
284
+ for prop_name, clk, condition in properties:
285
+ # Replace $past(x) with past_x
286
+ cond = condition.strip()
287
+ for sig in past_signals:
288
+ cond = cond.replace(f'$past({sig})', f'past_{sig}')
289
+
290
+ # Parse implication operator |=>
291
+ if '|=>' in cond:
292
+ antecedent, consequent = cond.split('|=>')
293
+ antecedent = antecedent.strip()
294
+ consequent = consequent.strip()
295
+
296
+ # Handle disable iff
297
+ disable_cond = ""
298
+ if 'disable iff' in antecedent:
299
+ disable_match = re.search(r'disable\s+iff\s*\(([^)]+)\)', antecedent)
300
+ if disable_match:
301
+ disable_cond = disable_match.group(1)
302
+ antecedent = re.sub(r'disable\s+iff\s*\([^)]+\)\s*', '', antecedent)
303
+
304
+ yosys_code += f" // Property: {prop_name}\n"
305
+ yosys_code += f" always @(posedge {clk}) begin\n"
306
+ if disable_cond:
307
+ yosys_code += f" if (!({disable_cond}) && init_done && ({antecedent.strip()}))\n"
308
+ else:
309
+ yosys_code += f" if (init_done && ({antecedent.strip()}))\n"
310
+ yosys_code += f" assert({consequent.strip()});\n"
311
+ yosys_code += f" end\n\n"
312
+ else:
313
+ # Simple assertion without implication
314
+ yosys_code += f" // Property: {prop_name}\n"
315
+ yosys_code += f" always @(posedge {clk}) begin\n"
316
+ yosys_code += f" assert({cond});\n"
317
+ yosys_code += f" end\n\n"
318
+
319
+ yosys_code += f'''endmodule
320
+
321
+ // Bind to DUT
322
+ bind {module_name} {module_name}_sby_check sby_inst (.*);
323
+ '''
324
+
325
+ return yosys_code
326
+
327
+ def write_sby_config(design_name, use_sby_check: bool = True):
328
+ """Writes a default SBY config for the design.
329
+
330
+ Args:
331
+ design_name: Name of the design
332
+ use_sby_check: If True, use the Yosys-compatible _sby_check.sv file
333
+ """
334
  path = f"{OPENLANE_ROOT}/designs/{design_name}/src/{design_name}.sby"
335
+
336
+ sva_file = f"{design_name}_sby_check.sv" if use_sby_check else f"{design_name}_sva.sv"
337
+
338
  config = f"""[options]
339
  mode prove
340
 
 
343
 
344
  [script]
345
  read -formal {design_name}.v
346
+ read -formal {sva_file}
347
  prep -top {design_name}
348
 
349
  [files]
350
  {design_name}.v
351
+ {sva_file}
352
  """
353
  with open(path, "w") as f:
354
  f.write(config)
 
362
  if not os.path.exists(sby_file):
363
  return False, "SBY configuration file not found."
364
 
365
+ # Run SBY (using bundled binary)
366
+ sby_cmd = SBY_BIN if os.path.exists(SBY_BIN) else "sby"
367
  try:
368
  result = subprocess.run(
369
+ [sby_cmd, "-f", f"{design_name}.sby"],
370
  cwd=design_dir,
371
  capture_output=True,
372
+ text=True,
373
+ timeout=600 # 10 minute timeout for formal verification
374
  )
375
  if result.returncode == 0:
376
+ return True, f"Formal Verification PASSED.\n{result.stdout}"
377
  else:
378
+ return False, f"Formal Verification FAILED:\n{result.stdout}\n{result.stderr}"
379
+ except subprocess.TimeoutExpired:
380
+ return False, "Formal Verification timed out (>10 mins). Design may be too complex for bounded model checking."
381
  except FileNotFoundError:
382
  return False, "SymbiYosys (sby) tool not installed/found in path."
383
 
 
438
  except Exception as e:
439
  return None, f"Error parsing metrics: {str(e)}"
440
 
441
+ def run_simulation(design_name) -> tuple:
442
  """Compiles and runs the testbench simulation."""
443
  src_dir = f"{OPENLANE_ROOT}/designs/{design_name}/src"
444
  rtl_file = f"{src_dir}/{design_name}.v"
445
  tb_file = f"{src_dir}/{design_name}_tb.v"
446
  sim_out = f"{src_dir}/sim"
447
 
448
+ # Validate files exist
449
+ if not os.path.exists(rtl_file):
450
+ return False, f"RTL file not found: {rtl_file}"
451
+ if not os.path.exists(tb_file):
452
+ return False, f"Testbench file not found: {tb_file}"
453
+
454
  # Compile
455
+ try:
456
+ compile_result = subprocess.run(
457
+ ["iverilog", "-g2012", "-o", sim_out, rtl_file, tb_file],
458
+ capture_output=True, text=True,
459
+ timeout=120 # 2 minute timeout for compilation
460
+ )
461
+ except subprocess.TimeoutExpired:
462
+ return False, "Compilation timed out (>120s). Design may be too complex."
463
+ except FileNotFoundError:
464
+ return False, "iverilog not found. Please install Icarus Verilog."
465
  if compile_result.returncode != 0:
466
  return False, f"Compilation failed:\n{compile_result.stderr}"
467
 
 
575
  error_text = (process.stdout + "\n" + error_text).strip()
576
  return False, error_text
577
 
578
+ def run_verification(design_name: str) -> str:
579
+ """Runs the verify_design.sh script.
580
+
581
+ Args:
582
+ design_name: Name of the design to verify
583
+
584
+ Returns:
585
+ str: Output from verification script or error message
586
+ """
587
+ # Input validation
588
+ if not design_name or '..' in design_name or '/' in design_name:
589
+ return f"Error: Invalid design name: {design_name}"
590
+
591
  script_path = os.path.join(SCRIPTS_DIR, "verify_design.sh")
592
 
593
+ if not os.path.exists(script_path):
594
+ return f"Error: Verification script not found: {script_path}"
595
+
596
+ try:
597
+ result = subprocess.run(
598
+ ["bash", script_path, design_name],
599
+ capture_output=True,
600
+ text=True,
601
+ timeout=300 # 5 minute timeout for verification
602
+ )
603
+ return result.stdout + (result.stderr if result.stderr else "")
604
+ except subprocess.TimeoutExpired:
605
+ return "Error: Verification timed out (>5 mins)."
606
+ except Exception as e:
607
+ return f"Error running verification: {str(e)}"