From ec0891326aee1334bce4bb096e7521a3907d4bdc Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 15 Aug 2015 10:50:27 +0200 Subject: Renamed scripts/smt2-bmc/mem_equiv to .../async --- scripts/smt2-bmc/.gitignore | 10 +- scripts/smt2-bmc/async.py | 323 ++++++++++++++++++++++++++++++++++++++++++ scripts/smt2-bmc/async.sh | 4 + scripts/smt2-bmc/async.v | 48 +++++++ scripts/smt2-bmc/async.ys | 31 ++++ scripts/smt2-bmc/mem_equiv.py | 323 ------------------------------------------ scripts/smt2-bmc/mem_equiv.sh | 4 - scripts/smt2-bmc/mem_equiv.v | 48 ------- scripts/smt2-bmc/mem_equiv.ys | 31 ---- 9 files changed, 411 insertions(+), 411 deletions(-) create mode 100644 scripts/smt2-bmc/async.py create mode 100644 scripts/smt2-bmc/async.sh create mode 100644 scripts/smt2-bmc/async.v create mode 100644 scripts/smt2-bmc/async.ys delete mode 100644 scripts/smt2-bmc/mem_equiv.py delete mode 100644 scripts/smt2-bmc/mem_equiv.sh delete mode 100644 scripts/smt2-bmc/mem_equiv.v delete mode 100644 scripts/smt2-bmc/mem_equiv.ys (limited to 'scripts/smt2-bmc') diff --git a/scripts/smt2-bmc/.gitignore b/scripts/smt2-bmc/.gitignore index 460c1c5..40f0c37 100644 --- a/scripts/smt2-bmc/.gitignore +++ b/scripts/smt2-bmc/.gitignore @@ -1,6 +1,6 @@ debug.smt2 -mem_equiv_a.smt2 -mem_equiv_b.smt2 -mem_equiv_tb -mem_equiv_tb.v -mem_equiv_tb.vcd +async_a.smt2 +async_b.smt2 +async_tb +async_tb.v +async_tb.vcd diff --git a/scripts/smt2-bmc/async.py b/scripts/smt2-bmc/async.py new file mode 100644 index 0000000..76edeb6 --- /dev/null +++ b/scripts/smt2-bmc/async.py @@ -0,0 +1,323 @@ +#!/usr/bin/python3 + +import os, sys, getopt +from time import time +from smtio import smtio + +steps = 12 +words = 0 +solver = "yices" +allmem = False +fastmem = False +initzero = False +check_mem = True +check_regs = True +debug_print = False +debug_file = open("debug.smt2", "w") + +start_time = time() +smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file) + +def timestamp(): + secs = int(time() - start_time) + return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) + +smt.write("(set-logic QF_AUFBV)") + +regs_a = list() +regs_b = list() + +with open("async_a.smt2", "r") as f: + for line in f: + if line.startswith("; yosys-smt2-register "): + line = line.split() + regs_a.append((line[2], int(line[3]))) + else: + smt.write(line) + +with open("async_b.smt2", "r") as f: + for line in f: + if line.startswith("; yosys-smt2-register "): + line = line.split() + regs_b.append((line[2], int(line[3]))) + else: + smt.write(line) + +for step in range(steps): + smt.write("(declare-fun a%d () main_a_s)" % step) + smt.write("(declare-fun b%d () main_b_s)" % step) + + if fastmem: + smt.write("(assert (|main_a_n domem| a%d))" % step) + smt.write("(assert (|main_b_n domem| b%d))" % step) + + if words > 0: + if allmem: + smt.write("(assert (bvult (|main_a_n mem_addr| a%d) #x%08x))" % (step, words)) + smt.write("(assert (bvult (|main_b_n mem_addr| b%d) #x%08x))" % (step, words)) + else: + smt.write("(assert (or (not (|main_a_n mem_valid| a%d)) (bvult (|main_a_n mem_addr| a%d) #x%08x)))" % (step, step, words)) + smt.write("(assert (or (not (|main_b_n mem_valid| b%d)) (bvult (|main_b_n mem_addr| b%d) #x%08x)))" % (step, step, words)) + + if step == 0: + # start with synced memory and register file + smt.write("(assert (= (|main_a_m cpu.cpuregs| a0) (|main_b_m cpu.cpuregs| b0)))") + smt.write("(assert (= (|main_a_m memory| a0) (|main_b_m memory| b0)))") + + # reset in first cycle + smt.write("(assert (not (|main_a_n resetn| a%d)))" % step) + smt.write("(assert (not (|main_b_n resetn| b%d)))" % step) + + else: + smt.write("(assert (main_a_t a%d a%d))" % (step-1, step)) + smt.write("(assert (main_b_t b%d b%d))" % (step-1, step)) + + smt.write("(assert (|main_a_n resetn| a%d))" % step) + smt.write("(assert (|main_b_n resetn| b%d))" % step) + + print("%s Checking sequence of length %d.." % (timestamp(), step)) + smt.write("(push 1)") + + # stop with a trap and no pending memory xfer + smt.write("(assert (not (|main_a_n mem_valid| a%d)))" % step) + smt.write("(assert (not (|main_b_n mem_valid| b%d)))" % step) + smt.write("(assert (|main_a_n trap| a%d))" % step) + smt.write("(assert (|main_b_n trap| b%d))" % step) + + # look for differences in memory and/or register file + if check_mem and check_regs: + smt.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)) + elif check_mem: + smt.write(("(assert (distinct (|main_a_m memory| a%d) (|main_b_m memory| b%d)))") % (step, step)) + elif check_regs: + smt.write(("(assert (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)))") % (step, step)) + else: + assert False + + smt.write("(check-sat)") + + if smt.read() == "sat": + + print("%s Creating model.." % timestamp()) + + def make_cpu_regs(step): + for i in range(1, 32): + smt.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:])) + smt.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) + + smt.write("(check-sat)") + + def print_status(mod, step): + resetn = smt.get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step)) + memvld = smt.get_net_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step)) + domem = smt.get_net_bool("main_" + mod, "domem", "%s%d" % (mod, step)) + memrdy = smt.get_net_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step)) + trap = smt.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 allmem or smt.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 = smt.get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, step)) + mem_wdata = smt.get_net_hex("main_" + mod, "mem_wdata", "%s%d" % (mod, step)) + mem_wstrb = smt.get_net_bin("main_" + mod, "mem_wstrb", "%s%d" % (mod, step)) + mem_rdata = smt.get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, step)) + if allmem and smt.get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true': + print("mem %5s: addr=%s, wdata=%s, wstrb=%s, rdata=%s <-" % ("%s[%d]" % (mod, step), mem_addr, mem_wdata, mem_wstrb, mem_rdata)) + else: + 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 = smt.bv2hex(smt.get("a%d_r%d" % (step, i))) + rb = smt.bv2hex(smt.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 smt.read() == "sat" + + if initzero: + for rn, rs in regs_a: + force_to_zero = True + if smt.get_net_bin("main_a", rn, "a0").count("1") != 0: + print("Looking for a solution with |main_a_n %s| initialized to all zeros.." % rn) + smt.write("(push 1)") + if rs == 1: + smt.write("(assert (not (|main_a_n %s| a0)))" % rn) + else: + smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs)) + smt.write("(check-sat)") + if smt.read() != "sat": + force_to_zero = False + smt.write("(pop 1)") + if force_to_zero: + if rs == 1: + smt.write("(assert (not (|main_a_n %s| a0)))" % rn) + else: + smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs)) + smt.write("(check-sat)") + assert smt.read() == "sat" + for rn, rs in regs_b: + force_to_zero = True + if smt.get_net_bin("main_b", rn, "b0").count("1") != 0: + print("Looking for a solution with |main_b_n %s| initialized to all zeros.." % rn) + smt.write("(push 1)") + if rs == 1: + smt.write("(assert (not (|main_b_n %s| b0)))" % rn) + else: + smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs)) + smt.write("(check-sat)") + if smt.read() != "sat": + force_to_zero = False + smt.write("(pop 1)") + if force_to_zero: + if rs == 1: + smt.write("(assert (not (|main_b_n %s| b0)))" % rn) + else: + smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs)) + smt.write("(check-sat)") + assert smt.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("async_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 allmem or smt.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 = smt.get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, i)) + mem_rdata = smt.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) >> 2)+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(\"async_tb.vcd\");", file=f) + print(" $dumpvars(0, testbench);", file=f) + print("", file=f) + + for rn, rs in regs_a: + print(" main_a.%s = %d'b %s;" % (rn, rs, smt.get_net_bin("main_a", rn, "a0")), file=f) + print("", file=f) + + for rn, rs in regs_b: + print(" main_b.%s = %d'b %s;" % (rn, rs, smt.get_net_bin("main_b", rn, "b0")), file=f) + print("", file=f) + + for i in range(1, 32): + ra = smt.bv2hex(smt.get("a%d_r%d" % (0, i))) + rb = smt.bv2hex(smt.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 %08x] = 'h %s;" % (int(addr, 16) >> 2, data), file=f) + print(" main_b.memory['h %08x] = 'h %s;" % (int(addr, 16) >> 2, data), file=f) + print("", file=f) + + for i in range(step+1): + print(" resetn = %d;" % smt.get_net_bool("main_a", "resetn", "a%d" % i), file=f) + print(" domem_a = %d;" % smt.get_net_bool("main_a", "domem", "a%d" % i), file=f) + print(" domem_b = %d;" % smt.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(" @(posedge clk);", file=f) + print(" @(posedge clk);", file=f) + print(" $finish;", file=f) + print(" end", file=f) + print("endmodule", file=f) + + if words > 0: + print("running verilog test bench...") + os.system("iverilog -o async_tb -s testbench async_tb.v async.v ../../picorv32.v && ./async_tb") + + break + + else: # unsat + smt.write("(pop 1)") + +print("%s Done." % timestamp()) +smt.write("(exit)") +smt.wait() + diff --git a/scripts/smt2-bmc/async.sh b/scripts/smt2-bmc/async.sh new file mode 100644 index 0000000..2149c05 --- /dev/null +++ b/scripts/smt2-bmc/async.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -ex +yosys -qv1 async.ys +time python3 async.py diff --git a/scripts/smt2-bmc/async.v b/scripts/smt2-bmc/async.v new file mode 100644 index 0000000..1904e06 --- /dev/null +++ b/scripts/smt2-bmc/async.v @@ -0,0 +1,48 @@ +`timescale 1 ns / 1 ps + +module main (input clk, resetn, domem, output trap); + parameter integer MEMORY_WORDS = 2**30; + 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_COUNTERS ( 0), + .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:MEMORY_WORDS-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/async.ys b/scripts/smt2-bmc/async.ys new file mode 100644 index 0000000..1f7c8f8 --- /dev/null +++ b/scripts/smt2-bmc/async.ys @@ -0,0 +1,31 @@ +read_verilog async.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 -regs async_a.smt2 +design -reset + +read_verilog async.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 -regs async_b.smt2 +design -reset diff --git a/scripts/smt2-bmc/mem_equiv.py b/scripts/smt2-bmc/mem_equiv.py deleted file mode 100644 index 10f50c7..0000000 --- a/scripts/smt2-bmc/mem_equiv.py +++ /dev/null @@ -1,323 +0,0 @@ -#!/usr/bin/python3 - -import os, sys, getopt -from time import time -from smtio import smtio - -steps = 15 -words = 0 -solver = "yices" -allmem = False -fastmem = False -initzero = False -check_mem = True -check_regs = True -debug_print = False -debug_file = open("debug.smt2", "w") - -start_time = time() -smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file) - -def timestamp(): - secs = int(time() - start_time) - return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) - -smt.write("(set-logic QF_AUFBV)") - -regs_a = list() -regs_b = list() - -with open("mem_equiv_a.smt2", "r") as f: - for line in f: - if line.startswith("; yosys-smt2-register "): - line = line.split() - regs_a.append((line[2], int(line[3]))) - else: - smt.write(line) - -with open("mem_equiv_b.smt2", "r") as f: - for line in f: - if line.startswith("; yosys-smt2-register "): - line = line.split() - regs_b.append((line[2], int(line[3]))) - else: - smt.write(line) - -for step in range(steps): - smt.write("(declare-fun a%d () main_a_s)" % step) - smt.write("(declare-fun b%d () main_b_s)" % step) - - if fastmem: - smt.write("(assert (|main_a_n domem| a%d))" % step) - smt.write("(assert (|main_b_n domem| b%d))" % step) - - if words > 0: - if allmem: - smt.write("(assert (bvult (|main_a_n mem_addr| a%d) #x%08x))" % (step, words)) - smt.write("(assert (bvult (|main_b_n mem_addr| b%d) #x%08x))" % (step, words)) - else: - smt.write("(assert (or (not (|main_a_n mem_valid| a%d)) (bvult (|main_a_n mem_addr| a%d) #x%08x)))" % (step, step, words)) - smt.write("(assert (or (not (|main_b_n mem_valid| b%d)) (bvult (|main_b_n mem_addr| b%d) #x%08x)))" % (step, step, words)) - - if step == 0: - # start with synced memory and register file - smt.write("(assert (= (|main_a_m cpu.cpuregs| a0) (|main_b_m cpu.cpuregs| b0)))") - smt.write("(assert (= (|main_a_m memory| a0) (|main_b_m memory| b0)))") - - # reset in first cycle - smt.write("(assert (not (|main_a_n resetn| a%d)))" % step) - smt.write("(assert (not (|main_b_n resetn| b%d)))" % step) - - else: - smt.write("(assert (main_a_t a%d a%d))" % (step-1, step)) - smt.write("(assert (main_b_t b%d b%d))" % (step-1, step)) - - smt.write("(assert (|main_a_n resetn| a%d))" % step) - smt.write("(assert (|main_b_n resetn| b%d))" % step) - - print("%s Checking sequence of length %d.." % (timestamp(), step)) - smt.write("(push 1)") - - # stop with a trap and no pending memory xfer - smt.write("(assert (not (|main_a_n mem_valid| a%d)))" % step) - smt.write("(assert (not (|main_b_n mem_valid| b%d)))" % step) - smt.write("(assert (|main_a_n trap| a%d))" % step) - smt.write("(assert (|main_b_n trap| b%d))" % step) - - # look for differences in memory and/or register file - if check_mem and check_regs: - smt.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)) - elif check_mem: - smt.write(("(assert (distinct (|main_a_m memory| a%d) (|main_b_m memory| b%d)))") % (step, step)) - elif check_regs: - smt.write(("(assert (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)))") % (step, step)) - else: - assert False - - smt.write("(check-sat)") - - if smt.read() == "sat": - - print("%s Creating model.." % timestamp()) - - def make_cpu_regs(step): - for i in range(1, 32): - smt.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:])) - smt.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) - - smt.write("(check-sat)") - - def print_status(mod, step): - resetn = smt.get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step)) - memvld = smt.get_net_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step)) - domem = smt.get_net_bool("main_" + mod, "domem", "%s%d" % (mod, step)) - memrdy = smt.get_net_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step)) - trap = smt.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 allmem or smt.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 = smt.get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, step)) - mem_wdata = smt.get_net_hex("main_" + mod, "mem_wdata", "%s%d" % (mod, step)) - mem_wstrb = smt.get_net_bin("main_" + mod, "mem_wstrb", "%s%d" % (mod, step)) - mem_rdata = smt.get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, step)) - if allmem and smt.get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true': - print("mem %5s: addr=%s, wdata=%s, wstrb=%s, rdata=%s <-" % ("%s[%d]" % (mod, step), mem_addr, mem_wdata, mem_wstrb, mem_rdata)) - else: - 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 = smt.bv2hex(smt.get("a%d_r%d" % (step, i))) - rb = smt.bv2hex(smt.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 smt.read() == "sat" - - if initzero: - for rn, rs in regs_a: - force_to_zero = True - if smt.get_net_bin("main_a", rn, "a0").count("1") != 0: - print("Looking for a solution with |main_a_n %s| initialized to all zeros.." % rn) - smt.write("(push 1)") - if rs == 1: - smt.write("(assert (not (|main_a_n %s| a0)))" % rn) - else: - smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - if smt.read() != "sat": - force_to_zero = False - smt.write("(pop 1)") - if force_to_zero: - if rs == 1: - smt.write("(assert (not (|main_a_n %s| a0)))" % rn) - else: - smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - assert smt.read() == "sat" - for rn, rs in regs_b: - force_to_zero = True - if smt.get_net_bin("main_b", rn, "b0").count("1") != 0: - print("Looking for a solution with |main_b_n %s| initialized to all zeros.." % rn) - smt.write("(push 1)") - if rs == 1: - smt.write("(assert (not (|main_b_n %s| b0)))" % rn) - else: - smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - if smt.read() != "sat": - force_to_zero = False - smt.write("(pop 1)") - if force_to_zero: - if rs == 1: - smt.write("(assert (not (|main_b_n %s| b0)))" % rn) - else: - smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - assert smt.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 allmem or smt.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 = smt.get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, i)) - mem_rdata = smt.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) >> 2)+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 rn, rs in regs_a: - print(" main_a.%s = %d'b %s;" % (rn, rs, smt.get_net_bin("main_a", rn, "a0")), file=f) - print("", file=f) - - for rn, rs in regs_b: - print(" main_b.%s = %d'b %s;" % (rn, rs, smt.get_net_bin("main_b", rn, "b0")), file=f) - print("", file=f) - - for i in range(1, 32): - ra = smt.bv2hex(smt.get("a%d_r%d" % (0, i))) - rb = smt.bv2hex(smt.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 %08x] = 'h %s;" % (int(addr, 16) >> 2, data), file=f) - print(" main_b.memory['h %08x] = 'h %s;" % (int(addr, 16) >> 2, data), file=f) - print("", file=f) - - for i in range(step+1): - print(" resetn = %d;" % smt.get_net_bool("main_a", "resetn", "a%d" % i), file=f) - print(" domem_a = %d;" % smt.get_net_bool("main_a", "domem", "a%d" % i), file=f) - print(" domem_b = %d;" % smt.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(" @(posedge clk);", file=f) - print(" @(posedge clk);", file=f) - print(" $finish;", file=f) - print(" end", file=f) - print("endmodule", file=f) - - if words > 0: - 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") - - break - - else: # unsat - smt.write("(pop 1)") - -print("%s Done." % timestamp()) -smt.write("(exit)") -smt.wait() - diff --git a/scripts/smt2-bmc/mem_equiv.sh b/scripts/smt2-bmc/mem_equiv.sh deleted file mode 100644 index ce9486d..0000000 --- a/scripts/smt2-bmc/mem_equiv.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/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 deleted file mode 100644 index 1904e06..0000000 --- a/scripts/smt2-bmc/mem_equiv.v +++ /dev/null @@ -1,48 +0,0 @@ -`timescale 1 ns / 1 ps - -module main (input clk, resetn, domem, output trap); - parameter integer MEMORY_WORDS = 2**30; - 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_COUNTERS ( 0), - .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:MEMORY_WORDS-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 deleted file mode 100644 index 67b49de..0000000 --- a/scripts/smt2-bmc/mem_equiv.ys +++ /dev/null @@ -1,31 +0,0 @@ -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 -regs 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 -regs mem_equiv_b.smt2 -design -reset -- cgit