一键导入
claude-skill-verilog-contracts
Component boundaries, interfaces, bound SVA properties, and conformance-harness discipline for SystemVerilog projects
用 Codex 或 Claude 帮你安装 复制这段 Prompt,粘贴到 Codex、Claude 或其他助手里,让它检查 Skill 页面并帮你完成安装。
菜单
Component boundaries, interfaces, bound SVA properties, and conformance-harness discipline for SystemVerilog projects
用 Codex 或 Claude 帮你安装 复制这段 Prompt,粘贴到 Codex、Claude 或其他助手里,让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
| name | claude-skill-verilog-contracts |
| description | Component boundaries, interfaces, bound SVA properties, and conformance-harness discipline for SystemVerilog projects |
Apply when a project has adopted the component-contracts layout: a shared types package, per-component interface files, bound property modules, and conformance testbenches. If the project has none of these, this skill does not apply — follow only the base style skill and do not invent the missing infrastructure.
Before using this skill, verify the project actually has:
pkg/<project>_types_pkg.sv or similar) imported by implementations.contracts/ or interfaces/) with *_if.sv files.*_properties.sv alongside each interface).tb/ or tb/cocotb/).If any of these are absent, stop and ask before proceeding — do not create the structure speculatively.
Every component boundary consists of three artifacts, authored in this order:
Types — added to the shared types package. All signals crossing module boundaries use named packed struct types. Never introduce a raw logic [N:0] port without first checking whether an appropriate type exists; if it doesn't, add one to the types package before writing the interface.
Interface — one <name>_if.sv file per component boundary. Declares ports and modports for one boundary only. Parameterized by widths, never by behavior. Kept shallow: no nested interfaces inside synthesis paths.
Properties — one <name>_properties.sv file per interface. A separate module containing bound SVA for protocol legality, handshake rules, and latency bounds. Attached to implementations via bind in testbenches, never instantiated inside the implementation itself.
The interface is the shape contract. The properties file is the behavioral contract. Neither alone is sufficient; both are required.
Properties files contain protocol hygiene: handshake legality, no-X on valid cycles, response-after-request ordering, bounded latency, mutual exclusion between signals. Things that can be stated as SVA properties and that hold across all valid inputs.
The conformance testbench contains functional correctness: bit-accurate comparison against a reference model (digital twin, golden trace, or algorithmic spec). Things that require specific stimulus and observation of outputs over time.
Do not assert functional correctness in SVA. Do not assert protocol properties only in the testbench. Keeping these separate prevents properties files from sprawling into speculative half-working behavioral specs.
Every named type has a comment stating its purpose and, where applicable, its Q-format annotation:
package example_types_pkg;
// Request from client to cache
typedef struct packed {
logic [31:0] addr; // Byte address
logic [7:0] len; // Burst length minus 1
logic [3:0] id; // Transaction ID
} cache_req_t;
// Fixed-point gain, Q4.12
typedef logic signed [15:0] gain_q4_12_t;
endpackage
Never define the same concept as a raw vector in one place and a packed struct in another. If the types package has cache_req_t, the interface uses it; ports do not accept a flattened equivalent.
interface cache_if
import example_types_pkg::*;
(
input logic clk,
input logic rst_n
);
cache_req_t req;
logic req_valid;
logic req_ready;
cache_resp_t resp;
logic resp_valid;
modport client (
output req, req_valid,
input req_ready,
input resp, resp_valid
);
modport server (
input req, req_valid,
output req_ready,
output resp, resp_valid
);
modport monitor (
input req, req_valid, req_ready,
input resp, resp_valid
);
endinterface
client, server, and monitor modports. The monitor modport is required for property binding.Properties are authored as a module taking the interface's monitor modport:
module cache_properties (cache_if.monitor bus);
// Handshake: req_valid must not drop while ready is pending
property p_req_stable_until_ready;
@(posedge bus.clk) disable iff (!bus.rst_n)
bus.req_valid && !bus.req_ready |=>
bus.req_valid && $stable(bus.req);
endproperty
assert property (p_req_stable_until_ready)
else $error("req dropped or changed before ready");
// Bounded response latency
localparam int MAX_LAT = 32;
property p_resp_within_latency;
@(posedge bus.clk) disable iff (!bus.rst_n)
(bus.req_valid && bus.req_ready) |-> ##[1:MAX_LAT] bus.resp_valid;
endproperty
assert property (p_resp_within_latency)
else $error("no response within MAX_LAT cycles");
endmodule
Attached in the testbench, not in the implementation:
bind cache_bram cache_properties props (.bus(cache_bus));
Rules:
p_.else $error(...) with a human-readable message.disable iff (!rst_n) uniformly.initial or always blocks in properties files. Properties only.A conformance testbench proves that an implementation satisfies the contract. It must:
server (or client) modport.client (or server) modport.The testbench is the executable definition of "this implementation satisfies the contract." Passing lint is necessary but not sufficient. Passing properties is necessary but not sufficient. Passing the trace diff against the reference is also necessary. All three are required for acceptance.
A project using this skill typically has something like:
rtl/
├── pkg/
│ └── <project>_types_pkg.sv
├── contracts/
│ ├── <name>_if.sv
│ └── <name>_properties.sv
└── <component>/
└── <component>.sv
tb/
└── <name>_conformance/
Do not move files between these directories without being asked. Do not create parallel organizational schemes.
When asked to implement a new component that has a contract:
When asked to add a new component that does not yet have a contract:
Never write an implementation before the properties exist. The properties are the specification; writing the implementation first and the properties afterward produces properties that describe what the implementation happens to do rather than what it should do.
If the component was authored under this discipline (has matching interface, properties, and conformance testbench): modify all four artifacts together, keeping them in sync. If the change is to the contract itself, expect the conformance harness to fail until implementations are updated — this is intended.
If the component predates this discipline: do not retrofit it unless explicitly asked. Work within its existing structure. Retrofitting in the course of unrelated work is how projects lose a weekend.
A component change is not complete until the single project-level check command (typically scripts/check_contract.sh <component> or a make target) reports success. That command must cover:
--lint-only -Wall -Wpedantic, no suppressions)."Lint passes" is not acceptance. "My testbench works" is not acceptance. The full check command passing is acceptance. Do not claim completion otherwise.
contracts/ does not exist in the project, do not create it and scatter files into it. Ask.bind. They never appear in synthesizable source.