Compare commits
No commits in common. '301eebf289c7362dd123323f0b64a8802fe3ad47' and 'e8348f26c055ebc2b85a67f85afbd94df2594723' have entirely different histories.
301eebf289
...
e8348f26c0
5 changed files with 3 additions and 425 deletions
@ -1 +1 @@ |
|||||||
Subproject commit 7a69ce901680164ad392a303f11b9f8067df5728 |
Subproject commit f5af7ec3d9554c35f72ed42be6719f49438201c2 |
||||||
@ -1,146 +0,0 @@ |
|||||||
import time |
|
||||||
from collections.abc import Collection |
|
||||||
|
|
||||||
import numpy as np |
|
||||||
|
|
||||||
from kyupy import log, batchrange, cdiv, Timers, logic |
|
||||||
from kyupy.circuit import Circuit, Node |
|
||||||
from kyupy.logic_sim import LogicSim2V |
|
||||||
from kyupy.techlib import KYUPY |
|
||||||
|
|
||||||
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): |
|
||||||
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) |
|
||||||
for stem, nodes in circuit_resolved.fanout_free_regions(KYUPY): |
|
||||||
self.ffr_stem2idx[stem] = len(self.ffr_stem2idx) |
|
||||||
for n in nodes + [stem]: |
|
||||||
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']: |
|
||||||
self.sim.c_prop() # trigger jit |
|
||||||
c_golden = np.zeros_like(self.sim.c) |
|
||||||
fclass_DS = set() |
|
||||||
nbatches = cdiv(patterns.shape[1], self.sim.sims) |
|
||||||
nfaults = len(faults) |
|
||||||
ffr_obs = np.zeros((len(self.ffr_stem2idx), self.sim.c.shape[2]), dtype=np.uint8) |
|
||||||
ffr_obs_valid = np.zeros(len(self.ffr_stem2idx), dtype=np.uint8) |
|
||||||
obs_mask = np.packbits(np.full(patterns.shape[1], 1, dtype=np.uint8), bitorder='little') |
|
||||||
fault_to_stem_obs = obs_mask.copy() |
|
||||||
fault_act = obs_mask.copy() |
|
||||||
|
|
||||||
with self.timers['sim'], log.progress() as p: |
|
||||||
for bidx, (bo, bs) in enumerate(batchrange(patterns.shape[1], self.sim.sims)): |
|
||||||
self.sim.s_assign[:, :bs] = patterns[:, bo:bo+bs] |
|
||||||
self.sim.s_to_c() |
|
||||||
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] |
|
||||||
ffr_obs_valid[...] = 0 |
|
||||||
|
|
||||||
for fidx, fault in enumerate(faults): |
|
||||||
fault_site = fault//2 |
|
||||||
fault_polarity = fault&1 |
|
||||||
ffr_stem = self.lines2ffr_stem[fault_site] |
|
||||||
assert ffr_stem is not None |
|
||||||
ffr_idx = self.ffr_stem2idx[ffr_stem] |
|
||||||
|
|
||||||
# compute FFR observability vector ffr_obs[ffr_idx] if necessary |
|
||||||
if not ffr_obs_valid[ffr_idx]: |
|
||||||
if len(ffr_stem.outs) > 1: |
|
||||||
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_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 |
|
||||||
ffr_obs_valid[ffr_idx] = 1 |
|
||||||
|
|
||||||
# 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 |
|
||||||
if fault_polarity: # stuck-at 1? |
|
||||||
fault_act ^= obs_mask # activated iff signal is 0 |
|
||||||
|
|
||||||
if np.bitwise_or.reduce(ffr_obs[ffr_idx] & fault_to_stem_obs & fault_act) != 0: |
|
||||||
fclass_DS.add(fault) |
|
||||||
p.update(((fidx+1) / nfaults) * ((bidx+1) / nbatches)) |
|
||||||
|
|
||||||
return {'DS': fclass_DS, 'NO': set(faults) - fclass_DS} |
|
||||||
@ -1,53 +0,0 @@ |
|||||||
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 |
|
||||||
@ -1,219 +0,0 @@ |
|||||||
"""Unit tests for the stuck-at fault simulators (the SAF* classes). |
|
||||||
|
|
||||||
Each fault is identified by ``line.index * 2 + polarity`` where polarity 0 is |
|
||||||
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 and must agree exactly: |
|
||||||
* ``SAFSimSimple`` - brute force, exact. |
|
||||||
* ``SAFSimIncremental`` - incremental cone re-simulation, exact. |
|
||||||
* ``SAFSimPPSFP`` - FFR-based: explicit simulation only at FFR stems, |
|
||||||
with fault-to-stem observability from bit-parallel path sensitisation. |
|
||||||
""" |
|
||||||
|
|
||||||
import itertools |
|
||||||
|
|
||||||
import numpy as np |
|
||||||
import pytest |
|
||||||
|
|
||||||
from kyupy import bench, verilog, logic |
|
||||||
from kyupy.techlib import KYUPY |
|
||||||
from fsim.static import FaultSet |
|
||||||
from fsim.simple import SAFSimSimple |
|
||||||
from fsim.incremental import SAFSimIncremental |
|
||||||
from fsim.ppsfp import SAFSimPPSFP |
|
||||||
|
|
||||||
|
|
||||||
# All three simulators are exact and must classify every fault identically. |
|
||||||
ALL_ALGS = [SAFSimSimple, SAFSimIncremental, SAFSimPPSFP] |
|
||||||
|
|
||||||
|
|
||||||
def make_patterns(*specs): |
|
||||||
"""Build a 2D pattern array from per-pattern strings via ``logic.mvarray``. |
|
||||||
|
|
||||||
Each string holds one character per s-node, ordered as the inputs and |
|
||||||
outputs are defined in the netlist (output positions are don't-cares here, |
|
||||||
overwritten by simulation). The result has shape ``(n_s_nodes, n_patterns)`` |
|
||||||
as expected by the simulators; a lone pattern is reshaped to a single column. |
|
||||||
""" |
|
||||||
pat = logic.mvarray(*specs) |
|
||||||
return pat if pat.ndim == 2 else pat.reshape(-1, 1) |
|
||||||
|
|
||||||
|
|
||||||
def classify(alg, circuit, faults, patterns): |
|
||||||
# PPSFP requires the batch size to match the pattern count (as main.py does). |
|
||||||
sim = alg(circuit, patterns.shape[1]) |
|
||||||
return sim.classify_faults(list(faults), patterns) |
|
||||||
|
|
||||||
|
|
||||||
def saf(line, polarity): |
|
||||||
return line.index * 2 + polarity |
|
||||||
|
|
||||||
|
|
||||||
# --------------------------------------------------------------------------- # |
|
||||||
# Inline single-gate circuits with hand-computed expectations. |
|
||||||
# --------------------------------------------------------------------------- # |
|
||||||
|
|
||||||
@pytest.mark.parametrize('alg', ALL_ALGS) |
|
||||||
def test_inv_single_pattern(alg): |
|
||||||
# s-nodes are 'i','o'. i=0 => golden o=1. Detect faults that flip o off 1. |
|
||||||
c = bench.parse('input(i) output(o) o=INV(i)') |
|
||||||
oline = c.forks['o'].ins[0] |
|
||||||
iline = oline.driver.ins[0] |
|
||||||
pat = make_patterns('0-') # i=0 (o position is a don't-care) |
|
||||||
faults = [saf(oline, 0), saf(oline, 1), saf(iline, 0), saf(iline, 1)] |
|
||||||
r = classify(alg, c, faults, pat) |
|
||||||
# o s-a-0 forces 0 (!=1) -> detected; i s-a-1 forces i=1 -> o=0 -> detected. |
|
||||||
assert r['DS'] == {saf(oline, 0), saf(iline, 1)} |
|
||||||
# o s-a-1 already matches golden; i s-a-0 keeps i=0 -> nothing changes. |
|
||||||
assert r['NO'] == {saf(oline, 1), saf(iline, 0)} |
|
||||||
|
|
||||||
|
|
||||||
@pytest.mark.parametrize('alg', ALL_ALGS) |
|
||||||
def test_inv_both_polarities_detected(alg): |
|
||||||
# Applying both i=0 and i=1 sensitises every fault of the inverter. |
|
||||||
c = bench.parse('input(i) output(o) o=INV(i)') |
|
||||||
oline = c.forks['o'].ins[0] |
|
||||||
iline = oline.driver.ins[0] |
|
||||||
pat = make_patterns('00', '10') # i=0 and i=1 |
|
||||||
faults = [saf(oline, 0), saf(oline, 1), saf(iline, 0), saf(iline, 1)] |
|
||||||
r = classify(alg, c, faults, pat) |
|
||||||
assert r['DS'] == set(faults) |
|
||||||
assert r['NO'] == set() |
|
||||||
|
|
||||||
|
|
||||||
@pytest.mark.parametrize('alg', ALL_ALGS) |
|
||||||
def test_and2_output(alg): |
|
||||||
# s-nodes are 'i0','i1','o'. |
|
||||||
c = bench.parse('input(i0,i1) output(o) o=AND2(i0,i1)') |
|
||||||
oline = c.forks['o'].ins[0] |
|
||||||
o_sa0, o_sa1 = saf(oline, 0), saf(oline, 1) |
|
||||||
|
|
||||||
# i0=i1=1 => golden o=1: only o s-a-0 is observable. |
|
||||||
r = classify(alg, c, [o_sa0, o_sa1], make_patterns('110')) |
|
||||||
assert r['DS'] == {o_sa0} |
|
||||||
assert r['NO'] == {o_sa1} |
|
||||||
|
|
||||||
# i0=0,i1=1 => golden o=0: only o s-a-1 is observable. |
|
||||||
r = classify(alg, c, [o_sa0, o_sa1], make_patterns('010')) |
|
||||||
assert r['DS'] == {o_sa1} |
|
||||||
assert r['NO'] == {o_sa0} |
|
||||||
|
|
||||||
|
|
||||||
@pytest.mark.parametrize('alg', ALL_ALGS) |
|
||||||
def test_two_level_nand_propagation(alg): |
|
||||||
# o = NAND2(NAND2(a,b), c); s-nodes 'a','b','c','o'. a=b=c=1: n=0, o=1. |
|
||||||
c = bench.parse('input(a,b,c) output(o) n=NAND2(a,b) o=NAND2(n,c)') |
|
||||||
nline = c.forks['n'].ins[0] |
|
||||||
oline = c.forks['o'].ins[0] |
|
||||||
faults = [saf(nline, 0), saf(nline, 1), saf(oline, 0), saf(oline, 1)] |
|
||||||
r = classify(alg, c, faults, make_patterns('1110')) |
|
||||||
# n already 0 (s-a-0 invisible); n s-a-1 -> o=0; o s-a-0 visible; o already 1. |
|
||||||
assert r['DS'] == {saf(nline, 1), saf(oline, 0)} |
|
||||||
assert r['NO'] == {saf(nline, 0), saf(oline, 1)} |
|
||||||
|
|
||||||
|
|
||||||
# --------------------------------------------------------------------------- # |
|
||||||
# c17 fixture: small, fully testable combinational benchmark. |
|
||||||
# --------------------------------------------------------------------------- # |
|
||||||
|
|
||||||
def _c17_exhaustive_patterns(): |
|
||||||
"""All 2**5 input combinations of c17. |
|
||||||
|
|
||||||
s-nodes are inputs 1,2,3,6,7 then outputs 22,23 (netlist order); the two |
|
||||||
output positions are don't-cares appended after the five input bits. |
|
||||||
""" |
|
||||||
return make_patterns(*[''.join(combo) + '--' |
|
||||||
for combo in itertools.product('01', repeat=5)]) |
|
||||||
|
|
||||||
|
|
||||||
@pytest.mark.parametrize('alg', ALL_ALGS) |
|
||||||
def test_c17_fully_detected(alg, c17_bench, c17_resolved): |
|
||||||
# c17 has no redundant faults, so exhaustive patterns detect every fault. |
|
||||||
fs = FaultSet(c17_bench, KYUPY, c17_resolved) |
|
||||||
faults = list(fs.saf_equiv_classes.keys()) |
|
||||||
pat = _c17_exhaustive_patterns() |
|
||||||
r = classify(alg, c17_resolved, faults, pat) |
|
||||||
assert r['DS'] == set(faults) |
|
||||||
assert r['NO'] == set() |
|
||||||
|
|
||||||
|
|
||||||
@pytest.mark.parametrize('alg', ALL_ALGS) |
|
||||||
def test_c17_output_fault_class(alg, c17_resolved): |
|
||||||
# All-zero inputs: output 22 settles to 0, so only its s-a-1 is observable. |
|
||||||
o22 = c17_resolved.forks['22'].ins[0] |
|
||||||
pat = make_patterns('00000--') # all inputs 0 |
|
||||||
r = classify(alg, c17_resolved, [saf(o22, 0), saf(o22, 1)], pat) |
|
||||||
assert r['DS'] == {saf(o22, 1)} |
|
||||||
assert r['NO'] == {saf(o22, 0)} |
|
||||||
|
|
||||||
|
|
||||||
# --------------------------------------------------------------------------- # |
|
||||||
# s27 fixture: exposes the exact-vs-optimistic difference between simulators. |
|
||||||
# --------------------------------------------------------------------------- # |
|
||||||
|
|
||||||
def _s27_setup(s27_bench, s27_resolved): |
|
||||||
fs = FaultSet(s27_bench, KYUPY, s27_resolved) |
|
||||||
faults = list(fs.saf_equiv_classes.keys()) |
|
||||||
rng = np.random.default_rng(1) |
|
||||||
pat = rng.choice([logic.ZERO, logic.ONE], |
|
||||||
size=(len(s27_resolved.s_nodes(KYUPY)), 64)).astype(np.uint8) |
|
||||||
return faults, pat |
|
||||||
|
|
||||||
|
|
||||||
def test_s27_exact_simulators_agree(s27_bench, s27_resolved): |
|
||||||
faults, pat = _s27_setup(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 one fault unobserved. |
|
||||||
assert len(simple['DS']) == 31 |
|
||||||
assert len(simple['NO']) == 1 |
|
||||||
|
|
||||||
|
|
||||||
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) |
|
||||||
|
|
||||||
# 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) |
|
||||||
def test_ppsfp_multibranch_stem_observability(alg): |
|
||||||
# Stem `s` fans out to two AND gates; with sel1=0,sel2=1 the stem is |
|
||||||
# observable only through the o2 branch (the stem's *second* fanout line). |
|
||||||
c = bench.parse('input(a,b,sel1,sel2) output(o1,o2) ' |
|
||||||
's=NAND2(a,b) o1=AND2(s,sel1) o2=AND2(s,sel2)') |
|
||||||
a_sa0 = saf(c.forks['s'].ins[0].driver.ins[0], 0) |
|
||||||
# a=1,b=1,sel1=0,sel2=1: a s-a-0 flips s, propagating through o2 only. |
|
||||||
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'] |
|
||||||
Loading…
Reference in new issue