From ad56ad44c3bdd3d075a32879785a04e3e30491eb Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 24 Aug 2016 23:18:29 +0200 Subject: [PATCH] More yosys-smtbmc smtc features --- backends/smt2/smtbmc.py | 74 ++++++++++++++++++++++++++++++-------- examples/smtbmc/.gitignore | 5 ++- examples/smtbmc/Makefile | 15 +++++--- examples/smtbmc/demo3.smtc | 5 +++ examples/smtbmc/demo3.v | 18 ++++++++++ 5 files changed, 97 insertions(+), 20 deletions(-) create mode 100644 examples/smtbmc/demo3.smtc create mode 100644 examples/smtbmc/demo3.v diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 1c017df18..9dba68b2a 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -20,6 +20,7 @@ import os, sys, getopt, re ##yosys-sys-path## from smtio import smtio, smtopts, mkvcd +from collections import defaultdict skip_steps = 0 step_size = 1 @@ -120,43 +121,70 @@ if tempind and len(inconstr) != 0: sys.exit(1) -constr_asserts = dict() -constr_assumes = dict() +constr_asserts = defaultdict(list) +constr_assumes = defaultdict(list) for fn in inconstr: - current_state = None + current_states = None with open(fn, "r") as f: for line in f: + if line.startswith("#"): + continue + tokens = line.split() if len(tokens) == 0: continue if tokens[0] == "initial": - current_state = 0 + current_states = set() + current_states.add(0) continue if tokens[0] == "state": - current_state = int(tokens[1]) + current_states = set() + for token in tokens[1:]: + tok = token.split(":") + if len(tok) == 1: + current_states.add(int(token)) + elif len(tok) == 2: + lower = int(tok[0]) + if tok[1] == "*": + upper = num_steps + else: + upper = int(tok[1]) + for i in range(lower, upper+1): + current_states.add(i) + else: + assert 0 + continue + + if tokens[0] == "always": + if len(tokens) == 1: + current_states = set(range(0, num_steps+1)) + elif len(tokens) == 2: + i = int(tokens[1]) + assert i < 0 + current_states = set(range(-i, num_steps+1)) + else: + assert 0 continue if tokens[0] == "assert": - assert current_state is not None + assert current_states is not None - if current_state not in constr_asserts: - constr_asserts[current_state] = list() + for state in current_states: + constr_asserts[state].append(" ".join(tokens[1:])) - constr_asserts[current_state].append(" ".join(tokens[1:])) continue if tokens[0] == "assume": - assert current_state is not None + assert current_states is not None - if current_state not in constr_assumes: - constr_assumes[current_state] = list() + for state in current_states: + constr_assumes[state].append(" ".join(tokens[1:])) - constr_assumes[current_state].append(" ".join(tokens[1:])) continue assert 0 @@ -166,9 +194,25 @@ def get_constr_expr(db, state): if state not in db: return "true" + netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)') + + def replace_netref(match): + state_sel = match.group(2) + + if state_sel == "": + st = state + elif state_sel[0] == "-": + st = state + int(state_sel[:-1]) + else: + st = int(state_sel[:-1]) + + expr = smt.net_expr(topmod, "s%d" % st, smt.get_path(topmod, match.group(3))) + + return match.group(1) + expr + expr_list = list() for expr in db[state]: - expr = re.sub(r'\[([^\]]+)\]', lambda match: smt.net_expr(topmod, "s%d" % state, smt.get_path(topmod, match.group(1))), expr) + expr = netref_regex.sub(replace_netref, expr) expr_list.append(expr) if len(expr_list) == 0: @@ -430,7 +474,7 @@ if tempind: break -else: # not tempind, not gentrace +else: # not tempind step = 0 retstatus = True while step < num_steps: diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore index 1c9afd5ba..bf83e0d44 100644 --- a/examples/smtbmc/.gitignore +++ b/examples/smtbmc/.gitignore @@ -1,9 +1,12 @@ demo1.smt2 demo1.yslog demo2.smt2 +demo2.smtc demo2.vcd demo2.yslog demo2_tb -demo2_tb.smtc demo2_tb.v demo2_tb.vcd +demo3.smt2 +demo3.vcd +demo3.yslog diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile index a266567e4..b3feb07c7 100644 --- a/examples/smtbmc/Makefile +++ b/examples/smtbmc/Makefile @@ -1,24 +1,31 @@ -all: demo1 demo2 +all: demo1 demo2 demo3 demo1: demo1.smt2 yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2 yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2 demo2: demo2.smt2 - yosys-smtbmc -g --dump-vcd demo2.vcd --dump-vlogtb demo2_tb.v --dump-smtc demo2_tb.smtc demo2.smt2 + yosys-smtbmc -g --dump-vcd demo2.vcd --dump-smtc demo2.smtc --dump-vlogtb demo2_tb.v demo2.smt2 iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v vvp demo2_tb +vcd=demo2_tb.vcd +demo3: demo3.smt2 + yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2 + demo1.smt2: demo1.v yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2' demo2.smt2: demo2.v yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires -mem -bv demo2.smt2' +demo3.smt2: demo3.v + yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires -mem -bv demo3.smt2' + clean: rm -f demo1.yslog demo1.smt2 demo1.vcd - rm -f demo2.yslog demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd demo2_tb.smtc + rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd + rm -f demo3.yslog demo3.smt2 demo3.vcd -.PHONY: demo1 clean +.PHONY: demo1 demo2 demo3 clean diff --git a/examples/smtbmc/demo3.smtc b/examples/smtbmc/demo3.smtc new file mode 100644 index 000000000..f5e017cf0 --- /dev/null +++ b/examples/smtbmc/demo3.smtc @@ -0,0 +1,5 @@ +initial +assume [rst] + +always -1 +assert (= [-1:mem] [mem]) diff --git a/examples/smtbmc/demo3.v b/examples/smtbmc/demo3.v new file mode 100644 index 000000000..13b3a1970 --- /dev/null +++ b/examples/smtbmc/demo3.v @@ -0,0 +1,18 @@ +// Whatever the initial content of this memory is at reset, it will never change +// see demo3.smtc for assumptions and assertions + +module demo3(input clk, rst, input [15:0] addr, output reg [31:0] data); + reg [31:0] mem [0:2**16-1]; + reg [15:0] addr_q; + + always @(posedge clk) begin + if (rst) begin + data <= mem[0] ^ 123456789; + addr_q <= 0; + end else begin + mem[addr_q] <= data ^ 123456789; + data <= mem[addr] ^ 123456789; + addr_q <= addr; + end + end +endmodule -- 2.30.2