mirror of
https://github.com/YosysHQ/sby.git
synced 2025-10-28 19:49:25 +00:00
44 lines
1 KiB
Systemverilog
44 lines
1 KiB
Systemverilog
// You are given an 8 litre bucket of water, and two empty buckets which can
|
|
// contain 5 and 3 litre respectively. You are required to divide the water into
|
|
// two by pouring water between buckets (that is, to end up with 4 litre in the 8
|
|
// litre bucket, and 4 litre in the 5 litre bucket).
|
|
//
|
|
// Inspired by:
|
|
// https://github.com/DennisYurichev/random_notes/blob/master/Z3/pour.py
|
|
|
|
module pour_853_to_4 (
|
|
input clk,
|
|
input [1:0] src, dst
|
|
);
|
|
reg [3:0] state [0:2];
|
|
reg [3:0] max_amount [0:2];
|
|
reg [3:0] xfer_amount;
|
|
|
|
initial begin
|
|
state[0] = 8;
|
|
state[1] = 0;
|
|
state[2] = 0;
|
|
|
|
max_amount[0] = 8;
|
|
max_amount[1] = 5;
|
|
max_amount[2] = 3;
|
|
end
|
|
|
|
always @* begin
|
|
assume (src < 3);
|
|
assume (dst < 3);
|
|
assume (src != dst);
|
|
|
|
if (state[src] > (max_amount[dst] - state[dst]))
|
|
xfer_amount = max_amount[dst] - state[dst];
|
|
else
|
|
xfer_amount = state[src];
|
|
|
|
cover (state[0] == 4 && state[1] == 4);
|
|
end
|
|
|
|
always @(posedge clk) begin
|
|
state[src] <= state[src] - xfer_amount;
|
|
state[dst] <= state[dst] + xfer_amount;
|
|
end
|
|
endmodule
|