Removed old scripts/smt2-bmc/
This commit is contained in:
Clifford Wolf
parent
54a8e4b311
commit
9c494af6e1
|
|
@ -1,12 +0,0 @@
|
||||||
__pycache__
|
|
||||||
debug.smt2
|
|
||||||
async_a.smt2
|
|
||||||
async_b.smt2
|
|
||||||
async_tb
|
|
||||||
async_tb.v
|
|
||||||
async_tb.vcd
|
|
||||||
sync_a.smt2
|
|
||||||
sync_b.smt2
|
|
||||||
sync_tb
|
|
||||||
sync_tb.v
|
|
||||||
sync_tb.vcd
|
|
||||||
|
|
@ -1,47 +0,0 @@
|
||||||
|
|
||||||
Checking equivalence of different configurations of PicoRV32 using Yosys and
|
|
||||||
SMT solvers (Yices, Z3, CVC4, MathSAT).
|
|
||||||
|
|
||||||
The PicoRV32 core provides configuration parameters that change the supported
|
|
||||||
ISA and/or the timing of the core. This set of scripts uses model checking
|
|
||||||
techniques to proof equivalence of cores in different configurations, thus
|
|
||||||
transfering the confidence in the cores gained by running test benches on a few
|
|
||||||
configurations to the rest of the configurations.
|
|
||||||
|
|
||||||
|
|
||||||
async
|
|
||||||
-----
|
|
||||||
|
|
||||||
The async test compares two cores with different timings (number of clock
|
|
||||||
cycles per operation), but same ISA. The SMT problem models the following
|
|
||||||
scenario:
|
|
||||||
|
|
||||||
The cores start out with identical memory and register file. In cycle 0 the
|
|
||||||
reset input is active, in all other cycles the reset input is inactive. The
|
|
||||||
trap output must by active in the last cycle for both cores. I.e. whatever
|
|
||||||
the program in memory does, it must terminate in a trap and it must do so
|
|
||||||
for both cores within the simulated number of clock cycles.
|
|
||||||
|
|
||||||
The script searches for a trace that ends in different memory content and/or
|
|
||||||
different register file content in the last cycle, i.e. a trace that exposes
|
|
||||||
divergent behavior in the two cores.
|
|
||||||
|
|
||||||
|
|
||||||
sync
|
|
||||||
----
|
|
||||||
|
|
||||||
The sync test compares two cores same timings but different ISA. The ISA of the
|
|
||||||
2nd code (main_b) must be a superset of the ISA of the first core (main_a), and
|
|
||||||
catching illegal instructions and illegal memory transfers must be enabled in
|
|
||||||
the first core. The SMT problem models the following scenario:
|
|
||||||
|
|
||||||
The cores start out with identical memory and register file. In cycle 0 the
|
|
||||||
reset input is active, in all other cycles the reset input is inactive. The
|
|
||||||
cores are run in parallel for a number of cycles with the first core not going
|
|
||||||
into the trap state. I.e. all traces are limited to the ISA supported by the
|
|
||||||
first core.
|
|
||||||
|
|
||||||
The script searches for a trace that ends in different memory content and/or
|
|
||||||
different register file content in the last cycle, i.e. a trace that exposes
|
|
||||||
divergent behavior in the two cores.
|
|
||||||
|
|
||||||
|
|
@ -1,333 +0,0 @@
|
||||||
#!/usr/bin/env python3
|
|
||||||
|
|
||||||
import os, sys, getopt
|
|
||||||
from smtio import smtio, smtopts
|
|
||||||
|
|
||||||
steps = 12
|
|
||||||
words = 0
|
|
||||||
allmem = False
|
|
||||||
fastmem = False
|
|
||||||
initzero = False
|
|
||||||
check_mem = True
|
|
||||||
check_regs = True
|
|
||||||
so = smtopts()
|
|
||||||
|
|
||||||
def usage():
|
|
||||||
print("""
|
|
||||||
python3 async.py [options]
|
|
||||||
|
|
||||||
-t <steps>
|
|
||||||
default: 12
|
|
||||||
""" + so.helpmsg())
|
|
||||||
sys.exit(1)
|
|
||||||
|
|
||||||
try:
|
|
||||||
opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:")
|
|
||||||
except:
|
|
||||||
usage()
|
|
||||||
|
|
||||||
for o, a in opts:
|
|
||||||
if o == "-t":
|
|
||||||
steps = int(a)
|
|
||||||
elif so.handle(o, a):
|
|
||||||
pass
|
|
||||||
else:
|
|
||||||
usage()
|
|
||||||
|
|
||||||
if len(args) > 0:
|
|
||||||
usage()
|
|
||||||
|
|
||||||
smt = smtio(opts=so)
|
|
||||||
|
|
||||||
print("Solver: %s" % so.solver)
|
|
||||||
smt.setup("QF_AUFBV", "PicoRV32 \"async.py\" BMC script, powered by Yosys")
|
|
||||||
|
|
||||||
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.." % (smt.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
|
|
||||||
|
|
||||||
if smt.check_sat() == "sat":
|
|
||||||
|
|
||||||
print("%s Creating model.." % smt.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)
|
|
||||||
|
|
||||||
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.check_sat() == "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))
|
|
||||||
if smt.check_sat() != "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))
|
|
||||||
assert smt.check_sat() == "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))
|
|
||||||
if smt.check_sat() != "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))
|
|
||||||
assert smt.check_sat() == "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 main.v ../../picorv32.v && ./async_tb")
|
|
||||||
|
|
||||||
break
|
|
||||||
|
|
||||||
else: # unsat
|
|
||||||
smt.write("(pop 1)")
|
|
||||||
|
|
||||||
print("%s Done." % smt.timestamp())
|
|
||||||
smt.write("(exit)")
|
|
||||||
smt.wait()
|
|
||||||
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
#!/bin/bash
|
|
||||||
set -ex
|
|
||||||
yosys -qv1 async.ys
|
|
||||||
time python3 async.py
|
|
||||||
|
|
@ -1,31 +0,0 @@
|
||||||
read_verilog main.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 main.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
|
|
||||||
|
|
@ -1,64 +0,0 @@
|
||||||
`timescale 1 ns / 1 ps
|
|
||||||
|
|
||||||
module main (input clk, resetn, domem, output trap);
|
|
||||||
parameter integer MEMORY_WORDS = 2**30;
|
|
||||||
|
|
||||||
// timing parameters (vary for async test)
|
|
||||||
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;
|
|
||||||
|
|
||||||
// isa parameters (vary for sync test)
|
|
||||||
parameter [0:0] ENABLE_COUNTERS = 0;
|
|
||||||
parameter [0:0] CATCH_MISALIGN = 1;
|
|
||||||
parameter [0:0] CATCH_ILLINSN = 1;
|
|
||||||
parameter [0:0] ENABLE_MUL = 0;
|
|
||||||
parameter [0:0] ENABLE_IRQ = 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 #(
|
|
||||||
// timing parameters
|
|
||||||
.ENABLE_REGS_DUALPORT(ENABLE_REGS_DUALPORT),
|
|
||||||
.TWO_STAGE_SHIFT (TWO_STAGE_SHIFT ),
|
|
||||||
.TWO_CYCLE_COMPARE (TWO_CYCLE_COMPARE ),
|
|
||||||
.TWO_CYCLE_ALU (TWO_CYCLE_ALU ),
|
|
||||||
|
|
||||||
// isa parameters
|
|
||||||
.ENABLE_COUNTERS(ENABLE_COUNTERS),
|
|
||||||
.CATCH_MISALIGN (CATCH_MISALIGN ),
|
|
||||||
.CATCH_ILLINSN (CATCH_ILLINSN ),
|
|
||||||
.ENABLE_MUL (ENABLE_MUL ),
|
|
||||||
.ENABLE_IRQ (ENABLE_IRQ )
|
|
||||||
) 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
|
|
||||||
|
|
@ -1,285 +0,0 @@
|
||||||
#!/usr/bin/env python3
|
|
||||||
|
|
||||||
import sys
|
|
||||||
import subprocess
|
|
||||||
from select import select
|
|
||||||
from time import time
|
|
||||||
|
|
||||||
class smtio:
|
|
||||||
def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
|
|
||||||
if opts is not None:
|
|
||||||
self.solver = opts.solver
|
|
||||||
self.debug_print = opts.debug_print
|
|
||||||
self.debug_file = opts.debug_file
|
|
||||||
self.timeinfo = opts.timeinfo
|
|
||||||
|
|
||||||
else:
|
|
||||||
self.solver = "yices"
|
|
||||||
self.debug_print = False
|
|
||||||
self.debug_file = None
|
|
||||||
self.timeinfo = True
|
|
||||||
|
|
||||||
if solver is not None:
|
|
||||||
self.solver = solver
|
|
||||||
|
|
||||||
if debug_print is not None:
|
|
||||||
self.debug_print = debug_print
|
|
||||||
|
|
||||||
if debug_file is not None:
|
|
||||||
self.debug_file = debug_file
|
|
||||||
|
|
||||||
if timeinfo is not None:
|
|
||||||
self.timeinfo = timeinfo
|
|
||||||
|
|
||||||
if self.solver == "yices":
|
|
||||||
popen_vargs = ['yices-smt2', '--incremental']
|
|
||||||
|
|
||||||
if self.solver == "z3":
|
|
||||||
popen_vargs = ['z3', '-smt2', '-in']
|
|
||||||
|
|
||||||
if self.solver == "cvc4":
|
|
||||||
popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
|
|
||||||
|
|
||||||
if self.solver == "mathsat":
|
|
||||||
popen_vargs = ['mathsat']
|
|
||||||
|
|
||||||
self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
|
|
||||||
self.start_time = time()
|
|
||||||
|
|
||||||
def setup(self, logic="ALL", info=None):
|
|
||||||
self.write("(set-logic %s)" % logic)
|
|
||||||
if info is not None:
|
|
||||||
self.write("(set-info :source |%s|)" % info)
|
|
||||||
self.write("(set-info :smt-lib-version 2.5)")
|
|
||||||
self.write("(set-info :category \"industrial\")")
|
|
||||||
|
|
||||||
def timestamp(self):
|
|
||||||
secs = int(time() - self.start_time)
|
|
||||||
return "+ %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
|
|
||||||
|
|
||||||
def write(self, stmt):
|
|
||||||
stmt = stmt.strip()
|
|
||||||
if self.debug_print:
|
|
||||||
print("> %s" % stmt)
|
|
||||||
if self.debug_file:
|
|
||||||
print(stmt, file=self.debug_file)
|
|
||||||
self.debug_file.flush()
|
|
||||||
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
|
|
||||||
self.p.stdin.flush()
|
|
||||||
|
|
||||||
def read(self):
|
|
||||||
stmt = []
|
|
||||||
count_brackets = 0
|
|
||||||
|
|
||||||
while True:
|
|
||||||
line = self.p.stdout.readline().decode("ascii").strip()
|
|
||||||
count_brackets += line.count("(")
|
|
||||||
count_brackets -= line.count(")")
|
|
||||||
stmt.append(line)
|
|
||||||
if self.debug_print:
|
|
||||||
print("< %s" % line)
|
|
||||||
if count_brackets == 0:
|
|
||||||
break
|
|
||||||
if not self.p.poll():
|
|
||||||
print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
|
|
||||||
sys.exit(1)
|
|
||||||
|
|
||||||
stmt = "".join(stmt)
|
|
||||||
if stmt.startswith("(error"):
|
|
||||||
print("SMT Solver Error: %s" % stmt, file=sys.stderr)
|
|
||||||
sys.exit(1)
|
|
||||||
|
|
||||||
return stmt
|
|
||||||
|
|
||||||
def check_sat(self):
|
|
||||||
if self.debug_print:
|
|
||||||
print("> (check-sat)")
|
|
||||||
if self.debug_file:
|
|
||||||
print("; running check-sat..", file=self.debug_file)
|
|
||||||
self.debug_file.flush()
|
|
||||||
|
|
||||||
self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
|
|
||||||
self.p.stdin.flush()
|
|
||||||
|
|
||||||
if self.timeinfo:
|
|
||||||
i = 0
|
|
||||||
s = "/-\|"
|
|
||||||
|
|
||||||
count = 0
|
|
||||||
num_bs = 0
|
|
||||||
while select([self.p.stdout], [], [], 0.1) == ([], [], []):
|
|
||||||
count += 1
|
|
||||||
|
|
||||||
if count < 25:
|
|
||||||
continue
|
|
||||||
|
|
||||||
if count % 10 == 0 or count == 25:
|
|
||||||
secs = count // 10
|
|
||||||
|
|
||||||
if secs < 60:
|
|
||||||
m = "(%d seconds)" % secs
|
|
||||||
elif secs < 60*60:
|
|
||||||
m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
|
|
||||||
else:
|
|
||||||
m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
|
|
||||||
|
|
||||||
print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
|
|
||||||
num_bs = len(m) + 3
|
|
||||||
|
|
||||||
else:
|
|
||||||
print("\b" + s[i], end="", file=sys.stderr)
|
|
||||||
|
|
||||||
sys.stderr.flush()
|
|
||||||
i = (i + 1) % len(s)
|
|
||||||
|
|
||||||
if num_bs != 0:
|
|
||||||
print("\b \b" * num_bs, end="", file=sys.stderr)
|
|
||||||
sys.stderr.flush()
|
|
||||||
|
|
||||||
result = self.read()
|
|
||||||
if self.debug_file:
|
|
||||||
print("(set-info :status %s)" % result, file=self.debug_file)
|
|
||||||
print("(check-sat)", file=self.debug_file)
|
|
||||||
self.debug_file.flush()
|
|
||||||
return result
|
|
||||||
|
|
||||||
def parse(self, 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 bv2hex(self, v):
|
|
||||||
if v == "true": return "1"
|
|
||||||
if v == "false": return "0"
|
|
||||||
h = ""
|
|
||||||
while len(v) > 2:
|
|
||||||
d = 0
|
|
||||||
if len(v) > 0 and v[-1] == "1": d += 1
|
|
||||||
if len(v) > 1 and v[-2] == "1": d += 2
|
|
||||||
if len(v) > 2 and v[-3] == "1": d += 4
|
|
||||||
if len(v) > 3 and v[-4] == "1": d += 8
|
|
||||||
h = hex(d)[2:] + h
|
|
||||||
if len(v) < 4: break
|
|
||||||
v = v[:-4]
|
|
||||||
return h
|
|
||||||
|
|
||||||
def bv2bin(self, v):
|
|
||||||
if v == "true": return "1"
|
|
||||||
if v == "false": return "0"
|
|
||||||
return v[2:]
|
|
||||||
|
|
||||||
def get(self, expr):
|
|
||||||
self.write("(get-value (%s))" % (expr))
|
|
||||||
return self.parse(self.read())[0][1]
|
|
||||||
|
|
||||||
def get_net(self, mod_name, net_name, state_name):
|
|
||||||
return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
|
|
||||||
|
|
||||||
def get_net_bool(self, mod_name, net_name, state_name):
|
|
||||||
v = self.get_net(mod_name, net_name, state_name)
|
|
||||||
assert v in ["true", "false"]
|
|
||||||
return 1 if v == "true" else 0
|
|
||||||
|
|
||||||
def get_net_hex(self, mod_name, net_name, state_name):
|
|
||||||
return self.bv2hex(self.get_net(mod_name, net_name, state_name))
|
|
||||||
|
|
||||||
def get_net_bin(self, mod_name, net_name, state_name):
|
|
||||||
return self.bv2bin(self.get_net(mod_name, net_name, state_name))
|
|
||||||
|
|
||||||
def wait(self):
|
|
||||||
self.p.wait()
|
|
||||||
|
|
||||||
|
|
||||||
class smtopts:
|
|
||||||
def __init__(self):
|
|
||||||
self.optstr = "s:d:vp"
|
|
||||||
self.solver = "yices"
|
|
||||||
self.debug_print = False
|
|
||||||
self.debug_file = None
|
|
||||||
self.timeinfo = True
|
|
||||||
|
|
||||||
def handle(self, o, a):
|
|
||||||
if o == "-s":
|
|
||||||
self.solver = a
|
|
||||||
elif o == "-v":
|
|
||||||
self.debug_print = True
|
|
||||||
elif o == "-p":
|
|
||||||
self.timeinfo = True
|
|
||||||
elif o == "-d":
|
|
||||||
self.debug_file = open(a, "w")
|
|
||||||
else:
|
|
||||||
return False
|
|
||||||
return True
|
|
||||||
|
|
||||||
def helpmsg(self):
|
|
||||||
return """
|
|
||||||
-s <solver>
|
|
||||||
set SMT solver: yices, z3, cvc4, mathsat
|
|
||||||
default: yices
|
|
||||||
|
|
||||||
-v
|
|
||||||
enable debug output
|
|
||||||
|
|
||||||
-p
|
|
||||||
disable timer display during solving
|
|
||||||
|
|
||||||
-d <filename>
|
|
||||||
write smt2 statements to file
|
|
||||||
"""
|
|
||||||
|
|
||||||
|
|
||||||
class mkvcd:
|
|
||||||
def __init__(self, f):
|
|
||||||
self.f = f
|
|
||||||
self.t = -1
|
|
||||||
self.nets = dict()
|
|
||||||
|
|
||||||
def add_net(self, name, width):
|
|
||||||
assert self.t == -1
|
|
||||||
key = "n%d" % len(self.nets)
|
|
||||||
self.nets[name] = (key, width)
|
|
||||||
|
|
||||||
def set_net(self, name, bits):
|
|
||||||
assert name in self.nets
|
|
||||||
assert self.t >= 0
|
|
||||||
print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
|
|
||||||
|
|
||||||
def set_time(self, t):
|
|
||||||
assert t >= self.t
|
|
||||||
if t != self.t:
|
|
||||||
if self.t == -1:
|
|
||||||
for name in sorted(self.nets):
|
|
||||||
key, width = self.nets[name]
|
|
||||||
print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
|
|
||||||
print("$enddefinitions $end", file=self.f)
|
|
||||||
self.t = t
|
|
||||||
assert self.t >= 0
|
|
||||||
print("#%d" % self.t, file=self.f)
|
|
||||||
|
|
||||||
|
|
@ -1,267 +0,0 @@
|
||||||
#!/usr/bin/env python3
|
|
||||||
|
|
||||||
import os, sys, getopt
|
|
||||||
from smtio import smtio, smtopts
|
|
||||||
|
|
||||||
steps = 14
|
|
||||||
words = 0
|
|
||||||
allmem = False
|
|
||||||
so = smtopts()
|
|
||||||
|
|
||||||
def usage():
|
|
||||||
print("""
|
|
||||||
python3 sync.py [options]
|
|
||||||
|
|
||||||
-t <steps>
|
|
||||||
default: 20
|
|
||||||
""" + so.helpmsg())
|
|
||||||
sys.exit(1)
|
|
||||||
|
|
||||||
try:
|
|
||||||
opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:")
|
|
||||||
except:
|
|
||||||
usage()
|
|
||||||
|
|
||||||
for o, a in opts:
|
|
||||||
if o == "-t":
|
|
||||||
steps = int(a)
|
|
||||||
elif so.handle(o, a):
|
|
||||||
pass
|
|
||||||
else:
|
|
||||||
usage()
|
|
||||||
|
|
||||||
if len(args) > 0:
|
|
||||||
usage()
|
|
||||||
|
|
||||||
smt = smtio(opts=so)
|
|
||||||
|
|
||||||
print("Solver: %s" % so.solver)
|
|
||||||
smt.setup("QF_AUFBV", "PicoRV32 \"sync.py\" BMC script, powered by Yosys")
|
|
||||||
|
|
||||||
regs_a = list()
|
|
||||||
regs_b = list()
|
|
||||||
|
|
||||||
with open("sync_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("sync_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)
|
|
||||||
|
|
||||||
smt.write("(assert (= (|main_a_n domem| a%d) (|main_b_n domem| b%d)))" % (step, step))
|
|
||||||
smt.write("(assert (not (|main_a_n trap| a%d)))" % step)
|
|
||||||
|
|
||||||
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.." % (smt.timestamp(), step))
|
|
||||||
smt.write("(push 1)")
|
|
||||||
|
|
||||||
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))" +
|
|
||||||
"(distinct (|main_a_n trap| a%d) (|main_b_n trap| b%d))))") % (step, step, step, step, step, step))
|
|
||||||
|
|
||||||
if smt.check_sat() == "sat":
|
|
||||||
|
|
||||||
print("%s Creating model.." % smt.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)
|
|
||||||
|
|
||||||
assert smt.sheck_sat() == "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 ""))
|
|
||||||
|
|
||||||
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("sync_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(" /* FIXME */", 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(" /* FIXME */", 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(\"sync_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 sync_tb -s testbench sync_tb.v main.v ../../picorv32.v && ./sync_tb")
|
|
||||||
|
|
||||||
break
|
|
||||||
|
|
||||||
else: # unsat
|
|
||||||
smt.write("(pop 1)")
|
|
||||||
|
|
||||||
smt.write("(assert (= (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)))" % (step, step))
|
|
||||||
smt.write("(assert (= (|main_a_m memory| a%d) (|main_b_m memory| b%d)))" % (step, step))
|
|
||||||
smt.write("(assert (= (|main_a_n trap| a%d) (|main_b_n trap| b%d)))" % (step, step))
|
|
||||||
|
|
||||||
print("%s Done." % smt.timestamp())
|
|
||||||
smt.write("(exit)")
|
|
||||||
smt.wait()
|
|
||||||
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
#!/bin/bash
|
|
||||||
set -ex
|
|
||||||
yosys -qv1 sync.ys
|
|
||||||
time python3 sync.py
|
|
||||||
|
|
@ -1,28 +0,0 @@
|
||||||
read_verilog main.v
|
|
||||||
read_verilog ../../picorv32.v
|
|
||||||
rename main main_a
|
|
||||||
hierarchy -top main_a
|
|
||||||
proc
|
|
||||||
opt
|
|
||||||
memory -nordff -nomap
|
|
||||||
flatten
|
|
||||||
opt
|
|
||||||
write_smt2 -bv -mem -regs sync_a.smt2
|
|
||||||
design -reset
|
|
||||||
|
|
||||||
read_verilog main.v
|
|
||||||
read_verilog ../../picorv32.v
|
|
||||||
rename main main_b
|
|
||||||
chparam -set ENABLE_COUNTERS 1 \
|
|
||||||
-set CATCH_MISALIGN 0 \
|
|
||||||
-set CATCH_ILLINSN 0 \
|
|
||||||
-set ENABLE_MUL 1 \
|
|
||||||
-set ENABLE_IRQ 0 main_b
|
|
||||||
hierarchy -top main_b
|
|
||||||
proc
|
|
||||||
opt
|
|
||||||
memory -nordff -nomap
|
|
||||||
flatten
|
|
||||||
opt
|
|
||||||
write_smt2 -bv -mem -regs sync_b.smt2
|
|
||||||
design -reset
|
|
||||||
Loading…
Reference in New Issue