Skip to content

Commit

Permalink
experiments: use zero init and yices for FPGA
Browse files Browse the repository at this point in the history
  • Loading branch information
ekiwi committed Jan 17, 2024
1 parent 004f0b6 commit 1a7575e
Showing 1 changed file with 13 additions and 2 deletions.
15 changes: 13 additions & 2 deletions scripts/run_rtl_repair_experiment.py
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,15 @@
# global experiment default settings
_solver = 'bitwuzla'
_incremental = True
_init = 'random' # the incremental solver always uses random init
_init = 'random'
_timeout = 60 # one minute timeout
_verbose_synth = True

# the FPGA benchmarks all have testbenches from Verilator which assume a zero init
_init_fpga = 'zero'
# the FPGA benchmarks benefit from running with yices2
_solver_fpga = 'yices2'

@dataclass
class ExpConfig:
incremental: bool
Expand Down Expand Up @@ -161,8 +166,14 @@ def run_all_cirfix_benchmarks(conf: Config, projects: dict) -> dict:
continue
sys.stdout.write(f"{bb.name} w/ {testbench.name}")
sys.stdout.flush()
if exp_conf.fpga_instead_of_cirfix_bench:
init = _init_fpga
solver = _solver_fpga
else:
init = _init
solver = _solver
status, changes, template = run_rtl_repair(conf.working_dir, bb, project_toml, bb.bug.name,
testbench=testbench.name, solver=_solver, init=_init,
testbench=testbench.name, solver=solver, init=init,
incremental=exp_conf.incremental,
timeout=exp_conf.timeout,
all_templates=exp_conf.all_templates,
Expand Down

0 comments on commit 1a7575e

Please sign in to comment.