菜单
Formal property verification (FPV) and logical equivalence checking (LEC). Use when proving design properties exhaustively, checking RTL vs gate-level netlist equivalence, verifying CDC crossings formally, or closing verification coverage gaps that simulation cannot efficiently reach.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Distil accumulated experience records (experiences.jsonl) into updated domain knowledge summaries (knowledge.md) for any chip-design domain. Run after every 10 orchestrator sessions, or on demand when a domain has collected new issue/fix patterns.
Cross-domain loop orchestration for the chip design pipeline. Provides the fix_request protocol, iteration-cap logic, escalation templates, and dispatch patterns for routing verification/formal failures to the RTL orchestrator and back. Use when driving the closed-loop verification↔RTL feedback cycle.
High-Level Synthesis — C/C++ algorithm analysis, HLS directive optimisation, synthesis execution, and co-simulation verification. Use when converting C/C++ to synthesisable RTL, optimising for latency/throughput/area targets using pragmas, or verifying that generated RTL matches the golden C model.
Static timing analysis — multi-corner constraint validation, setup and hold analysis, timing exception review, and ECO guidance for closure. Use when running timing analysis on a design, reviewing timing violations, guiding ECO fixes, or performing timing sign-off for tape-out.
Microarchitecture exploration, PPA estimation, risk assessment, and architecture sign-off for digital chip design. Use when evaluating design candidates, estimating power/area/performance, assessing technical risk, or producing a microarchitecture document for handoff to RTL design.
Design for Test — scan architecture planning, scan insertion, ATPG pattern generation, MBIST for embedded memories, and JTAG boundary scan. Use when planning a DFT strategy, inserting scan, generating test patterns, or verifying that a chip will be testable in manufacturing.
| name | formal-verification |
| description | Formal property verification (FPV) and logical equivalence checking (LEC). Use when proving design properties exhaustively, checking RTL vs gate-level netlist equivalence, verifying CDC crossings formally, or closing verification coverage gaps that simulation cannot efficiently reach. |
| version | 1.0.0 |
| author | chuanseng-ng |
| license | MIT |
| allowed-tools | Read, Write, Bash |
When this skill is loaded and a user presents a formal verification task, do not
execute stages directly. Immediately spawn the
digital-chip-design-agents:formal-orchestrator agent and pass the full user
request and any available context to it. The orchestrator enforces the stage
sequence, loop-back rules, and sign-off criteria defined below.
Use the domain rules in this file only when the orchestrator reads this skill mid-flow for stage-specific guidance, or when the user asks a targeted reference question rather than requesting a full flow execution.
Before executing or advising on any stage, read the following files if they exist:
memory/formal/knowledge.md — known failure patterns, successful tool flags, PDK/tool quirks.
Incorporate its guidance into every stage decision. If absent, proceed without it.memory/formal/run_state.md — current run identity (run_id, design_name, tool,
last_stage). Use this to resume correctly after interruption. If absent, a new run
is starting; the orchestrator will create this file before the first stage.This pre-run read applies whether this skill is loaded by a user or called by the orchestrator mid-flow. It ensures the fix database is consulted before any diagnosis step.
Exhaustively prove design properties and equivalence using formal methods. Complements simulation-based verification for correctness proofs, protocol compliance, and equivalence checking between RTL and gate-level netlists.
sby) — formal property verification front-end for open-source solversyosys) — synthesis and equivalence checking back-endjg) — industry-standard FPV, CDC, DFT formalvcf) — property checking and equivalence verificationqformal) — FPV and coverage closureassert property (@(posedge clk) !(error && valid));assert property (@(posedge clk) req |-> ##[1:MAX] ack);assert property (@(posedge clk) valid |-> $stable(data));cover property (@(posedge clk) state == DONE);$past(), $rose(), $fell() over manual delay logicdisable iff: use for reset gating// Reset sequence
assume property (@(posedge clk) $rose(rst_n) |-> ##[1:5] rst_n);
// AXI valid stability
assume property (@(posedge clk)
(s_axi_awvalid && !s_axi_awready) |=> $stable(s_axi_awaddr));
| Result | Meaning | Action |
|---|---|---|
| PROVEN | Holds for all reachable states | Log and continue |
| CEX | Counterexample found | Analyse; fix RTL or assumption |
| VACUOUS | Antecedent never fires | Fix assumption or property |
| INCONCLUSIVE | Bound too small or state space too large | Increase bound / abstract |
| UNREACHABLE | Cover never reachable | Verify or waive |
| Failure | Fix |
|---|---|
| Optimizer removed logic | Verify with report_removal; add set_dont_touch if needed |
| SDC mismatch | Ensure same clock groupings in both netlists |
| Scan chain reordering | Use scan-unaware LEC mode |
| Black box mismatch | Align black box list in both netlists |
See plugins/meta/skills/pipeline-orchestration/SKILL.md §Constraints Schema for the authoritative schema and stage-entry validation rule.
No required keys for formal verification — all constraints in this domain are optional.
There are no numeric coverage thresholds unique to formal; this domain shares coverage targets
with the functional-verification domain (coverage.*) and timing targets with the STA domain
(timing.wns_ns_target). When evaluating LEC equivalence or FPV property results, tag
constraint_ref in history entries with the relevant dot-path key if a constraint value was
consulted (e.g. "coverage.functional_pct" when reporting coverage contribution).
After each stage completes (regardless of whether an orchestrator session is active),
write or overwrite one JSON record in memory/formal/experiences.jsonl keyed by
run_id. This ensures data is persisted even if the flow is interrupted or called
without full orchestrator context.
Use run_id = formal_<YYYYMMDD>_<HHMMSS> (set once at flow start; reuse on each
stage update). Every JSON record written must include a top-level "run_id" field
whose value matches this key — stage writes must upsert/overwrite by matching this
persisted run_id. Set signoff_achieved: false until the final sign-off stage
completes.
Write memory/formal/run_state.md as the first action before launching any tool:
run_id: formal_<YYYYMMDD>_<HHMMSS>
design_name: <design>
tool: <primary tool>
start_time: <ISO-8601>
last_stage: null
current_stage: <first stage name>
Update current_stage when a stage starts, and set last_stage to the completed stage
name only after successful completion (then clear current_stage). This file lets
wakeup-loop prompts and resumed sessions identify the correct run and distinguish
completed vs in-flight work. Create the file and parent directories if they do not exist.
If mcp__plugin_ecc_memory__add_observations is available in this session, emit each
applied fix as an observation to entity chip-design-formal-fixes after writing to
experiences.jsonl. Skip silently if the tool is absent — JSONL is the canonical record.