PWR-HYBRID-3/fret-pipeline/docs/trace_aiger.md

# trace_aiger.py -- Circuit Tracer and State Machine Visualizer

## Purpose

Takes a synthesized AIGER circuit and produces a complete state machine
analysis: full transition tables, reachability analysis, and a Graphviz DOT
diagram with human-readable guard condition labels. Every label is derived
from exhaustive circuit evaluation -- no manual annotation, no probabilistic
inference.

## Usage

```bash
python3 scripts/trace_aiger.py <circuit.aag> [output_dir]
dot -Tpng diagrams/SPEC_states.dot -o diagrams/SPEC_states.png
```

The script is generic -- it works with any `.aag` file, not just the PWR
reactor controller.

## How It Works

### Phase 1: Parse (`parse_aag`)

Reads the ASCII AIGER file and extracts:

- **Input literals**: the environment signals (even numbers)
- **Latch pairs**: `(current_literal, next_state_literal)` for each state bit
- **Output literals**: which computed values are controller outputs
- **AND gates**: the combinational logic `(lhs, rhs0, rhs1)`
- **Symbol table**: human-readable names for inputs/outputs

Returns a dictionary that `eval_circuit` can simulate.

### Phase 2: Simulate (`eval_circuit`)

Evaluates the circuit for one clock cycle given specific latch values (current
state) and input values (environment signals).

**How it works:**

1. Initialize a literal-value table with constant 0/1
2. Set input literals and their negations: `val[lit] = v; val[lit ^ 1] = 1 - v`
3. Set latch literals the same way
4. Evaluate AND gates in order: `val[lhs] = val[rhs0] & val[rhs1]`
5. Read output values and next-state latch values from the table

The `^ 1` trick exploits AIGER's literal encoding: even literals are positive,
odd literals are negated. XOR-ing with 1 flips between positive and negative.
This means we never need explicit negation logic -- every gate's inputs are
already in the table, whether positive or negated.

**Critical assumption:** AND gates are listed in topological order in the AIGER
file, so evaluating them sequentially guarantees all inputs are computed before
they're needed. This is a property of the AIGER format specification.

### Phase 3: Enumerate

For every combination of latch state and input values:

- `2^L` latch states (L = number of latches)
- `2^I` input combinations (I = number of inputs)
- Total: `2^(L+I)` evaluations

For the PWR reactor: 2 latches, 6 inputs = 256 evaluations. Trivial.

For each evaluation, records:
- Which outputs are active (determines the "mode")
- What the next latch state is (determines the transition)

Results are stored in:
- `transitions[src_state][dst_state]` = set of input tuples
- `state_modes[state]` = set of mode labels

### Phase 4: Reachability Analysis

Starting from the initial state (all latches = 0), performs a breadth-first
search through the transition graph to identify which states are actually
reachable during operation. Unreachable states are grayed out in the diagram.

### Phase 5: Guard Extraction (`extract_guard`)

This is the core algorithm that makes the diagram human-readable. Given a set
of input combinations that all produce the same transition, it finds a minimal
boolean expression describing exactly that set.

**Simple case -- single conjunction:**

For each input variable, check if it's fixed (always 0 or always 1) or
don't-care (both 0 and 1 appear) across all combos. If the fixed variables
alone perfectly predict the combo count (`2^(don't-cares) == combo count`),
the guard is a single AND of the fixed variables.

Example: the shutdown-to-heatup edge has 32 combos. In all 32,
`t_avg_above_min = 1`. The other 5 inputs vary freely: `2^5 = 32`. So the
guard is simply `t_avg_above_min`.

**Complex case -- cube covering:**

When a single conjunction can't explain the combo set, the algorithm uses
greedy cube covering:

1. Pick a sample combo from the uncovered set
2. Start with all variables fixed to the sample's values (a point cube)
3. Try relaxing each variable (making it don't-care), one at a time
4. Accept the relaxation only if the expanded cube is a strict subset of the
   edge's combos (`trial_set <= combo_set`) -- this prevents the cube from
   "leaking" into other transitions
5. Repeat relaxation until no more variables can be freed
6. Record this cube, remove its combos from the uncovered set, go to step 1
7. OR all the cubes together

**What is a "cube"?** A conjunction where some variables are fixed and the
rest are don't-care. Example: `inv1_holds & !t_avg_in_range` fixes 2 of 6
variables, so it covers `2^4 = 16` input combinations. The term comes from
digital logic (Karnaugh maps), where a cube is a rectangular group of cells.

**Correctness guarantee:** The subset check `trial_set <= combo_set` on line
176 ensures that every cube covers ONLY combos belonging to this edge. The
check tests set containment, not size -- even one foreign combo causes
rejection. The union of all cubes exactly equals the original combo set.

**Optimality caveat:** The greedy algorithm does not guarantee a minimal
number of cubes. The order in which variables are relaxed can affect the
result. For guaranteed minimality, a Quine-McCluskey or Espresso algorithm
would be needed. In practice, with 6 inputs, the greedy result is typically
optimal or off by at most one cube.

### Phase 6: DOT Generation

Produces a Graphviz DOT file with:

- **State nodes** labeled with human-readable mode names (stripping `in_`
  prefix, uppercasing)
- **Edge labels** showing the extracted guard conditions
- **Color coding:**
  - State fill: blue (initial), yellow (transitory), green (operation),
    red (scram/emergency), gray (unreachable)
  - Edge color: blue (self-loop/stay), green (normal transition),
    red (scram transition)
  - Edge width: thicker for edges with more input combinations

Color assignment uses keyword heuristics on the output variable names
(e.g., "scram" in the name -> red). This is cosmetic and does not affect
correctness.

## Scaling Considerations

The exhaustive enumeration approach has complexity `O(2^(L+I) * A)` where
`A` is the number of AND gates. This is perfectly tractable for small
controllers:

| Latches | Inputs | Evaluations | Feasible? |
|---|---|---|---|
| 2 | 6 | 256 | Instant |
| 3 | 8 | 2,048 | Instant |
| 4 | 10 | 16,384 | < 1 second |
| 5 | 12 | 131,072 | ~ seconds |
| 8 | 16 | 16M | ~ minutes |
| 10 | 20 | 1B | Impractical |

For controllers with more than ~12 latches, a symbolic (BDD-based) analysis
would be needed instead of exhaustive enumeration.

## Future Improvements

- **Symbolic analysis**: Replace exhaustive enumeration with BDD-based
  reachability for large controllers. Libraries like `dd` (Python) or
  direct use of Spot's automata operations could handle this.

- **Guard minimization**: Replace the greedy cube-covering algorithm with
  Espresso or Quine-McCluskey for guaranteed minimal expressions. The Python
  `pyeda` library provides `espresso_exprs()` for this.

- **Trace simulation**: Add a mode that simulates specific input sequences
  step-by-step, showing the controller's response. Useful for validating
  against specific scenarios (e.g., "what happens if t_avg_above_min is
  asserted, then inv1_holds drops?").

- **Cross-reference with FRET requirements**: Annotate each edge with which
  FRET requirement(s) it satisfies. This would provide traceability from the
  synthesized controller back to the natural-language specifications.

- **Multi-output modes**: Currently assumes each state has exactly one active
  output (mode). If the controller has overlapping outputs, the labeling
  would need to handle composite states.

- **Interactive HTML output**: Generate an interactive diagram (e.g., using
  D3.js or vis.js) instead of static SVG, allowing users to click states
  and see the full transition table for that state.