This workspace is organized around Synopsys VC Formal / FSV, OpenTitan RTL, security information-flow verification, blackbox strategy analysis, and LLM-assisted RTL analysis. The top-level directory contains experiment workspaces, analysis scripts, third-party RTL sources, and verification results.

VCF_workplace/
├── baseline_bb_strategy/  # Baseline blackbox strategy tool based on RTL hierarchy and properties
├── COI_analysis/          # COI report post-processing: module statistics and hierarchy visualization
├── FSV/                   # VC Formal FSV experiments, TCL scripts, traces, and results
├── llm4fsv/               # LLM-assisted RTL blackboxing and hardware security analysis
├── opensource_llm/        # Local/open-source LLM integration, including Ollama model management and RTL APIs
├── opentitan/             # OpenTitan source snapshot used as the main RTL / DV / SW reference
├── sv2dag/                # RTL-to-graph conversion, DAG/path analysis, and module scoring scripts
├── .certitudeGUI/         # Synopsys/Certitude GUI configuration or state directory
├── setup_vcf.sh           # VC Formal environment setup script
└── __init__.py            # Python package marker

Generated files commonly appear under __pycache__/, FSV/*/vcst_rtdb/, llm4fsv/output/, and sv2dag/*_sv2dag/. The FSV/*/run/ directories may contain both useful TCL scripts and generated logs, so review them before committing.

Enter the workspace:

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace

Load the VC Formal environment:

source setup_vcf.sh

Check the current git status:

git status

Python tools are best run from an isolated environment. llm4fsv provides a conda environment file:

cd llm4fsv
conda env create -f environment.yml
conda activate llm4fsv
pip install -r requirements.txt

For lightweight scripts, installing the relevant subdirectory's requirements.txt in your current Python environment may be enough.

FSV experiments are mainly stored under FSV/. Each experiment directory usually contains:

• design/: RTL filelists, wrappers, or property-related inputs
• run/: VC Formal TCL scripts and run logs
• trace_*: trace/play scripts generated from FSV properties or counterexamples
• vcst_rtdb/: VC Formal/Verdi runtime database

Example:

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace
source setup_vcf.sh

cd FSV/fsv_keymgr
vcf -f run/run.tcl

If the VC Formal command name differs on the current machine, inspect the executables under $VC_STATIC_HOME/bin:

echo "$VC_STATIC_HOME"
ls "$VC_STATIC_HOME/bin"

Common experiment directories:

• FSV/fsv_keymgr/: OpenTitan keymgr information-flow verification experiments
• FSV/fsv_keymgr_baseline/: keymgr baseline or comparison experiments
• FSV/fsv_keymgr_llm/, FSV/fsv_keymgr_llm_2/: LLM-assisted strategy experiments
• FSV/fsv_aes/: AES-related FSV experiments
• FSV/fsv_otbn/: OTBN-related FSV experiments
• FSV/fsv_test/: small test designs
• FSV/run/: older or shared run directory

baseline_bb_strategy/ uses RTL hierarchy and information-flow properties to perform instance-level reachability analysis and report modules that can or cannot be blackboxed.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace/baseline_bb_strategy
python baseline_bb_strategy.py --help

Example:

python baseline_bb_strategy.py \
  --rtl ../llm4fsv/data/rtl_files/src \
  --prop ../llm4fsv/data/properties/information_flow.tcl \
  --stats

Print only blackboxable modules:

python baseline_bb_strategy.py \
  --rtl ../llm4fsv/data/rtl_files/src \
  --prop ../llm4fsv/data/properties/information_flow.tcl \
  --blackbox-only --quiet

llm4fsv/ is an LLM-assisted RTL analysis tool. It supports RTL parsing, blackbox classification, RAG, and hardware security report generation.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace/llm4fsv
conda activate llm4fsv

Configure API keys before the first run:

nano config/my_api_config.py

Run the default analysis:

python main.py

Or use the quick-start script:

./run_analysis.sh

Run the baseline structural heuristic:

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace
python -m llm4fsv.main_baseline \
  --rtl llm4fsv/data/rtl_files/src \
  --prop llm4fsv/data/properties/information_flow.tcl \
  --out llm4fsv/output/results

Run hierarchical analysis:

./run_hierarchical_analysis.sh \
  --top-module keymgr \
  --rtl-dir data/rtl_files/src \
  --max-depth 3

opensource_llm/ provides local LLM deployment and RTL analysis interfaces. The current README mainly targets Ollama-based workflows.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace/opensource_llm
conda activate llm4fsv
pip install -r requirements.txt

Install Ollama:

./install_ollama.sh

List or install recommended models:

python scripts/model_manager.py --list
python scripts/model_manager.py --installed
python scripts/model_manager.py --install qwen2.5-7b

Run the local analysis API on a single Verilog file:

python api/rtl_api.py --file test_module.v --model qwen2.5:7b

sv2dag/ converts RTL into Yosys JSON and then runs graph analyses such as input-to-output influence, output-to-destination path counting, and control-bias scoring.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace/sv2dag

Generate Yosys JSON:

python3 rtl2graphs.py \
  --src-dir keymgr_src \
  --top keymgr \
  --out-dir keymgr_sv2dag \
  --no-cdfg

Compute how many input bits can influence each module instance output:

python3 analyze_module_io_link_score.py \
  --json keymgr_sv2dag/keymgr.json \
  --top keymgr \
  --out-dir keymgr_sv2dag

Count paths from module outputs to a specific destination:

python3 analyze_output_to_dest_path_count.py \
  --json keymgr_sv2dag/keymgr.json \
  --top keymgr \
  --dest keymgr.u_kmac_if.data_o \
  --out-dir keymgr_sv2dag

Aggregate per-bit results into a per-module score:

python3 export_module_score.py \
  --in-csv keymgr_sv2dag/keymgr_output_to_keymgr_u_kmac_if_data_o_path_count_per_bit.csv \
  --out-csv keymgr_sv2dag/keymgr_output_to_keymgr_u_kmac_if_data_o_score_per_module.csv

COI_analysis/ processes COI CSV/log outputs and generates module-level statistics and module hierarchy graphs.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace/COI_analysis

Summarize primary inputs/outputs, registers, nets, ports, and operators per module:

python src/analyze_module_net_port.py \
  coi_report/example.csv \
  --top-name top \
  --output-csv coi_report/module_summary.csv \
  --with-subtypes

Generate a DOT/SVG hierarchy graph from a module table log:

python src/visualize_module_graph.py \
  coi_report/example.log \
  --root top \
  --max-depth 2 \
  --collapse-index

SVG output depends on Graphviz. If Graphviz is not installed, the script may only keep the DOT file or report a Graphviz-related warning.

opentitan/ is an OpenTitan source snapshot used mainly as a reference for RTL, DIFs, software, and utility scripts.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace/opentitan

Read the upstream OpenTitan README:

less README.md

Before using Bazel/Bazelisk, check the upstream OpenTitan documentation and the local machine dependencies:

./bazelisk.sh --version
./bazelisk.sh test //...

opentitan/ is large third-party source content. Avoid modifying it directly unless an experiment explicitly requires it.

cd /var/home/kvf4sf/dailt_workplace/VCF_workplace
git status
git diff

Check for:

• Accidental commits of vcst_rtdb/, large logs, temporary traces, or __pycache__/
• API keys, .env files, private configs, or machine-specific absolute paths
• README commands that no longer match the current experiment paths