verilog/rtl/softshell/third_party/wb2axip/bench/mcy/easyaxil/config.mcy

[options]
size 1000
tags COVERED UNCOVERED NOCHANGE EQGAP FMONLY

[script]
read -sv easyaxil.v
prep -top easyaxil

[files]
easyaxil.v

[logic]
use_formal = True

tb_okay = (result("test_sim") == "PASS")
eq_okay = (result("test_eq") == "PASS")

if tb_okay and use_formal:
    tb_okay = (result("test_fm") == "PASS")
    if not tb_okay:
        tag("FMONLY")

if tb_okay and not eq_okay:
    tag("UNCOVERED")
elif not tb_okay and not eq_okay:
    tag("COVERED")
elif tb_okay and eq_okay:
    tag("NOCHANGE")
elif not tb_okay and eq_okay:
    tag("EQGAP")
else:
    assert 0

[report]
if tags("EQGAP"):
    print("Found %d mutations exposing a formal equivalence gap!" % tags("EQGAP"))
if tags("COVERED")+tags("UNCOVERED"):
    print("Coverage: %.2f%%" % (100.0*tags("COVERED")/(tags("COVERED")+tags("UNCOVERED"))))

[test test_sim]
maxbatchsize 10
expect PASS FAIL
run bash $PRJDIR/test_sim.sh

[test test_eq]
expect PASS FAIL
run bash $PRJDIR/test_eq.sh

[test test_fm]
expect PASS FAIL
run bash $PRJDIR/test_fm.sh