Merge branch 'master' of https://github.com/YosysHQ/SymbiYosys

docs/examples/puzzles/.gitignore

@@ -2,3 +2,4 @@
 /primegen_primegen
 /primegen_primes_pass
 /primegen_primes_fail
+/djb2hash

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

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