Description
Start at the bad acknowledgement, then walk back to the input that should have stopped it.
An acknowledgement appears after cancellation. Read the recorded trace and numbered source, then select the root cause and the line responsible. An abort must cancel the pending acknowledgement on the following sample.
Pinned interface
| Port | Direction | Bits |
|---|---|---|
| clk | input | 1 |
| rst | input | 1 |
| req | input | 1 |
| abort | input | 1 |
| pending | output | 1 |
| ack | output | 1 |
Full specification
Read the recorded solver trace and the numbered source. Choose the root cause and the line that first implements the wrong decision. The assertion checks abort |=> !ack, with reset cancellation.
| Recorded case | Local contract |
|---|---|
| Cancellation trace | Local contract: abort at edge n cancels any pending acknowledgement at n+1. Requests and aborts may coincide. |
| Execution rule | Meaning |
|---|---|
| Interface | Use the pinned port names, directions and bit widths shown above. Observed state and tracker outputs are not environment inputs. |
| Sampling | One positive edge of clk; binary values. Non-overlapping implication observes the next sample. Reset and initialization follow the source and contract above. |
| Submission | Select a cause and a numbered line for every recorded case. Checking these choices runs no engine. |
| How this is graded | The cause and responsible line must agree with each recorded local contract. A timeout or induction candidate must not be diagnosed as a reachable RTL failure. |
Cancellation Trace
Local contract: abort at edge n cancels any pending acknowledgement at n+1. Requests and aborts may coincide.
FAIL · bmc · depth 12 · 497 ms
Samples from the measured run. Free input lanes are shaded; the terminal VCD record is omitted.
Numbered source and task
1 module top(input clk, input rst, input req, input abort, output reg pending=0, output reg ack=0);
2 always @(posedge clk) begin
3 if(rst) begin pending<=0;ack<=0;end
4 else begin
5 pending <= req && !abort;
6 ack <= pending;
7 end
8 end
9 endmoduleRequirements
- Use the published ports and widths. The checker and the DUT variants are owned by the judge.
- Do not add assumptions unless the statement explicitly asks for one. A passing assertion without a reachable trigger is insufficient.
Hints
Hint 1
The contract explicitly permits abort while a request is pending.
Hint 2
Separate the pending-register update from the acknowledgement decision at the same edge.
Hint 3
Use the four-cause triage table in F1.4.
Single clock, binary values, synchronous reset. The judge checks the pinned interface, reachability and the declared proof or bound. UNKNOWN, resource limits and timeouts remain inconclusive.
The recordings are fixed. Checking a diagnosis does not run an engine.
More problems on this topic