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