From 3ec2b6b4e4378373ce1b95348cc314edc66bae38 Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Thu, 9 Apr 2020 19:46:19 +0200 Subject: [PATCH 1/3] 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 From c91efe15a3d98884c4e8fe3c1791581d5753216e Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Tue, 14 Apr 2020 19:54:24 +0200 Subject: [PATCH 2/3] Add a status message when one or more tasks returned a non-zero return code, closes #78 Signed-off-by: Claire Wolf --- sbysrc/sby.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 4bf354f..e546c9c 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -410,4 +410,8 @@ retcode = 0 for t in tasknames: retcode |= run_job(t) +if retcode and (len(tasknames) > 1 or tasknames[0] is not None): + tm = localtime() + print("SBY {:2d}:{:02d}:{:02d} One or more tasks produced a non-zero return code.".format(tm.tm_hour, tm.tm_min, tm.tm_sec)) + sys.exit(retcode) From 69ef444464ef6b79ce4279234898e355d4c41e44 Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Tue, 14 Apr 2020 19:55:14 +0200 Subject: [PATCH 3/3] Add task pattern matching, closes #76 Signed-off-by: Claire Wolf --- sbysrc/sby.py | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index e546c9c..82f6eae 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -17,7 +17,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import argparse, os, sys, shutil, tempfile +import argparse, os, sys, shutil, tempfile, re ##yosys-sys-path## from sby_core import SbyJob, SbyAbort, process_filename from time import localtime @@ -149,6 +149,7 @@ def early_log(workdir, msg): def read_sbyconfig(sbydata, taskname): cfgdata = list() tasklist = list() + task_matched = False pycode = None tasks_section = False @@ -159,7 +160,7 @@ def read_sbyconfig(sbydata, taskname): def handle_line(line): nonlocal pycode, tasks_section, task_tags_active, task_tags_all - nonlocal task_skip_block, task_skiping_blocks + nonlocal task_skip_block, task_skiping_blocks, task_matched line = line.rstrip("\n") line = line.rstrip("\r") @@ -230,11 +231,23 @@ def read_sbyconfig(sbydata, taskname): return line = line.split() if len(line) > 0: - tasklist.append(line[0]) - for t in line: - if taskname == line[0]: - task_tags_active.add(t) - task_tags_all.add(t) + tname = line[0] + tpattern = False + for c in tname: + if c in "(?*.[]|)": + tpattern = True + if not tpattern: + tasklist.append(tname) + task_tags_all.add(tname) + if taskname is not None and re.fullmatch(tname, taskname): + task_matched = True + task_tags_active.add(tname) + for t in line[1:]: + task_tags_active.add(t) + task_tags_all.add(t) + else: + for t in line[1:]: + task_tags_all.add(t) elif line == "[tasks]": if taskname is None: @@ -247,6 +260,10 @@ def read_sbyconfig(sbydata, taskname): for line in sbydata: handle_line(line) + if taskname is not None and not task_matched: + print("ERROR: Task name '{}' didn't match any lines in [tasks].".format(taskname), file=sys.stderr) + sys.exit(1) + return cfgdata, tasklist