Ghost Bike Dock

Dock 7 at the Riverside bike-share station jams a few times a week. The app shows a bike present, and the locking jaw's solenoid (the electromagnet that drives the jaw) buzzes at full current. But there is no bike in the dock at all. The operations team calls them ghost bikes. Maintenance has replaced two burned-out solenoids this season. The station logs show the jam always follows a rental by one of the fast regulars: commuters who pull the bike out before the buzz has finished.

The block in your editor is the jaw controller as it shipped. Slow customers run the intended cycle a thousand times a day without trouble, and the test rig only ever tried that path. The fast regulars free the bike a couple of cycles into the pull, so removed_i pulses while the solenoid is still in its 4-cycle window. Follow the shipped state machine with a pulse arriving there, and you will see exactly how dock 7 gets stuck.

Your task: fix the controller in place, so that a fast pull ends the same way a slow one does. Bike gone, jaw released, app showing an empty dock.

Interface

Behavior

• After reset the dock is HOLDING: occupied_o = 1, unlock_o = 0
• A tap_i sampled while HOLDING starts the pull: unlock_o is high for exactly the next four cycles
• If removed_i was high during any of those four cycles, the dock goes straight to EMPTY when the window ends
• Straight to EMPTY means unlock_o and occupied_o both low from the fifth cycle after the tap, with no open-jaw wait
• If removed_i did not arrive during the window, the jaw stays open (unlock_o high, occupied_o high) until the cycle removed_i is sampled
• In that case unlock_o and occupied_o drop together on the next cycle
• In EMPTY, a docked_i pulse returns the dock to HOLDING (occupied_o high the next cycle); tap_i and removed_i are ignored
• tap_i is ignored outside HOLDING
• removed_i is ignored in HOLDING and in EMPTY; docked_i is ignored outside EMPTY
• rst_i = 1 at any rising edge returns the dock to HOLDING, whatever was in flight

What the bench checks

• The testbench checks unlock_o and occupied_o on every cycle
• A slow rental must keep the jaw open after the four-cycle pull window until removed_i arrives
• Removals on the first, middle, and final pull cycles must be remembered while the full window finishes
• Returns must restore occupancy, while taps, removals, and dock events in the wrong states must be ignored
• Reset during either the pull window or open-jaw wait must return the controller to occupied holding state

Constraints

TIMING: everything is synchronous to clk_i; both outputs are decoded from state held in registers and change only at clock edges.

SCOPE: this models the jaw controller's state machine. The solenoid electronics, the card reader, and the app are out of scope; tap_i, removed_i, and docked_i arrive as clean one-cycle pulses.

PULL WINDOW: the four-cycle pull is a mechanical requirement and must not shrink.

The template contains the shipped controller: fix it in place rather than starting over.

Do not add ports.