From 9c494af6e1bc4f89e7842085d266fb386d923729 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 3 Dec 2016 12:28:36 +0100 Subject: Removed old scripts/smt2-bmc/ --- scripts/smt2-bmc/.gitignore | 12 -- scripts/smt2-bmc/README | 47 ------- scripts/smt2-bmc/async.py | 333 -------------------------------------------- scripts/smt2-bmc/async.sh | 4 - scripts/smt2-bmc/async.ys | 31 ----- scripts/smt2-bmc/main.v | 64 --------- scripts/smt2-bmc/smtio.py | 285 ------------------------------------- scripts/smt2-bmc/sync.py | 267 ----------------------------------- scripts/smt2-bmc/sync.sh | 4 - scripts/smt2-bmc/sync.ys | 28 ---- 10 files changed, 1075 deletions(-) delete mode 100644 scripts/smt2-bmc/.gitignore delete mode 100644 scripts/smt2-bmc/README delete mode 100644 scripts/smt2-bmc/async.py delete mode 100644 scripts/smt2-bmc/async.sh delete mode 100644 scripts/smt2-bmc/async.ys delete mode 100644 scripts/smt2-bmc/main.v delete mode 100644 scripts/smt2-bmc/smtio.py delete mode 100644 scripts/smt2-bmc/sync.py delete mode 100644 scripts/smt2-bmc/sync.sh delete mode 100644 scripts/smt2-bmc/sync.ys (limited to 'scripts') diff --git a/scripts/smt2-bmc/.gitignore b/scripts/smt2-bmc/.gitignore deleted file mode 100644 index 919b4a2..0000000 --- a/scripts/smt2-bmc/.gitignore +++ /dev/null @@ -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 diff --git a/scripts/smt2-bmc/README b/scripts/smt2-bmc/README deleted file mode 100644 index f947664..0000000 --- a/scripts/smt2-bmc/README +++ /dev/null @@ -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. - diff --git a/scripts/smt2-bmc/async.py b/scripts/smt2-bmc/async.py deleted file mode 100644 index e4854de..0000000 --- a/scripts/smt2-bmc/async.py +++ /dev/null @@ -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 - 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() - diff --git a/scripts/smt2-bmc/async.sh b/scripts/smt2-bmc/async.sh deleted file mode 100644 index 2149c05..0000000 --- a/scripts/smt2-bmc/async.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash -set -ex -yosys -qv1 async.ys -time python3 async.py diff --git a/scripts/smt2-bmc/async.ys b/scripts/smt2-bmc/async.ys deleted file mode 100644 index 627d717..0000000 --- a/scripts/smt2-bmc/async.ys +++ /dev/null @@ -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 diff --git a/scripts/smt2-bmc/main.v b/scripts/smt2-bmc/main.v deleted file mode 100644 index db854bc..0000000 --- a/scripts/smt2-bmc/main.v +++ /dev/null @@ -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 diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py deleted file mode 100644 index df14dee..0000000 --- a/scripts/smt2-bmc/smtio.py +++ /dev/null @@ -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 - set SMT solver: yices, z3, cvc4, mathsat - default: yices - - -v - enable debug output - - -p - disable timer display during solving - - -d - 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) - diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py deleted file mode 100644 index e73ee99..0000000 --- a/scripts/smt2-bmc/sync.py +++ /dev/null @@ -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 - 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() - diff --git a/scripts/smt2-bmc/sync.sh b/scripts/smt2-bmc/sync.sh deleted file mode 100644 index 9c8b6b6..0000000 --- a/scripts/smt2-bmc/sync.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash -set -ex -yosys -qv1 sync.ys -time python3 sync.py diff --git a/scripts/smt2-bmc/sync.ys b/scripts/smt2-bmc/sync.ys deleted file mode 100644 index ea190b7..0000000 --- a/scripts/smt2-bmc/sync.ys +++ /dev/null @@ -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 -- cgit