14Verification

Read a counter value

Problem

Counter.value is an observation boundary: clients should see the exact 8-bit state held by the counter, and calling it must not create a state transition. The starter violates the observation part of that contract. After mkTop loads 8'h2a, the public run reports decimal 43 instead of 42.

Only repair the implementation of mkCounter. Preserve the interface, the set method, and the supplied top module. A one-sample patch is not enough: the same value implementation must accurately report every representable counter state.

Read, predict, and repair

Read starter/Main.bsv in this order:

Read interface Counter and classify set and value by method kind.
Find the Reg#(Bit#(8)) that owns persistent state.
Trace the load rule through set, then the later show rule through value.
Inspect only the expression that implements value and compare it with the interface contract.

Before editing, predict two cycles. The first rule schedules count to become 8'h2a; that value is visible in the following cycle. The second rule calls a value method, so it performs no write, but the starter's extra transformation changes the reported number. The smallest repair removes that mismatch without changing storage, scheduling, or method kind.

Run after the edit. Completion is observable when the supplied load is reported as decimal 42, value still has a non-Action result type, and reasoning about the expression shows that zero, an ordinary value, and the maximum 8-bit value would all be returned unchanged. Hard-coding the visible sample does not satisfy that contract.

Progressive hints

Hint 1 — identify the owner of the value

The Reg instance is the only declaration here that retains state across cycles. A value method should expose state, not invent another state value.

Hint 2 — narrow the repair

set already schedules the requested value correctly, and show runs one cycle later. The defect is therefore in the assignment-form definition of value.

Hint 3 — choose the expression by contract

Ask which in-scope expression denotes the stored 8-bit state itself. Arithmetic on that expression would make value a transformed view rather than an exact observation.

Transfer experiment

After the required repair works, change the value passed by load to 8'hff and predict the public decimal result before running. This checks that the method observes the full 8-bit state rather than merely reproducing the original sample. Restore the starter scenario before submission.