A DV engineer needs a first verification plan for DCPeripheral. The specification gives a synchronous active-low reset, a configuration write event, and a depth-four request queue. The useful AI deliverable is a matrix linking requirements to stimulus, observations, and acceptance criteria. An assertion draft is one part of that plan. It cannot replace a reference model, resolve missing interface behavior, or establish signoff by looking plausible.
Requirement | Planned scenario | Expected observation |
|---|---|---|
S1 reset priority | Drive cfg_write with 0xA5 while reset is sampled low | Post-update config_q=0 and occupancy=0 |
S2 accepted write | Outside reset, apply cfg_write with 0xA5 | Post-update config_q=0xA5 |
S2 hold | No accepted write over two edges outside reset | Configuration value stays unchanged |
S3 capacity | Reach occupancy three, then accept enqueue-only | Occupancy becomes four; next acceptance behavior remains TBD |
Give this table to the assistant and ask for one property with an explanation of its sampling. Concurrent assertions sample signals before the design's nonblocking updates at a clock event. A reset branch taking effect after that edge is therefore not generally visible in the property's same-edge sample. This is why a property that looks like a direct English translation may check the wrong instant.
// snippet: synthetic candidate properties; binding context is omitted.
// clk is the sole clock; sampled rst_n is known at the relevant edges.
// config_q has no writer other than the rising-edge sequential process.
ap_reset_visible_next_sample: assert property (@(posedge clk)
(!rst_n) |=> (config_q == 8'h00));
// This intentionally excludes reset edges from the occupancy range check.
ap_occupancy_range: assert property (@(posedge clk)
(rst_n) |-> (occupancy <= 3'd4));For the first candidate, if edge E samples reset low, the reset assignment updates config_q after sampling at E. The consequent at E+1 samples that cleared value before an ordinary write at E+1 updates it. This reasoning depends on there being no intervening writer or asynchronous update. There is deliberately no disable iff (!rst_n) on this reset property: disabling it during reset would remove the condition it is intended to check. A different functional property may need disabling, but that choice needs reset timing and abort semantics explained.
SYNTHETIC hand-derived trace, not simulator output:
edge sampled rst_n sampled config_q value after sequential update
E 0 A5 00
E+1 1 00 3C if cfg_write supplies 3C
The reset property checks the 00 sampled at E+1, not the later 3C.At E the old register is 0xA5 and reset is low. At E+1 reset is high and a write supplies 0x3C. State the sampled values and decide whether the reset candidate should fail. Then list context you need before drafting a response-latency property. Include a way to notice that the reset antecedent never occurred: an assertion that never starts a relevant attempt provides little reassurance.
The samples are A5 at E and 00 at E+1, so the reset candidate should pass this hand trace; 3C appears after the E+1 update. Request acceptance and completion definitions, latency bounds, ordering, reset cancellation, clocking, and monitor sampling. Plan reset-event coverage and an intentional bad reset update to challenge the checker; neither has been executed here.
The range property cannot fail on a two-bit occupancy, so it would not detect the RTL-review width bug, and it does not establish queue ordering, legal acceptance, data integrity, or correct occupancy transitions. Unknown-state policy, initialization, binding scope, simulator support, and functional coverage still require review. Treat every matrix entry as planned, and keep unresolved protocol rows blocked on specification input. Use IEEE 1800-2023, SystemVerilog for sampled-value and implication semantics. These partial properties are teaching drafts, not compile-checked assertions or verification signoff.