From 3ec2b6b4e4378373ce1b95348cc314edc66bae38 Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Thu, 9 Apr 2020 19:46:19 +0200 Subject: [PATCH] Add djb2hash example Signed-off-by: Claire Wolf --- docs/examples/puzzles/.gitignore | 1 + docs/examples/puzzles/djb2hash.sby | 14 ++++++++++++++ docs/examples/puzzles/djb2hash.sv | 13 +++++++++++++ 3 files changed, 28 insertions(+) create mode 100644 docs/examples/puzzles/djb2hash.sby create mode 100644 docs/examples/puzzles/djb2hash.sv diff --git a/docs/examples/puzzles/.gitignore b/docs/examples/puzzles/.gitignore index 0d917a7..e14320c 100644 --- 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 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 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 -- 2.30.2