From 8397962424388b755df18e368920d86f20391671 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 13 Aug 2015 11:52:53 +0200 Subject: Progress with smt2-based bmc scripts --- scripts/smt2-bmc/mem_equiv.py | 390 ++++++++++++++++++++++-------------------- scripts/smt2-bmc/mem_equiv.v | 1 + 2 files changed, 203 insertions(+), 188 deletions(-) (limited to 'scripts/smt2-bmc') diff --git a/scripts/smt2-bmc/mem_equiv.py b/scripts/smt2-bmc/mem_equiv.py index 2bb0538..02d90e2 100644 --- a/scripts/smt2-bmc/mem_equiv.py +++ b/scripts/smt2-bmc/mem_equiv.py @@ -1,6 +1,7 @@ #!/usr/bin/python3 import os, sys, getopt +from time import time import subprocess steps = 20 @@ -118,6 +119,7 @@ def yices_get_net_bin(mod_name, net_name, state_name): # Main Program ##################################### +start_time = time() yices_write("(set-logic QF_AUFBV)") with open("mem_equiv_a.smt2", "r") as f: @@ -126,195 +128,207 @@ with open("mem_equiv_a.smt2", "r") as f: 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) +for step in range(steps): + yices_write("(declare-fun a%d () main_a_s)" % step) + yices_write("(declare-fun b%d () main_b_s)" % step) + + # reset in first two cycles + if step < 2: + yices_write("(assert (not (|main_a_n resetn| a%d)))" % step) + yices_write("(assert (not (|main_b_n resetn| b%d)))" % step) + + else: + yices_write("(assert (|main_a_n resetn| a%d))" % step) + yices_write("(assert (|main_b_n resetn| b%d))" % step) + + if step == 0: + # 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)))") + 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)) -yices_write("(assert (|main_a_n trap| a%d))" % (steps-2)) -yices_write("(assert (|main_b_n trap| b%d))" % (steps-2)) - -# 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)) - -def make_cpu_regs(step): - for i in range(1, 32): - yices_write("(define-fun a%d_r%d () (_ BitVec 32) (select (|main_a_m cpu.cpuregs| a%d) #b%s))" % (step, i, step, bin(32+i)[3:])) - yices_write("(define-fun b%d_r%d () (_ BitVec 32) (select (|main_b_m cpu.cpuregs| b%d) #b%s))" % (step, i, step, bin(32+i)[3:])) - -make_cpu_regs(0) -make_cpu_regs(steps-1) - -print("checking...") -yices_write("(check-sat)") - -def print_status(mod, step): - resetn = yices_get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step)) - memvld = yices_get_net_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step)) - domem = yices_get_net_bool("main_" + mod, "domem", "%s%d" % (mod, step)) - memrdy = yices_get_net_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step)) - trap = yices_get_net_bool("main_" + mod, "trap", "%s%d" % (mod, step)) - print("status %5s: resetn=%s, memvld=%s, domem=%s, memrdy=%s, trap=%s" % ("%s[%d]" % (mod, step), resetn, memvld, domem, memrdy, trap)) - -def print_mem_xfer(mod, step): - if yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true': - mem_addr = yices_get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, step)) - mem_wdata = yices_get_net_hex("main_" + mod, "mem_wdata", "%s%d" % (mod, step)) - mem_wstrb = yices_get_net_bin("main_" + mod, "mem_wstrb", "%s%d" % (mod, step)) - mem_rdata = yices_get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, step)) - print("mem %5s: addr=%s, wdata=%s, wstrb=%s, rdata=%s" % ("%s[%d]" % (mod, step), mem_addr, mem_wdata, mem_wstrb, mem_rdata)) - -def print_cpu_regs(step): - for i in range(1, 32): - ra = yices_bv2hex(yices_get("a%d_r%d" % (step, i))) - rb = yices_bv2hex(yices_get("b%d_r%d" % (step, i))) - print("%3s[%d]: A=%s B=%s%s" % ("x%d" % i, step, ra, rb, " !" if ra != rb else "")) - -if yices_read() == "sat": - print("yices returned sat -> model check failed!") - - print() - print_cpu_regs(0) - - print() - print_cpu_regs(steps-1) - - 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) - - with open("mem_equiv_tb.v", "w") as f: - print() - print("writing verilog test bench...") - - memory_words = 1 - memory_datas = { "a": dict(), "b": dict() } - for i in range(steps-1, 0, -1): - for mod in ["a", "b"]: - if yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, i, mod, mod, i)) == 'true': - mem_addr = yices_get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, i)) - mem_rdata = yices_get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, i)) - memory_datas[mod][mem_addr] = mem_rdata - memory_words = max(int(mem_addr, 16)+1, memory_words) - memory_data = dict() - for k, v in memory_datas["a"].items(): memory_data[k] = v - for k, v in memory_datas["b"].items(): memory_data[k] = v - - print("`timescale 1 ns / 1 ps", file=f) - print("", file=f) - print("module testbench;", file=f) - print(" reg clk = 1, resetn, domem_a, domem_b;", file=f) - print(" always #5 clk = ~clk;", file=f) - print("", file=f) - print(" main #(", file=f) - print(" .MEMORY_WORDS(%d)," % memory_words, file=f) - print(" .ENABLE_REGS_DUALPORT(0),", file=f) - print(" .TWO_STAGE_SHIFT(0),", file=f) - print(" .TWO_CYCLE_COMPARE(0),", file=f) - print(" .TWO_CYCLE_ALU(0)", file=f) - print(" ) main_a (", file=f) - print(" .clk(clk),", file=f) - print(" .resetn(resetn),", file=f) - print(" .domem(domem_a)", file=f) - print(" );", file=f) - print("", file=f) - print(" main #(", file=f) - print(" .MEMORY_WORDS(%d)," % memory_words, file=f) - print(" .ENABLE_REGS_DUALPORT(1),", file=f) - print(" .TWO_STAGE_SHIFT(1),", file=f) - print(" .TWO_CYCLE_COMPARE(1),", file=f) - print(" .TWO_CYCLE_ALU(1)", file=f) - print(" ) main_b (", file=f) - print(" .clk(clk),", file=f) - print(" .resetn(resetn),", file=f) - print(" .domem(domem_b)", file=f) - print(" );", file=f) - print("", file=f) - print(" task check_reg;", file=f) - print(" input [4:0] n;", file=f) - print(" begin", file=f) - print(" if (main_a.cpu.cpuregs[n] != main_b.cpu.cpuregs[n])", file=f) - print(" $display(\"Divergent values for reg %1d: A=%08x B=%08x\", n, main_a.cpu.cpuregs[n], main_b.cpu.cpuregs[n]);", file=f) - print(" end", file=f) - print(" endtask", file=f) - print("", file=f) - print(" task check_mem;", file=f) - print(" input [31:0] n;", file=f) - print(" begin", file=f) - print(" if (main_a.memory[n] != main_b.memory[n])", file=f) - print(" $display(\"Divergent values for memory addr %08x: A=%08x B=%08x\", n, main_a.cpu.cpuregs[n], main_b.cpu.cpuregs[n]);", file=f) - print(" end", file=f) - print(" endtask", file=f) - print("", file=f) - print(" initial begin", file=f) - print(" $dumpfile(\"mem_equiv_tb.vcd\");", file=f) - print(" $dumpvars(0, testbench);", file=f) - print("", file=f) - - for i in range(1, 32): - ra = yices_bv2hex(yices_get("a%d_r%d" % (0, i))) - rb = yices_bv2hex(yices_get("b%d_r%d" % (0, i))) - print(" main_a.cpu.cpuregs[%2d] = 'h %s; main_b.cpu.cpuregs[%2d] = 'h %s;" % (i, ra, i, rb), file=f) - print("", file=f) - - for addr, data in memory_data.items(): - print(" main_a.memory['h %s] = 'h %s;" % (addr, data), file=f) - print(" main_b.memory['h %s] = 'h %s;" % (addr, data), file=f) - print("", file=f) - - for i in range(steps): - print(" resetn = %d;" % yices_get_net_bool("main_a", "resetn", "a%d" % i), file=f) - print(" domem_a = %d;" % yices_get_net_bool("main_a", "domem", "a%d" % i), file=f) - print(" domem_b = %d;" % yices_get_net_bool("main_b", "domem", "b%d" % i), file=f) - print(" @(posedge clk);", file=f) - print("", file=f) - - for i in range(1, 32): - print(" check_reg(%d);" % i, file=f) - for addr, data in memory_data.items(): - print(" check_mem('h %s);" % addr, file=f) - print("", file=f) - - print(" $finish;", file=f) - print(" end", file=f) - print("endmodule", file=f) - - print("running verilog test bench...") - os.system("iverilog -o mem_equiv_tb -s testbench mem_equiv_tb.v mem_equiv.v ../../picorv32.v && ./mem_equiv_tb") - -else: - print("yices returned unsat -> model check passed.") + yices_write("(assert (main_a_t a%d a%d))" % (step-1, step)) + yices_write("(assert (main_b_t b%d b%d))" % (step-1, step)) + + secs = int(time() - start_time) + print("[%3d:%02d:%02d] Checking sequence of length %d.." % (secs // (60*60), (secs // 60) % 60, secs % 60, step)) + yices_write("(push 1)") + + # stop with a trap and no pending memory xfer + yices_write("(assert (not (|main_a_n mem_valid| a%d)))" % step) + yices_write("(assert (not (|main_b_n mem_valid| b%d)))" % step) + yices_write("(assert (|main_a_n trap| a%d))" % step) + yices_write("(assert (|main_b_n trap| b%d))" % step) + + # 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))))") % (step, step, step, step)) + + yices_write("(check-sat)") + + if yices_read() == "sat": + + secs = int(time() - start_time) + print("[%3d:%02d:%02d] Creating model.." % (secs // (60*60), (secs // 60) % 60, secs % 60)) + + def make_cpu_regs(step): + for i in range(1, 32): + yices_write("(define-fun a%d_r%d () (_ BitVec 32) (select (|main_a_m cpu.cpuregs| a%d) #b%s))" % (step, i, step, bin(32+i)[3:])) + yices_write("(define-fun b%d_r%d () (_ BitVec 32) (select (|main_b_m cpu.cpuregs| b%d) #b%s))" % (step, i, step, bin(32+i)[3:])) + + make_cpu_regs(0) + make_cpu_regs(step) + + yices_write("(check-sat)") + + def print_status(mod, step): + resetn = yices_get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step)) + memvld = yices_get_net_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step)) + domem = yices_get_net_bool("main_" + mod, "domem", "%s%d" % (mod, step)) + memrdy = yices_get_net_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step)) + trap = yices_get_net_bool("main_" + mod, "trap", "%s%d" % (mod, step)) + print("status %5s: resetn=%s, memvld=%s, domem=%s, memrdy=%s, trap=%s" % ("%s[%d]" % (mod, step), resetn, memvld, domem, memrdy, trap)) + + def print_mem_xfer(mod, step): + if yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true': + mem_addr = yices_get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, step)) + mem_wdata = yices_get_net_hex("main_" + mod, "mem_wdata", "%s%d" % (mod, step)) + mem_wstrb = yices_get_net_bin("main_" + mod, "mem_wstrb", "%s%d" % (mod, step)) + mem_rdata = yices_get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, step)) + print("mem %5s: addr=%s, wdata=%s, wstrb=%s, rdata=%s" % ("%s[%d]" % (mod, step), mem_addr, mem_wdata, mem_wstrb, mem_rdata)) + + def print_cpu_regs(step): + for i in range(1, 32): + ra = yices_bv2hex(yices_get("a%d_r%d" % (step, i))) + rb = yices_bv2hex(yices_get("b%d_r%d" % (step, i))) + print("%3s[%d]: A=%s B=%s%s" % ("x%d" % i, step, ra, rb, " !" if ra != rb else "")) + + assert yices_read() == "sat" + + print() + print_cpu_regs(0) + + print() + print_cpu_regs(step) + + print() + for i in range(step+1): + print_status("a", i) + + print() + for i in range(step+1): + print_status("b", i) + + print() + for i in range(1, step+1): + print_mem_xfer("a", i) + + print() + for i in range(1, step+1): + print_mem_xfer("b", i) + + with open("mem_equiv_tb.v", "w") as f: + print() + print("writing verilog test bench...") + + memory_words = 1 + memory_datas = { "a": dict(), "b": dict() } + for i in range(step, 0, -1): + for mod in ["a", "b"]: + if yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, i, mod, mod, i)) == 'true': + mem_addr = yices_get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, i)) + mem_rdata = yices_get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, i)) + memory_datas[mod][mem_addr] = mem_rdata + memory_words = max(int(mem_addr, 16)+1, memory_words) + memory_data = dict() + for k, v in memory_datas["a"].items(): memory_data[k] = v + for k, v in memory_datas["b"].items(): memory_data[k] = v + + print("`timescale 1 ns / 1 ps", file=f) + print("", file=f) + print("module testbench;", file=f) + print(" reg clk = 1, resetn, domem_a, domem_b;", file=f) + print(" always #5 clk = ~clk;", file=f) + print("", file=f) + print(" main #(", file=f) + print(" .MEMORY_WORDS(%d)," % memory_words, file=f) + print(" .ENABLE_REGS_DUALPORT(0),", file=f) + print(" .TWO_STAGE_SHIFT(0),", file=f) + print(" .TWO_CYCLE_COMPARE(0),", file=f) + print(" .TWO_CYCLE_ALU(0)", file=f) + print(" ) main_a (", file=f) + print(" .clk(clk),", file=f) + print(" .resetn(resetn),", file=f) + print(" .domem(domem_a)", file=f) + print(" );", file=f) + print("", file=f) + print(" main #(", file=f) + print(" .MEMORY_WORDS(%d)," % memory_words, file=f) + print(" .ENABLE_REGS_DUALPORT(1),", file=f) + print(" .TWO_STAGE_SHIFT(1),", file=f) + print(" .TWO_CYCLE_COMPARE(1),", file=f) + print(" .TWO_CYCLE_ALU(1)", file=f) + print(" ) main_b (", file=f) + print(" .clk(clk),", file=f) + print(" .resetn(resetn),", file=f) + print(" .domem(domem_b)", file=f) + print(" );", file=f) + print("", file=f) + print(" task check_reg;", file=f) + print(" input [4:0] n;", file=f) + print(" begin", file=f) + print(" if (main_a.cpu.cpuregs[n] != main_b.cpu.cpuregs[n])", file=f) + print(" $display(\"Divergent values for reg %1d: A=%08x B=%08x\", n, main_a.cpu.cpuregs[n], main_b.cpu.cpuregs[n]);", file=f) + print(" end", file=f) + print(" endtask", file=f) + print("", file=f) + print(" task check_mem;", file=f) + print(" input [31:0] n;", file=f) + print(" begin", file=f) + print(" if (main_a.memory[n] != main_b.memory[n])", file=f) + print(" $display(\"Divergent values for memory addr %08x: A=%08x B=%08x\", n, main_a.cpu.cpuregs[n], main_b.cpu.cpuregs[n]);", file=f) + print(" end", file=f) + print(" endtask", file=f) + print("", file=f) + print(" initial begin", file=f) + print(" $dumpfile(\"mem_equiv_tb.vcd\");", file=f) + print(" $dumpvars(0, testbench);", file=f) + print("", file=f) + + for i in range(1, 32): + ra = yices_bv2hex(yices_get("a%d_r%d" % (0, i))) + rb = yices_bv2hex(yices_get("b%d_r%d" % (0, i))) + print(" main_a.cpu.cpuregs[%2d] = 'h %s; main_b.cpu.cpuregs[%2d] = 'h %s;" % (i, ra, i, rb), file=f) + print("", file=f) + + for addr, data in memory_data.items(): + print(" main_a.memory['h %s] = 'h %s;" % (addr, data), file=f) + print(" main_b.memory['h %s] = 'h %s;" % (addr, data), file=f) + print("", file=f) + + for i in range(step+1): + print(" resetn = %d;" % yices_get_net_bool("main_a", "resetn", "a%d" % i), file=f) + print(" domem_a = %d;" % yices_get_net_bool("main_a", "domem", "a%d" % i), file=f) + print(" domem_b = %d;" % yices_get_net_bool("main_b", "domem", "b%d" % i), file=f) + print(" @(posedge clk);", file=f) + print("", file=f) + + for i in range(1, 32): + print(" check_reg(%d);" % i, file=f) + for addr, data in memory_data.items(): + print(" check_mem('h %s);" % addr, file=f) + print("", file=f) + + print(" $finish;", file=f) + print(" end", file=f) + print("endmodule", file=f) + + secs = int(time() - start_time) + print("[%3d:%02d:%02d] Done." % (secs // (60*60), (secs // 60) % 60, secs % 60)) + break + + else: # unsat + yices_write("(pop 1)") yices_write("(exit)") yices.wait() diff --git a/scripts/smt2-bmc/mem_equiv.v b/scripts/smt2-bmc/mem_equiv.v index 6aba8f1..1904e06 100644 --- a/scripts/smt2-bmc/mem_equiv.v +++ b/scripts/smt2-bmc/mem_equiv.v @@ -15,6 +15,7 @@ module main (input clk, resetn, domem, output trap); (* keep *) wire [31:0] mem_rdata; picorv32 #( + .ENABLE_COUNTERS ( 0), .ENABLE_REGS_DUALPORT(ENABLE_REGS_DUALPORT), .TWO_STAGE_SHIFT (TWO_STAGE_SHIFT ), .TWO_CYCLE_COMPARE (TWO_CYCLE_COMPARE ), -- cgit