From 301eebf289c7362dd123323f0b64a8802fe3ad47 Mon Sep 17 00:00:00 2001 From: stefan Date: Sat, 27 Jun 2026 14:35:15 +0900 Subject: [PATCH] ppsfp finished --- kyupy | 2 +- src/fsim/ppsfp.py | 67 ++++++++++++++++++++++++++++++++++++-- tests/all_kyupy_simprims.v | 53 ++++++++++++++++++++++++++++++ tests/test_safsim.py | 38 ++++++++++++++------- 4 files changed, 145 insertions(+), 15 deletions(-) create mode 100644 tests/all_kyupy_simprims.v diff --git a/kyupy b/kyupy index f5af7ec..7a69ce9 160000 --- a/kyupy +++ b/kyupy @@ -1 +1 @@ -Subproject commit f5af7ec3d9554c35f72ed42be6719f49438201c2 +Subproject commit 7a69ce901680164ad392a303f11b9f8067df5728 diff --git a/src/fsim/ppsfp.py b/src/fsim/ppsfp.py index 2336b80..8e19881 100644 --- a/src/fsim/ppsfp.py +++ b/src/fsim/ppsfp.py @@ -24,6 +24,58 @@ class SAFSimPPSFP: for il in n.ins.without_nones(): self.lines2ffr_stem[il.index] = stem + def _gate_sensitivity(self, node: Node, pin: int) -> np.ndarray: + """Patterns (as a packed bit-vector) for which `node`'s output is + sensitive to a change on input `pin` (the Boolean difference d_o/d_pin), + evaluated bit-parallel from the current signal values in ``self.sim.c``. + + For simple gates an input is sensitised iff all the other inputs hold + their non-controlling value: 1 for AND/NAND, 0 for OR/NOR. XOR/XNOR and + single-input gates (INV/BUF) are always sensitive. For the AND-OR/OR-AND + complex cells the condition follows from their structure; output + inversion (the AOI/OAI variants) does not change sensitivity. + """ + kind = node.kind + v = [self.sim.c[self.sim.c_locs[il.index]][0] for il in node.ins] + + if kind.startswith('AND') or kind.startswith('NAND'): + sens = np.full(self.sim.c.shape[2], 0xff, dtype=np.uint8) + for j, vj in enumerate(v): + if j != pin: sens &= vj + return sens + if kind.startswith('OR') or kind.startswith('NOR'): + sens = np.full(self.sim.c.shape[2], 0xff, dtype=np.uint8) + for j, vj in enumerate(v): + if j != pin: sens &= ~vj + return sens + if (kind.startswith('XOR') or kind.startswith('XNOR') + or kind.startswith('INV') or kind.startswith('BUF')): + return np.full(self.sim.c.shape[2], 0xff, dtype=np.uint8) + + shape = ''.join(ch for ch in kind if ch.isdigit()) + if kind.startswith('AO'): # AOxx / AOIxx, sum-of-products + if shape == '21': # (i0&i1) | i2 + return [v[1] & ~v[2], v[0] & ~v[2], ~(v[0] & v[1])][pin] + if shape == '22': # (i0&i1) | (i2&i3) + return [v[1] & ~(v[2] & v[3]), v[0] & ~(v[2] & v[3]), + v[3] & ~(v[0] & v[1]), v[2] & ~(v[0] & v[1])][pin] + if shape == '211': # (i0&i1) | i2 | i3 + return [v[1] & ~v[2] & ~v[3], v[0] & ~v[2] & ~v[3], + ~(v[0] & v[1]) & ~v[3], ~(v[0] & v[1]) & ~v[2]][pin] + if kind.startswith('OA'): # OAxx / OAIxx, product-of-sums + if shape == '21': # (i0|i1) & i2 + return [~v[1] & v[2], ~v[0] & v[2], v[0] | v[1]][pin] + if shape == '22': # (i0|i1) & (i2|i3) + return [~v[1] & (v[2] | v[3]), ~v[0] & (v[2] | v[3]), + ~v[3] & (v[0] | v[1]), ~v[2] & (v[0] | v[1])][pin] + if shape == '211': # (i0|i1) & i2 & i3 + return [~v[1] & v[2] & v[3], ~v[0] & v[2] & v[3], + (v[0] | v[1]) & v[3], (v[0] | v[1]) & v[2]][pin] + if kind.startswith('MUX'): # MUX21(i0,i1,i2) = i2 ? i1 : i0 + return [~v[2], v[2], v[0] ^ v[1]][pin] + + raise NotImplementedError(f'gate sensitivity for cell kind {kind!r}') + def classify_faults(self, faults: Collection[int], patterns: np.ndarray): with self.timers['startup']: @@ -62,7 +114,7 @@ class SAFSimPPSFP: self.sim.c_dirty[...] = 0 with self.timers['sim_ffr_prop']: self.sim.c_prop(fault_line=ffr_stem.ins[0].index, fault_model=2) - with self.timers['sim_ffr_obs']: + with self.timers['sim_ffr_out_reduce']: ffr_obs[ffr_idx] = np.bitwise_or.reduce(c_golden_poppo ^ self.sim.c[self.sim.poppo_c_locs], axis=0) & obs_mask with self.timers['sim_ffr_reset']: self.sim.c[...] = c_golden # clear fault @@ -70,8 +122,17 @@ class SAFSimPPSFP: ffr_obs[ffr_idx] = obs_mask ffr_obs_valid[ffr_idx] = 1 - # FIXME: compute observability of fault location at FFR stem - fault_to_stem_obs[...] = obs_mask + # observability of the fault site at the FFR stem by tracing + # the (unique, fan-out free) path from the site to the stem + # and requiring every gate along it to be sensitised. + with self.timers['sim_sens']: + fault_to_stem_obs[...] = obs_mask + line = self.sim.circuit.lines[fault_site] + while line.reader is not ffr_stem: + n = line.reader + if n.kind != '__fork__': # forks pass the value through + fault_to_stem_obs &= self._gate_sensitivity(n, line.reader_pin) + line = n.outs[0] # compute fault activation fault_act[...] = self.sim.c[self.sim.c_locs[fault_site]] & obs_mask diff --git a/tests/all_kyupy_simprims.v b/tests/all_kyupy_simprims.v new file mode 100644 index 0000000..3279512 --- /dev/null +++ b/tests/all_kyupy_simprims.v @@ -0,0 +1,53 @@ +module all_kyupy_primitives (i0, i1, i2, i3, o); + input i0; + input i1; + input i2; + input i3; + output [32:0] o; + + BUF1 buf1_0 (.i0(i0), .o(o[0])); + INV1 inv1_0 (.i0(i1), .o(o[1])); + + AND2 and2_0 (.i0(i0), .i1(i1), .o(o[2])); + AND3 and3_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[3])); + AND4 and4_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[4])); + + NAND2 nand2_0 (.i0(i0), .i1(i1), .o(o[5])); + NAND3 nand3_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[6])); + NAND4 nand4_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[7])); + + OR2 or2_0 (.i0(i0), .i1(i1), .o(o[8])); + OR3 or3_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[9])); + OR4 or4_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[10])); + + NOR2 nor2_0 (.i0(i0), .i1(i1), .o(o[11])); + NOR3 nor3_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[12])); + NOR4 nor4_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[13])); + + XOR2 xor2_0 (.i0(i0), .i1(i1), .o(o[14])); + XOR3 xor3_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[15])); + XOR4 xor4_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[16])); + + XNOR2 xnor2_0 (.i0(i0), .i1(i1), .o(o[17])); + XNOR3 xnor3_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[18])); + XNOR4 xnor4_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[19])); + + AO21 ao21_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[20])); + AO22 ao22_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[21])); + OA21 oa21_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[22])); + OA22 oa22_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[23])); + + AOI21 aoi21_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[24])); + AOI22 aoi22_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[25])); + OAI21 oai21_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[26])); + OAI22 oai22_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[27])); + + AO211 ao211_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[28])); + OA211 oa211_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[29])); + + AOI211 aoi211_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[30])); + OAI211 oai211_0 (.i0(i0), .i1(i1), .i2(i2), .i3(i3), .o(o[31])); + + MUX21 mux21_0 (.i0(i0), .i1(i1), .i2(i2), .o(o[32])); + +endmodule \ No newline at end of file diff --git a/tests/test_safsim.py b/tests/test_safsim.py index 0fda9c7..c1120bd 100644 --- a/tests/test_safsim.py +++ b/tests/test_safsim.py @@ -5,12 +5,11 @@ stuck-at-0 and polarity 1 is stuck-at-1. ``classify_faults`` returns a dict with the detected-by-simulation set under ``'DS'`` and the not-observed set under ``'NO'``. -The three simulators are exercised side-by-side: +The three simulators are exercised side-by-side and must agree exactly: * ``SAFSimSimple`` - brute force, exact. * ``SAFSimIncremental`` - incremental cone re-simulation, exact. - * ``SAFSimPPSFP`` - FFR-based, deliberately *optimistic*: its stem - observability is hard-wired to "always observable" (see the FIXME in - ``ppsfp.py``), so its DS set is a super-set of the exact DS set. + * ``SAFSimPPSFP`` - FFR-based: explicit simulation only at FFR stems, + with fault-to-stem observability from bit-parallel path sensitisation. """ import itertools @@ -18,7 +17,7 @@ import itertools import numpy as np import pytest -from kyupy import bench, logic +from kyupy import bench, verilog, logic from kyupy.techlib import KYUPY from fsim.static import FaultSet from fsim.simple import SAFSimSimple @@ -26,7 +25,7 @@ from fsim.incremental import SAFSimIncremental from fsim.ppsfp import SAFSimPPSFP -# The two exact simulators must always agree; PPSFP only over-approximates. +# All three simulators are exact and must classify every fault identically. ALL_ALGS = [SAFSimSimple, SAFSimIncremental, SAFSimPPSFP] @@ -178,16 +177,16 @@ def test_s27_exact_simulators_agree(s27_bench, s27_resolved): assert len(simple['NO']) == 1 -def test_s27_ppsfp_over_approximates(s27_bench, s27_resolved): +def test_s27_ppsfp_matches_exact(s27_bench, s27_resolved): faults, pat = _s27_setup(s27_bench, s27_resolved) exact = classify(SAFSimSimple, s27_resolved, faults, pat) ppsfp = classify(SAFSimPPSFP, s27_resolved, faults, pat) - # PPSFP's optimistic stem observability can only add detections, never drop. - assert exact['DS'] <= ppsfp['DS'] - # Here it reports the lone exact-NO fault as detected too. - assert ppsfp['DS'] == exact['DS'] | exact['NO'] + # With exact FFR-stem observability, PPSFP classifies identically to the + # brute-force simulator -- no longer an over-approximation. + assert ppsfp['DS'] == exact['DS'] + assert ppsfp['NO'] == exact['NO'] @pytest.mark.parametrize('alg', ALL_ALGS) @@ -201,3 +200,20 @@ def test_ppsfp_multibranch_stem_observability(alg): pat = make_patterns('1101--') r = classify(alg, c, [a_sa0], pat) assert r['DS'] == {a_sa0} + +@pytest.mark.parametrize('alg', [SAFSimIncremental, SAFSimPPSFP]) +def test_all_simprims(mydir, alg): + c = verilog.load(mydir / 'all_kyupy_simprims.v') + faults = [saf(line, polarity) for line in c.lines for polarity in (0, 1)] + s_nodes = c.s_nodes(KYUPY) + in_positions = [i for i, n in enumerate(s_nodes) if len(n.ins) == 0] + + for combo in itertools.product('01', repeat=len(in_positions)): + chars = ['-'] * len(s_nodes) + for pos, bit in zip(in_positions, combo): + chars[pos] = bit + pat = make_patterns(''.join(chars)) + ref = classify(SAFSimSimple, c, faults, pat) + res = classify(alg, c, faults, pat) + assert res['DS'] == ref['DS'] + assert res['NO'] == ref['NO'] \ No newline at end of file