import os
import shutil
import time, datetime
import tabulate

times = []
tests = [
    "test0", "test1", "test2", "test3", "test4", "test5", "test6", "test7", "test8", "test9"
]

dut_dir1 = "proofs_lsu_taskBMC30_ni_lsu"
mod_dir1 = "proofs_lsu_taskBMC30_ni_model_lsu"
dut_dir2 = "proofs_lsu_taskBMC40_ni_lsu"
mod_dir2 = "proofs_lsu_taskBMC40_ni_model_lsu"

for (i, test) in enumerate(tests):
    print("Running test: " + test)
    shutil.copyfile(f"{os.getcwd()}/{test}/cva6_lsu_formal.v", f"{os.getcwd()}/cva6_lsu_formal.v")
    
    # Test with design
    pretime = time.time()
    if i < 8:
        os.system("time sby -f proofs_lsu.sby taskBMC30_ni_lsu")
    else:
        os.system("time sby -f proofs_lsu.sby taskBMC40_ni_lsu")
    posttime = time.time()
    dut_time = posttime - pretime
    print(f"For test: {test} DUT time: {dut_time}")

    # Save the results
    if i < 8:
        os.system(f"cp -r {dut_dir1} {test}/")
    else:
        os.system(f"cp -r {dut_dir2} {test}/")

    # Test on model
    pretime = time.time()
    if i < 8:
        os.system("time sby -f proofs_lsu.sby taskBMC30_ni_model_lsu")
    else:
        os.system("time sby -f proofs_lsu.sby taskBMC40_ni_model_lsu")

    posttime = time.time()
    model_time = posttime - pretime
    print(f"For test: {test} Model time: {model_time}")

    # Save the results
    if i < 8:
        os.system(f"cp -r {mod_dir1} {test}/")
    else:
        os.system(f"cp -r {mod_dir2} {test}/")

    # Save the times
    times.append([
        test, dut_time, model_time
    ])



with open("times.log", 'w') as f:
    f.write("// Generated by run_all.py at {}\n\n\n".format(datetime.datetime.now()))

    table = tabulate.tabulate(times, headers=["Test", "DUT Time", "Model Time"])
    f.write(table)