Skip to content
Permalink
Browse files

script finds qualifiers needed for FPU automatically

  • Loading branch information
gokhankici committed Jun 19, 2019
1 parent 186e418 commit 7b5d00eb37bf31b9d1c4e69e176271244e86b26f
@@ -25,6 +25,151 @@
}
],
"qualifiers": [
{
"type": "pairs",
"variables": [
"div_opa_ldz_d",
"fpu_op_r2",
"m_u0_expa_00",
"m_u0_expa_ff",
"m_u0_expb_00",
"m_u0_expb_ff",
"m_u0_fracta_00",
"m_u0_fractb_00",
"m_u0_infa_f_r",
"m_u0_infb_f_r",
"m_u0_opa_nan",
"m_u0_opb_nan",
"m_u0_qnan_r_a",
"m_u0_qnan_r_b",
"m_u0_snan_r_a",
"m_u0_snan_r_b",
"m_u1_add_d",
"m_u1_add_r",
"m_u1_exp_dn_out",
"m_u1_foo_u1",
"m_u1_fracta_eq_fractb",
"m_u1_fracta_lt_fractb",
"m_u1_fracta_out",
"m_u1_fractb_out",
"m_u1_sign_d",
"m_u1_signa_r",
"m_u1_signb_r",
"m_u1_sticky",
"m_u2_exp_out",
"m_u2_exp_ovf",
"m_u2_inf",
"m_u2_rewrite_fracta",
"m_u2_rewrite_fractb",
"m_u2_sign_d",
"m_u2_sign_exe",
"m_u2_underflow",
"m_u5_prod1",
"m_u6_quo1",
"m_u6_remainder",
"opa_r1",
"opas_r1",
"rmode_r2"
]
},
{
"type": "pairs",
"variables": [
"div_opa_ldz_r1",
"exp_ovf_r",
"exp_r",
"fpu_op_r3",
"fract_i2f",
"fract_out_q",
"inf_mul2",
"inf_mul_r",
"m_u0_ind",
"m_u0_inf",
"m_u0_opa_00",
"m_u0_opa_dn",
"m_u0_opa_inf",
"m_u0_opb_00",
"m_u0_opb_dn",
"m_u0_opb_inf",
"m_u0_qnan",
"m_u0_snan",
"m_u1_exp_dn_out",
"m_u1_fasu_op",
"m_u1_foo_u1",
"m_u1_fracta_out",
"m_u1_fractb_out",
"m_u1_nan_sign",
"m_u1_result_zero_sign",
"m_u1_sign",
"m_u1_sign_d",
"m_u2_foo_u2",
"m_u2_sign",
"m_u5_prod",
"m_u6_quo",
"m_u6_quo1",
"m_u6_rem",
"m_u6_remainder",
"opa_nan_r",
"opas_r2",
"rmode_r3",
"sign",
"sign_exe_r",
"underflow_fmul_r"
]
},
{
"type": "pairs",
"variables": [
"fpu_op_r1",
"opa_r",
"opb_r",
"rmode_r1"
]
},
{
"type": "pairs",
"variables": [
"div_by_zero",
"div_opa_ldz_r2",
"exp_r",
"fasu_op_r1",
"fract_denorm",
"fract_i2f",
"fract_out_q",
"m_u1_sign",
"m_u2_foo_u2",
"m_u4_rewrite_f2i_out_sign",
"m_u6_quo",
"m_u6_rem",
"qnan",
"sign",
"sign_fasu_r",
"sign_mul_r",
"snan"
]
},
{
"type": "pairs",
"variables": [
"fract_denorm",
"m_u4_fi_ldz",
"qnan"
]
},
{
"type": "pairs",
"variables": [
"fasu_op_r2",
"fract_denorm",
"fract_i2f",
"m_u4_fi_ldz",
"m_u4_rewrite_f2i_out_sign",
"sign",
"sign_fasu_r"
]
}
],
"qualifiers-history": [
{
"type": "pairs",
"variables": [
@@ -24,12 +24,11 @@
{
"type": "always_eq",
"variables": [
"csr_mtime",
"csr_mtimecmp",
"de_branch_taken",
"de_illegal_csr_access",
"de_inst",
"interrupt",
"interrupt_check",
"b_wr0",
"b_wr1",
"b_wr2",
@@ -649,8 +649,11 @@ module yarvi( input wire clock
wb_csrd <= ex_csrd;
end

// rewrite
wire interrupt_check = csr_mtime == csr_mtimecmp;

always @(posedge clock) begin
if (csr_mtime == csr_mtimecmp) begin
if (interrupt_check) begin
$display("Times up!");
if (!csr_mie`MTIP)
$display(" but the interrupt currently disabled");
@@ -1,4 +1,4 @@
PY_FILES = annotation.py assumptions.py benchmark.py config.py run.py utils.py testing.py minimize.py
PY_FILES = $(wildcard *.py)
JQ_TYPES = always_eq initial_eq

lint:
@@ -7,6 +7,9 @@ lint:
$(JQ_TYPES): %:
cat annot-last.json | jq '.annotations | map(select(.type == "$@") | .variables) | add | sort'

pairs:
cat annot-last.json | jq '.qualifiers | map(select(.type == "pairs") | .variables) | .[]'

freeze:
pip freeze > requirements.txt

@@ -139,6 +139,11 @@ def go_qualif_vs(typ, qs):

return j

def set_pairs(self, pairs):
self.qualif_pairs.clear()
for p in pairs:
self.qualif_pairs.add(frozenset(p))

def __len__(self):
return len(self.qualif_implies) + len(self.qualif_iff) + \
len(self.qualif_pairs) + len(self.qualif_assume)
@@ -2,8 +2,7 @@
import os.path as p
import subprocess
import sys
from config import IODINE_SCRIPT, ABDUCTION_OUTPUT, DEBUG
import shutil
from config import BENCHMARK_DIR, IODINE_SCRIPT, DEBUG


class Benchmark(collections.namedtuple("Benchmark",
@@ -25,13 +24,47 @@ def run_iodine(self, extra_args=[], **kwargs):

def run_abduction(self):
""" Run Iodine but with the abduction feature """
rc = self.run_iodine(["--abduction"])
if rc == 0:
shutil.move(ABDUCTION_OUTPUT, p.basename(ABDUCTION_OUTPUT))
return rc
return self.run_iodine(["--abduction"])

def with_annot(self, annotfile):
def with_annotfile(self, annotfile):
""" Returns a new benchmark with the given annotation file """
return Benchmark(filename=self.filename,
module=self.module,
annotfile=annotfile)


# name, file and module of the benchmarks
CONFIG = [("ctalu",
"xcrypto-ref/rtl/coprocessor/scarv_cop_palu.v",
"scarv_cop_palu"),
("mips",
"472-mips-pipelined/mips_pipeline.v",
"mips_pipeline"),
("yarvi",
"yarvi/shared/yarvi.v",
"yarvi"),
("sha",
"crypto_cores/sha_core/trunk/rtl/sha256.v",
"sha256"),
("fpu",
"fpu/verilog/fpu.v",
"fpu"),
("fpu-div",
"fpu2/divider/divider.v",
"divider"),
("modexp",
"crypto_cores/RSA4096/ModExp2/ModExp.v",
"ModExp")]


def mk_bmk(filename, module):
full_filename = p.join(BENCHMARK_DIR, filename)
h, t = p.split(full_filename)
n, _ = p.splitext(t)
a = p.join(h, "annot-{}.json".format(n))
return Benchmark(filename=full_filename,
module=module,
annotfile=a)


BENCHMARKS = {n: mk_bmk(f, m) for n, f, m in CONFIG}
@@ -8,3 +8,4 @@
SCHEMA_FILE = p.join(PROJECT_ROOT, "annotation-schema.json")
IODINE_SCRIPT = p.join(PROJECT_ROOT, "iodine")
ABDUCTION_OUTPUT = p.join(PROJECT_ROOT, "cplex.json")
TMP_ANNOTFILE = "annot-last.json"
@@ -9,7 +9,7 @@


def go(b, af, getter, setter):
new_b = b.with_annot(TMP_FILE)
new_b = b.with_annotfile(TMP_FILE)
orig_vars = getter(af)
needed = orig_vars.copy()

0 comments on commit 7b5d00e

Please sign in to comment.
You can’t perform that action at this time.