partitioning for ppsfp

main.py

@@ -28,6 +28,9 @@ def main():
     parser.add_argument('circuit', help='Gate-level verilog, bench, or nix package to import. See available packages: "nix flake show github:s-holst/benchmark-circuits".')
     args = parser.parse_args()
 
+    if int(args.partitions) > 1:
+        assert args.algorithm == 'ppsfp', "partitioning is only supported for PPSFP."
+
     if not (circuit_path := Path(args.circuit)).exists(): # fallback to published nix package.
         nix_cmd = f"nix build github:s-holst/benchmark-circuits#{args.circuit} --print-out-paths --no-link"
         benchmark_path = Path(subprocess.check_output(nix_cmd.split(), text=True).strip())
@@ -73,6 +76,9 @@ def main():
     saf_collapsed = np.array(list(fs.saf_equiv_classes.keys()), dtype=np.uint32)
     rng.shuffle(saf_collapsed)
 
+    if int(args.partitions) > 1:
+        safsim = algorithms[args.algorithm](c_resolved, min(patterns.shape[1], 10240), partitions.partitions)
+    else:
         safsim = algorithms[args.algorithm](c_resolved, min(patterns.shape[1], 10240))
     log.info(f'{args.algorithm} {safsim.sim=}')
 

src/fsim/incremental.py

@@ -13,7 +13,8 @@ class SAFSimIncremental:
     After priming the circuit with a batch of patterns, faults are injected and only the gates in its fan-out cone are re-simulated.
     """
 
-    def __init__(self, circuit_resolved: Circuit, batch_size: int):
+    def __init__(self, circuit_resolved: Circuit, batch_size: int, partitioning: dict[int,set[int]]|None = None):
+        assert partitioning is None
         self.sim = LogicSim2V(circuit_resolved, sims=batch_size)
         self.timers = Timers()
 

src/fsim/ppsfp.py

@@ -1,9 +1,9 @@
-import time
+from collections import defaultdict
 from collections.abc import Collection
 
 import numpy as np
 
-from kyupy import log, batchrange, cdiv, Timers, logic
+from kyupy import log, batchrange, cdiv, Timers
 from kyupy.circuit import Circuit, Node
 from kyupy.logic_sim import LogicSim2V
 from kyupy.techlib import KYUPY
@@ -21,6 +21,10 @@ class LogicSim2VCone:
         self.c = base_sim.c.copy()
         self.c_dirty = np.full(self.c_len, 1, dtype=np.uint8)
         self._full_mask = base_sim._full_mask
+        self.poppo_c_locs = base_sim.poppo_c_locs
+
+    def c_from_base(self, base_sim):
+        self.c[...] = base_sim.c
 
     def c_prop(self, fault_line=-1, fault_model=2, fault_mask=None):
         if fault_mask is None:
@@ -33,22 +37,56 @@ class LogicSim2VCone:
         c_prop_2v_cpu(self.ops, self.c_locs, self.c, self.c_dirty, int(fault_line), fault_mask, int(fault_model))
 
 
+def compute_ffr_obs(sim: LogicSim2V|LogicSim2VCone, ffr_stems: Collection[Node], obs_mask, timers):
+    ffr_obs = []
+    c_golden = sim.c.copy()
+    c_golden_poppo = c_golden[sim.poppo_c_locs]
+
+    for ffr_stem in ffr_stems:
+        if len(ffr_stem.outs) > 1:
+            sim.c_dirty[...] = 0
+            with timers['sim_ffr_prop']:
+                sim.c_prop(fault_line=ffr_stem.ins[0].index, fault_model=2)
+            with timers['sim_ffr_out_reduce']:
+                ffr_obs.append(np.bitwise_or.reduce(c_golden_poppo ^ sim.c[sim.poppo_c_locs], axis=0)[0] & obs_mask)
+            with timers['sim_ffr_reset']:
+                sim.c[...] = c_golden # clear fault
+        else:  # primary output, completely observable
+            ffr_obs.append(obs_mask)
+    return np.stack(ffr_obs)
+
+
 class SAFSimPPSFP:
     """A stuck-at fault simulator that uses explicit simulations only at roots of fan-out free regions.
     """
 
-    def __init__(self, circuit_resolved: Circuit, batch_size: int):
+    def __init__(self, circuit_resolved: Circuit, batch_size: int, partitioning: dict[int,set[int]]|None = None):
+        self.partitioning = partitioning
         self.sim = LogicSim2V(circuit_resolved, sims=batch_size)
         self.timers = Timers()
 
         self.ffr_stem2idx = {}
         self.lines2ffr_stem: list[Node|None] = [None] * len(circuit_resolved.lines)
+        # origin line (the stem's driving line, where faults are injected in
+        # compute_ffr_obs) keyed by stem *node* index -- as stored in partitioning.
+        stem_idx2origin_line = {}
         for stem, nodes in circuit_resolved.fanout_free_regions(KYUPY):
             self.ffr_stem2idx[stem] = len(self.ffr_stem2idx)
+            if len(stem.ins) > 0:  # PI-fork stems have no driving line / no fault site
+                stem_idx2origin_line[stem.index] = stem.ins[0].index
             for n in nodes + [stem]:
                 for il in n.ins.without_nones():
                     self.lines2ffr_stem[il.index] = stem
 
+        self.sim_parts = {0: self.sim}
+        if self.partitioning is not None:
+            self.ffr_stem2part = {s: p for p, ss in self.partitioning.items() for s in ss}
+            if len(self.partitioning) > 1:
+                self.sim_parts = {
+                    p: LogicSim2VCone(self.sim, {stem_idx2origin_line[s] for s in stems
+                                                 if s in stem_idx2origin_line})
+                    for p, stems in self.partitioning.items()}
+
     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),
@@ -109,14 +147,20 @@ class SAFSimPPSFP:
             fclass_DS = set()
             nbatches = cdiv(patterns.shape[1], self.sim.sims)
             ffr_obs = np.zeros((len(self.ffr_stem2idx), self.sim.c.shape[2]), dtype=np.uint8)
-            obs_mask = np.packbits(np.full(patterns.shape[1], 1, dtype=np.uint8), bitorder='little')
+            obs_mask = np.zeros(self.sim.c.shape[2], dtype=np.uint8)
+            obs_mask_start = np.packbits(np.full(patterns.shape[1], 1, dtype=np.uint8), bitorder='little')
+            obs_mask[:len(obs_mask_start)] = obs_mask_start
             fault_to_stem_obs = obs_mask.copy()
             fault_act = obs_mask.copy()
-            # collect necessary stems
+            # collate all necessary stems into partitions
-            ffr_stems = set()
+            part2stems = defaultdict(set)
             for fault in faults:
                 fault_site = fault//2
-                ffr_stems.add(self.lines2ffr_stem[fault_site])
+                stem = self.lines2ffr_stem[fault_site]
+                assert stem is not None
+                part = 0 if self.partitioning is None else self.ffr_stem2part[stem.index]
+                part2stems[part].add(stem)
+
 
         with self.timers['sim'], log.progress() as p:
             for bidx, (bo, bs) in enumerate(batchrange(patterns.shape[1], self.sim.sims)):
@@ -125,24 +169,13 @@ class SAFSimPPSFP:
                 self.sim.c_dirty[...] = 1
                 with self.timers['sim_full_prop']:
                     self.sim.c_prop()
-                c_golden[...] = self.sim.c
-                c_golden_poppo = c_golden[self.sim.poppo_c_locs]
 
-                # compute all necessary FFR observability vectors in ffr_obs
+                for part, ffr_stems in part2stems.items():
-                n_stems = len(ffr_stems)
+                    ffr_idxs = [self.ffr_stem2idx[stem] for stem in ffr_stems]
-                for stem_progress, ffr_stem in enumerate(ffr_stems):
+                    sim = self.sim_parts[part]
-                    ffr_idx = self.ffr_stem2idx[ffr_stem]
+                    if isinstance(sim, LogicSim2VCone):
-                    if len(ffr_stem.outs) > 1:
+                        sim.c_from_base(self.sim)
-                        self.sim.c_dirty[...] = 0
+                    ffr_obs[ffr_idxs] = compute_ffr_obs(sim, ffr_stems, obs_mask, self.timers)
-                        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_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
-                    else:  # primary output, completely observable
-                        ffr_obs[ffr_idx] = obs_mask
-                    p.update(((stem_progress+1) / n_stems) * ((bidx+1) / nbatches))
 
                 for fault in faults:
                     fault_site = fault//2

src/fsim/simple.py

@@ -13,7 +13,8 @@ class SAFSimSimple:
     Simplest brute-force simulation of all given stuck-at faults.
     """
 
-    def __init__(self, circuit_resolved: Circuit, batch_size: int):
+    def __init__(self, circuit_resolved: Circuit, batch_size: int, partitioning: dict[int,set[int]]|None = None):
+        assert partitioning is None
         self.sim = LogicSim2V(circuit_resolved, sims=batch_size)
         self.timers = Timers()
 

src/fsim/static.py

@@ -237,18 +237,18 @@ class CircuitPartition:
 
     def __init__(self, c_resolved: Circuit, k: int = 1):
         line2fo_node = np.full(len(c_resolved.lines), -1, dtype=np.int32)
-        fo_nodes = []
+        self.fo_nodes = []
         for fo_node, region_nodes in c_resolved.fanout_free_regions(KYUPY):
-            fo_nodes.append(fo_node)
+            self.fo_nodes.append(fo_node)
             for n in [fo_node] + region_nodes:
                 for il in n.ins.without_nones():
                     line2fo_node[il] = fo_node
 
-        log.info(f'FFR count: {len(fo_nodes)}')
+        log.info(f'FFR count: {len(self.fo_nodes)}')
 
         predecessors = defaultdict(set)
         successors = defaultdict(set)
-        for fo_node in fo_nodes:
+        for fo_node in self.fo_nodes:
             if len(fo_node.outs) > 1:
                 for ol in fo_node.outs.without_nones():
                     assert line2fo_node[ol] >= 0, f'unknown {ol}'
@@ -256,22 +256,23 @@ class CircuitPartition:
                     successors[fo_node.index].add(int(line2fo_node[ol]))
 
         ancestors = dict()
-        for fo_node in fo_nodes:
+        for fo_node in self.fo_nodes:
             collect_ancestors(fo_node.index, predecessors, ancestors)
 
-        reachable = dict()
+        self.reachable = dict()
-        for fo_node in fo_nodes:
+        for fo_node in self.fo_nodes:
-            collect_reachable(fo_node.index, successors, reachable)
+            collect_reachable(fo_node.index, successors, self.reachable)
 
         if k <= 1:
-            return {0: {n.index for n in fo_nodes}}
+            self.partitions = {0: {n.index for n in self.fo_nodes}}
+            return
 
-        stem2hnode = {s.index: i for i, s in enumerate(fo_nodes)}
+        stem2hnode = {s.index: i for i, s in enumerate(self.fo_nodes)}
 
-        num_hnodes = len(fo_nodes)
+        num_hnodes = len(self.fo_nodes)
-        hnode_weights = [len(reachable[n.index]) for n in fo_nodes]
+        hnode_weights = [len(self.reachable[n.index]) for n in self.fo_nodes]
 
-        num_hnets = len(fo_nodes)
+        num_hnets = len(self.fo_nodes)
         hnets = [[] for _ in range(num_hnodes)]
         for stem, anc in ancestors.items():
             hnets[stem2hnode[stem]] = sorted(stem2hnode[n] for n in anc)
@@ -292,7 +293,7 @@ class CircuitPartition:
         context.loadINIconfiguration("km1_kKaHyPar_sea20.ini")
 
         context.setK(k)
-        context.setEpsilon(0.1)
+        context.setEpsilon(0.05)
 
         log.info('Partitioning...')
 
@@ -302,9 +303,7 @@ class CircuitPartition:
 
         self.partitions = defaultdict(set)
         for n in hypergraph.nodes():
-            self.partitions[hypergraph.blockID(n)].add(fo_nodes[n].index)
+            self.partitions[hypergraph.blockID(n)].add(self.fo_nodes[n].index)
-        self.fo_nodes = fo_nodes
-        self.reachable = reachable
 
 
     def print_stats(self):

tests/test_safsim.py

@@ -13,6 +13,7 @@ The three simulators are exercised side-by-side and must agree exactly:
 """
 
 import itertools
+from collections import defaultdict
 
 import numpy as np
 import pytest
@@ -41,9 +42,8 @@ def make_patterns(*specs):
     return pat if pat.ndim == 2 else pat.reshape(-1, 1)
 
 
-def classify(alg, circuit, faults, patterns):
+def classify(alg, circuit, faults, patterns, partitioning = None):
-    # PPSFP requires the batch size to match the pattern count (as main.py does).
+    sim = alg(circuit, batch_size=patterns.shape[1], partitioning=partitioning)
-    sim = alg(circuit, patterns.shape[1])
     return sim.classify_faults(list(faults), patterns)
 
 
@@ -167,24 +167,36 @@ def test_s27_exact_simulators_agree(s27_bench, s27_resolved):
     assert len(faults) == 32  # collapsed fault count, see test_fault_set.test_s27
 
     simple = classify(SAFSimSimple, s27_resolved, faults, pat)
-    incr = classify(SAFSimIncremental, s27_resolved, faults, pat)
 
-    # The two exact simulators must classify every fault identically.
-    assert simple['DS'] == incr['DS']
-    assert simple['NO'] == incr['NO']
     # This deterministic pattern set leaves exactly 6 faults unobserved.
     assert len(simple['DS']) == 26
     assert len(simple['NO']) == 6
 
+    incr = classify(SAFSimIncremental, s27_resolved, faults, pat)
+    ppsfp = classify(SAFSimPPSFP, s27_resolved, faults, pat)
 
-def test_s27_ppsfp_matches_exact(s27_bench, s27_resolved):
+    assert simple['DS'] == incr['DS']
+    assert simple['NO'] == incr['NO']
+    assert simple['DS'] == ppsfp['DS']
+    assert simple['NO'] == ppsfp['NO']
+
+
+def test_s27_ppsfp_partitioning(s27_bench, s27_resolved):
     faults, pat = _s27_setup(s27_bench, s27_resolved)
 
+    stems = [stem.index for stem, _ in s27_resolved.fanout_free_regions(KYUPY)]
+    k = 4
+    rng = np.random.default_rng(1)
+    parts = rng.integers(0, k, size=len(stems))
+    partitioning = defaultdict(set)
+    for part, stem in zip(parts, stems):
+        partitioning[int(part)].add(stem)
+
+    print(partitioning)
+
     exact = classify(SAFSimSimple, s27_resolved, faults, pat)
-    ppsfp = classify(SAFSimPPSFP, s27_resolved, faults, pat)
+    ppsfp = classify(SAFSimPPSFP, s27_resolved, faults, pat, partitioning)
 
-    # 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']