ppsfp finished

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

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']