Renamed scripts/smt2-bmc/mem_equiv to .../async

6 files changed, 19 insertions, 19 deletions

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/mem_equiv.py b/scripts/smt2-bmc/async.py
index 10f50c7..76edeb6 100644
--- a/scripts/smt2-bmc/mem_equiv.py
+++ b/scripts/smt2-bmc/async.py
@@ -4,7 +4,7 @@ import os, sys, getopt
 from time import time
 from smtio import smtio
 
-steps = 15
+steps = 12
 words = 0
 solver = "yices"
 allmem = False
@@ -27,7 +27,7 @@ smt.write("(set-logic QF_AUFBV)")
 regs_a = list()
 regs_b = list()
 
-with open("mem_equiv_a.smt2", "r") as f:
+with open("async_a.smt2", "r") as f:
     for line in f:
         if line.startswith("; yosys-smt2-register "):
             line = line.split()
@@ -35,7 +35,7 @@ with open("mem_equiv_a.smt2", "r") as f:
         else:
             smt.write(line)
 
-with open("mem_equiv_b.smt2", "r") as f:
+with open("async_b.smt2", "r") as f:
     for line in f:
         if line.startswith("; yosys-smt2-register "):
             line = line.split()
@@ -202,7 +202,7 @@ for step in range(steps):
             for i in range(1, step+1):
                 print_mem_xfer("b", i)
 
-            with open("mem_equiv_tb.v", "w") as f:
+            with open("async_tb.v", "w") as f:
                 print()
                 print("writing verilog test bench...")
 
@@ -266,7 +266,7 @@ for step in range(steps):
                 print("    endtask", file=f)
                 print("", file=f)
                 print("    initial begin", file=f)
-                print("        $dumpfile(\"mem_equiv_tb.vcd\");", file=f)
+                print("        $dumpfile(\"async_tb.vcd\");", file=f)
                 print("        $dumpvars(0, testbench);", file=f)
                 print("", file=f)
 
@@ -310,7 +310,7 @@ for step in range(steps):
 
             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")
+                os.system("iverilog -o async_tb -s testbench async_tb.v async.v ../../picorv32.v && ./async_tb")
 
             break
 
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/mem_equiv.v b/scripts/smt2-bmc/async.v
index 1904e06..1904e06 100644
--- a/scripts/smt2-bmc/mem_equiv.v
+++ b/scripts/smt2-bmc/async.v
diff --git a/scripts/smt2-bmc/mem_equiv.ys b/scripts/smt2-bmc/async.ys
index 67b49de..1f7c8f8 100644
--- a/scripts/smt2-bmc/mem_equiv.ys
+++ b/scripts/smt2-bmc/async.ys
@@ -1,4 +1,4 @@
-read_verilog mem_equiv.v
+read_verilog async.v
 read_verilog ../../picorv32.v
 rename main main_a
 chparam -set ENABLE_REGS_DUALPORT 0 \
@@ -11,10 +11,10 @@ opt
 memory -nordff -nomap
 flatten
 opt
-write_smt2 -bv -mem -regs mem_equiv_a.smt2
+write_smt2 -bv -mem -regs async_a.smt2
 design -reset
 
-read_verilog mem_equiv.v
+read_verilog async.v
 read_verilog ../../picorv32.v
 rename main main_b
 chparam -set ENABLE_REGS_DUALPORT 1 \
@@ -27,5 +27,5 @@ opt
 memory -nordff -nomap
 flatten
 opt
-write_smt2 -bv -mem -regs mem_equiv_b.smt2
+write_smt2 -bv -mem -regs async_b.smt2
 design -reset
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