Add djb2hash example

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

diff --git a/docs/examples/puzzles/.gitignore b/docs/examples/puzzles/.gitignore
index 0d917a79a3ff7fec5d6a7171de84f863bd5f9a7d..e14320c55680ffe061e98ea9507646eabafe6926 100644 (file)
--- a/docs/examples/puzzles/.gitignore
+++ b/docs/examples/puzzles/.gitignore
@@ -2,3 +2,4 @@
 /primegen_primegen
 /primegen_primes_pass
 /primegen_primes_fail
+/djb2hash

diff --git a/docs/examples/puzzles/djb2hash.sby b/docs/examples/puzzles/djb2hash.sby
new file mode 100644 (file)
index 0000000..e999e70
--- /dev/null
+++ b/docs/examples/puzzles/djb2hash.sby
@@ -0,0 +1,14 @@
+[options]
+mode bmc
+expect fail
+
+[engines]
+smtbmc yices
+
+[script]
+read -noverific
+read -sv djb2hash.sv
+prep -top djb2hash
+
+[files]
+djb2hash.sv

diff --git a/docs/examples/puzzles/djb2hash.sv b/docs/examples/puzzles/djb2hash.sv
new file mode 100644 (file)
index 0000000..493f9be
--- /dev/null
+++ b/docs/examples/puzzles/djb2hash.sv
@@ -0,0 +1,13 @@
+// find a hash collision for DJB2 hash where it visits the same state twice
+module djb2hash (input clock);
+       (* keep *) rand const reg [31:0] magic;
+       (* keep *) rand reg [7:0] inputval;
+       (* keep *) reg [31:0] state = 5381;
+       (* keep *) integer cnt = 0;
+
+       always @(posedge clock) begin
+               state <= ((state << 5) + state) ^ inputval;
+               if (state == magic) cnt <= cnt + 1;
+               assert (cnt < 2);
+       end
+endmodule