From ec19a48df0cd9c022eeab8f8626e459090578b14 Mon Sep 17 00:00:00 2001 From: Ivan Kosarev Date: Sat, 15 Oct 2022 19:29:20 +0100 Subject: [PATCH] [Sim][#50] Support randomosing the order nodes are getting updated in. --- tests/z80sim/z80sim.py | 36 +++++++++++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 3 deletions(-) diff --git a/tests/z80sim/z80sim.py b/tests/z80sim/z80sim.py index c9ab34d..1333e46 100755 --- a/tests/z80sim/z80sim.py +++ b/tests/z80sim/z80sim.py @@ -23,6 +23,7 @@ import pathlib import pprint import pysat.solvers +import random import sys import traceback import z3 @@ -75,6 +76,16 @@ TESTED_NODES.add(f'instr{i}') +def get_opt(id, type): + for a in sys.argv: + if a.startswith(id + '='): + return type(a.split('=', maxsplit=1)[1]) + return None + + +SEED = get_opt('--seed', int) + + def _ceil_div(a, b): return -(a // -b) @@ -1406,9 +1417,18 @@ def __update_group_of(self, n, more, updated): updated.add(n) - def __update_nodes(self, nodes): + def __update_nodes(self, nodes, *, shuffle=True): + # TODO: Does always updating all nodes lead to any failures? + # nodes = list(self.__nodes.values()) + + shuffle &= (SEED is not None) + nodes = list(nodes) + round = 0 while nodes: + if shuffle: + random.shuffle(nodes) + round += 1 assert round < 100, 'Loop encountered!' @@ -1718,7 +1738,8 @@ def update_pin(self, pin): def update_all_nodes(self): with Status.do('update nodes'): self.__update_nodes([n for n in self.__nodes.values() - if n not in self.__gnd_pwr]) + if n not in self.__gnd_pwr], + shuffle=False) def dump(self): with open('z80.dump', mode='w') as f: @@ -1785,7 +1806,7 @@ def __get_cache(steps): # Whenever we make changes that invalidate cached states, # e.g., the names of the nodes are changed, the version # number must be bumped. - VERSION = 8 + VERSION = 8, SEED key = VERSION, __class__.__get_steps_image(steps) return Cache.get_entry('states', key) @@ -2769,6 +2790,9 @@ def get_cond_as_expr(cond, phase, before): def execute_instr(s, id, phase, before): + if SEED is not None: + random.seed(SEED) + cycles = TestedInstrs.get_cycles(id, phase) for cycle_no, (d, ticks, cond) in enumerate(cycles): cond = get_cond_as_expr(cond, phase, before) @@ -2896,6 +2920,9 @@ def rev(bits): s = build_reset_state() if '--no-symbolising' not in sys.argv: + if SEED is not None: + random.seed(SEED) + with s.status('build symbolised state'): for id, cycles in SYMBOLISING_SEQ: with s.status(id): @@ -2904,6 +2931,8 @@ def rev(bits): s.set_db_and_wait(d, ticks) s.cache(intermediate=True) + ''' TODO: Symbolising the latch seems to cause failures + on shiffling (updating nodes in random order). with s.status('symbolise instruction latch'): instr = Bits('instr', width=8) is_prefix = ((instr == 0xcb) | (instr == 0xed) | @@ -2912,6 +2941,7 @@ def rev(bits): for i in range(8): s.set_latch_state(f'instr{i}', f'~instr{i}', instr[i]) + ''' s.cache() s.report('after-symbolising')