From 6e53db0a6696bb6cc121bc7bd8456f56d40f7e83 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 25 Aug 2018 18:21:34 +0200 Subject: [PATCH] Add "pour_853_4" puzzle to examples Signed-off-by: Clifford Wolf --- docs/examples/puzzles/pour_853_to_4.sby | 13 ++++++++ docs/examples/puzzles/pour_853_to_4.sv | 44 +++++++++++++++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 docs/examples/puzzles/pour_853_to_4.sby create mode 100644 docs/examples/puzzles/pour_853_to_4.sv diff --git a/docs/examples/puzzles/pour_853_to_4.sby b/docs/examples/puzzles/pour_853_to_4.sby new file mode 100644 index 0000000..16c4173 --- /dev/null +++ b/docs/examples/puzzles/pour_853_to_4.sby @@ -0,0 +1,13 @@ +[options] +mode cover +depth 100 + +[engines] +smtbmc + +[script] +read -formal pour_853_to_4.sv +prep -top pour_853_to_4 + +[files] +pour_853_to_4.sv diff --git a/docs/examples/puzzles/pour_853_to_4.sv b/docs/examples/puzzles/pour_853_to_4.sv new file mode 100644 index 0000000..ac3fe16 --- /dev/null +++ b/docs/examples/puzzles/pour_853_to_4.sv @@ -0,0 +1,44 @@ +// 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 -- 2.30.2