Added smt2-based bmc scripts

5 files changed, 247 insertions, 0 deletions

diff --git a/scripts/smt2-bmc/.gitignore b/scripts/smt2-bmc/.gitignore
new file mode 100644
index 0000000..e3960b1
--- /dev/null
+++ b/scripts/smt2-bmc/.gitignore
@@ -0,0 +1,3 @@
+debug.smt2
+mem_equiv_a.smt2
+mem_equiv_b.smt2
diff --git a/scripts/smt2-bmc/mem_equiv.py b/scripts/smt2-bmc/mem_equiv.py
new file mode 100644
index 0000000..aaf5fdb
--- /dev/null
+++ b/scripts/smt2-bmc/mem_equiv.py
@@ -0,0 +1,165 @@
+#!/usr/bin/python3
+
+import sys, getopt
+import subprocess
+
+steps=15
+debug_print = False
+debug_file = None # open("debug.smt2", "w")
+
+yices = subprocess.Popen(['yices-smt2', '--incremental'], stdin=subprocess.PIPE,
+        stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+
+def yices_write(stmt):
+    stmt = stmt.strip()
+    if debug_print:
+        print("> %s" % stmt)
+    if debug_file:
+        print(stmt, file=debug_file)
+        debug_file.flush()
+    yices.stdin.write(bytes(stmt + "\n", "ascii"))
+    yices.stdin.flush()
+
+def yices_read():
+    stmt = []
+    count_brackets = 0
+
+    while True:
+        line = yices.stdout.readline().decode("ascii").strip()
+        count_brackets += line.count("(")
+        count_brackets -= line.count(")")
+        stmt.append(line)
+        if debug_print:
+            print("< %s" % line)
+        if count_brackets == 0:
+            break
+        if not yices.poll():
+            print("Yices terminated unexpectedly: %s" % "".join(stmt))
+            sys.exit(1)
+
+    stmt = "".join(stmt)
+    if stmt.startswith("(error"):
+        print("Yices Error: %s" % stmt, file=sys.stderr)
+        sys.exit(1)
+
+    return stmt
+
+def yices_parse(stmt):
+    def worker(stmt):
+        if stmt[0] == '(':
+            expr = []
+            cursor = 1
+            while stmt[cursor] != ')':
+                el, le = worker(stmt[cursor:])
+                expr.append(el)
+                cursor += le
+            return expr, cursor+1
+
+        if stmt[0] == '|':
+            expr = "|"
+            cursor = 1
+            while stmt[cursor] != '|':
+                expr += stmt[cursor]
+                cursor += 1
+            expr += "|"
+            return expr, cursor+1
+
+        if stmt[0] in [" ", "\t", "\r", "\n"]:
+            el, le = worker(stmt[1:])
+            return el, le+1
+
+        expr = ""
+        cursor = 0
+        while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
+            expr += stmt[cursor]
+            cursor += 1
+        return expr, cursor
+    return worker(stmt)[0]
+
+def yices_get(mod_name, net_name, state_name):
+    yices_write("(get-value ((|%s_n %s| %s)))" % (mod_name, net_name, state_name))
+    return yices_parse(yices_read())[0][1]
+
+def yices_get_bool(mod_name, net_name, state_name):
+    v = yices_get(mod_name, net_name, state_name)
+    assert v in ["true", "false"]
+    return 1 if v == "true" else 0
+
+yices_write("(set-logic QF_AUFBV)")
+
+with open("mem_equiv_a.smt2", "r") as f:
+    for line in f: yices_write(line)
+
+with open("mem_equiv_b.smt2", "r") as f:
+    for line in f: yices_write(line)
+
+# set-up states and transaction, reset for two cycles
+for i in range(steps):
+    yices_write("(declare-fun a%d () main_a_s)" % i)
+    yices_write("(declare-fun b%d () main_b_s)" % i)
+    if i > 0:
+        yices_write("(assert (main_a_t a%d a%d))" % (i-1, i))
+        yices_write("(assert (main_b_t b%d b%d))" % (i-1, i))
+    if i > 1:
+        yices_write("(assert (|main_a_n resetn| a%d))" % i)
+        yices_write("(assert (|main_b_n resetn| b%d))" % i)
+    else:
+        yices_write("(assert (not (|main_a_n resetn| a%d)))" % i)
+        yices_write("(assert (not (|main_b_n resetn| b%d)))" % i)
+
+# start with synced memory and register file
+yices_write("(assert (= (|main_a_m cpu.cpuregs| a0) (|main_b_m cpu.cpuregs| b0)))")
+yices_write("(assert (= (|main_a_m memory| a0) (|main_b_m memory| b0)))")
+
+# stop with a trap and no pending memory xfer
+yices_write("(assert (not (|main_a_n mem_valid| a%d)))" % (steps-1))
+yices_write("(assert (not (|main_b_n mem_valid| b%d)))" % (steps-1))
+yices_write("(assert (|main_a_n trap| a%d))" % (steps-1))
+yices_write("(assert (|main_b_n trap| b%d))" % (steps-1))
+
+# look for differences in memory or register file
+yices_write(("(assert (or (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)) " +
+        "(distinct (|main_a_m memory| a%d) (|main_b_m memory| b%d))))") % (steps-1, steps-1, steps-1, steps-1))
+
+print("checking...")
+yices_write("(check-sat)")
+
+def print_status(mod, step):
+    resetn = yices_get_bool("main_" + mod, "resetn", "%s%d" % (mod, step))
+    memvld = yices_get_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step))
+    domem  = yices_get_bool("main_" + mod, "domem", "%s%d" % (mod, step))
+    memrdy = yices_get_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step))
+    trap   = yices_get_bool("main_" + mod, "trap", "%s%d" % (mod, step))
+    print("%s[%d]: resetn=%s, memvld=%s, domem=%s, memrdy=%s, trap=%s" % (mod, step, resetn, memvld, domem, memrdy, trap))
+
+def print_mem_xfer(mod, step):
+    yices_write("(get-value ((and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))))" % (mod, mod, step, mod, mod, step))
+    if yices_parse(yices_read())[0][1] == 'true':
+        mem_addr = yices_get("main_" + mod, "mem_addr", "%s%d" % (mod, step))
+        mem_wdata = yices_get("main_" + mod, "mem_wdata", "%s%d" % (mod, step))
+        mem_wstrb = yices_get("main_" + mod, "mem_wstrb", "%s%d" % (mod, step))
+        mem_rdata = yices_get("main_" + mod, "mem_rdata", "%s%d" % (mod, step))
+        print("%s[%d]: addr=%s, wdata=%s, wstrb=%s, rdata=%s" % (mod, step, mem_addr, mem_wdata, mem_wstrb, mem_rdata))
+
+if yices_read() == "sat":
+    print("yices returned sat -> model check failed!")
+
+    print()
+    for i in range(steps):
+        print_status("a", i)
+
+    print()
+    for i in range(steps):
+        print_status("b", i)
+
+    print()
+    for i in range(1, steps):
+        print_mem_xfer("a", i)
+
+    print()
+    for i in range(1, steps):
+        print_mem_xfer("b", i)
+
+else:
+    print("yices returned unsat -> model check passed.")
+
diff --git a/scripts/smt2-bmc/mem_equiv.sh b/scripts/smt2-bmc/mem_equiv.sh
new file mode 100644
index 0000000..ce9486d
--- /dev/null
+++ b/scripts/smt2-bmc/mem_equiv.sh
@@ -0,0 +1,4 @@
+#!/bin/bash
+set -ex
+yosys -qv1 mem_equiv.ys
+time python3 mem_equiv.py 
diff --git a/scripts/smt2-bmc/mem_equiv.v b/scripts/smt2-bmc/mem_equiv.v
new file mode 100644
index 0000000..4c9c3d8
--- /dev/null
+++ b/scripts/smt2-bmc/mem_equiv.v
@@ -0,0 +1,44 @@
+module main (input clk, resetn, domem, output trap);
+	parameter [0:0] ENABLE_REGS_DUALPORT = 1;
+	parameter [0:0] TWO_STAGE_SHIFT = 1;
+	parameter [0:0] TWO_CYCLE_COMPARE = 0;
+	parameter [0:0] TWO_CYCLE_ALU = 0;
+
+	(* keep *) wire mem_valid;
+	(* keep *) wire mem_ready;
+	(* keep *) wire [31:0] mem_addr;
+	(* keep *) wire [31:0] mem_wdata;
+	(* keep *) wire [ 3:0] mem_wstrb;
+	(* keep *) wire [31:0] mem_rdata;
+
+	picorv32 #(
+		.ENABLE_REGS_DUALPORT(ENABLE_REGS_DUALPORT),
+		.TWO_STAGE_SHIFT     (TWO_STAGE_SHIFT     ),
+		.TWO_CYCLE_COMPARE   (TWO_CYCLE_COMPARE   ),
+		.TWO_CYCLE_ALU       (TWO_CYCLE_ALU       )
+	) cpu (
+		.clk      (clk      ),
+		.resetn   (resetn   ),
+		.trap     (trap     ),
+		.mem_valid(mem_valid),
+		.mem_ready(mem_ready),
+		.mem_addr (mem_addr ),
+		.mem_wdata(mem_wdata),
+		.mem_wstrb(mem_wstrb),
+		.mem_rdata(mem_rdata)
+	);
+
+	reg [31:0] memory [0:2**30-1];
+
+	assign mem_ready = domem && resetn && mem_valid;
+	assign mem_rdata = memory[mem_addr >> 2];
+
+	always @(posedge clk) begin
+		if (mem_ready && mem_valid) begin
+			if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0];
+			if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8];
+			if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16];
+			if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24];
+		end
+	end
+endmodule
diff --git a/scripts/smt2-bmc/mem_equiv.ys b/scripts/smt2-bmc/mem_equiv.ys
new file mode 100644
index 0000000..8aa6ba2
--- /dev/null
+++ b/scripts/smt2-bmc/mem_equiv.ys
@@ -0,0 +1,31 @@
+read_verilog mem_equiv.v
+read_verilog ../../picorv32.v
+rename main main_a
+chparam -set ENABLE_REGS_DUALPORT 0 \
+        -set TWO_STAGE_SHIFT      0 \
+	-set TWO_CYCLE_COMPARE    0 \
+	-set TWO_CYCLE_ALU        0 main_a
+hierarchy -top main_a
+proc
+opt
+memory -nordff -nomap
+flatten
+opt
+write_smt2 -bv -mem mem_equiv_a.smt2
+design -reset
+
+read_verilog mem_equiv.v
+read_verilog ../../picorv32.v
+rename main main_b
+chparam -set ENABLE_REGS_DUALPORT 1 \
+        -set TWO_STAGE_SHIFT      1 \
+	-set TWO_CYCLE_COMPARE    1 \
+	-set TWO_CYCLE_ALU        1 main_b
+hierarchy -top main_b
+proc
+opt
+memory -nordff -nomap
+flatten
+opt
+write_smt2 -bv -mem mem_equiv_b.smt2
+design -reset