write_path_spice: match side input values to the path arc's transitions (#475)

* write_path_spice: match side input values to the path arc's transitions

gatePortValues() chose side input values from the first CUDD cube of the
Boolean difference d(f)/d(input), which sensitizes the gate but ignores
the transition directions of the arc the path used:

- For non-unate gates whose Boolean difference is a tautology (xor2,
  xnor2) every side variable came back don't-care, and the unknown value
  fell through to tie-low in writeSubcktInstVoltSrcs() -- wrong whenever
  the path used the when-condition requiring the side high.
- For mux select arcs the cube was an arbitrary data assignment,
  unrelated to the output edge the path reported.

Either way the written deck's gate drives the opposite direction from
the reported path: the simulated chain switches with inverted polarity
from that gate onward, edge-qualified arrival measurements fail, and
the deck sums delays from the wrong rise/fall tables.

Constrain the side input condition to the cofactor pair matching this
arc -- f1 & !f0 when the input and driver edges agree (non-inverting),
f0 & !f1 when they differ (inverting) -- threading the gate input
RiseFall from the path stage into gatePortValues().  Also release the
CUDD nodes that were previously leaked (the old code Cudd_Ref'd the
Boolean difference after the generator was freed and never deref'd it).

Fixes #474

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* test: write_path_spice
  arc-sense regression for #474, and outlined in #475

---------

Co-authored-by: Brian Degnan <bpdegnan@users.noreply.github.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

spice/WritePathSpice.cc

@@ -514,11 +514,13 @@ WritePathSpice::writeGateStage(Stage stage)
 
   const Path *drvr_path = stageDrvrPath(stage);
   const RiseFall *drvr_rf = drvr_path->transition(this);
+  const Path *gate_input_path = stageGateInputPath(stage);
+  const RiseFall *input_rf = gate_input_path->transition(this);
   const Edge *gate_edge = stageGateEdge(stage);
 
   LibertyPortLogicValues port_values;
   bool is_clked;
-  gatePortValues(input_pin, drvr_pin, drvr_rf, gate_edge,
+  gatePortValues(input_pin, drvr_pin, input_rf, drvr_rf, gate_edge,
                  port_values, is_clked);
 
   PinSet inputs(network_);

spice/WriteSpice.cc

@@ -756,6 +756,7 @@ WriteSpice::railToRailSlew(float slew,
 void
 WriteSpice::gatePortValues(const Pin *input_pin,
                            const Pin *drvr_pin,
+                           const RiseFall *input_rf,
                            const RiseFall *drvr_rf,
                            const Edge *gate_edge,
                            // Return values.
@@ -771,7 +772,7 @@ WriteSpice::gatePortValues(const Pin *input_pin,
     if (gate_edge && gate_edge->role()->genericRole() == TimingRole::regClkToQ())
       regPortValues(input_pin, drvr_rf, drvr_port, drvr_func, port_values, is_clked);
     else
-      gatePortValues(inst, drvr_func, input_port, port_values);
+      gatePortValues(inst, drvr_func, input_port, input_rf, drvr_rf, port_values);
   }
 }
 
@@ -779,41 +780,61 @@ void
 WriteSpice::gatePortValues(const Instance *,
                            const FuncExpr *expr,
                            const LibertyPort *input_port,
+                           const RiseFall *input_rf,
+                           const RiseFall *drvr_rf,
                            // Return values.
                            LibertyPortLogicValues &port_values)
 {
+  DdManager *cudd_mgr = bdd_.cuddMgr();
   DdNode *bdd = bdd_.funcBdd(expr);
   DdNode *input_node = bdd_.findNode(input_port);
-  unsigned input_node_index = Cudd_NodeReadIndex(input_node);
+  // Cofactors of the driver function wrt the switching (path) input.
-  DdManager *cudd_mgr = bdd_.cuddMgr();
+  DdNode *f1 = Cudd_Cofactor(cudd_mgr, bdd, input_node);
-  DdNode *diff = Cudd_bddBooleanDiff(cudd_mgr, bdd, input_node_index);
+  Cudd_Ref(f1);
+  DdNode *f0 = Cudd_Cofactor(cudd_mgr, bdd, Cudd_Not(input_node));
+  Cudd_Ref(f0);
+  // The side inputs must sensitize the path with the polarity of this
+  // arc, not just any sensitization: for non-unate gates (xor/xnor, mux
+  // select arcs) the side values decide whether the gate inverts, so a
+  // cube of the plain Boolean difference (f1 XOR f0) can put the gate on
+  // the arc opposite to the one the path used.
+  //   input and driver edges agree  (non-inverting): f1 & ~f0
+  //   input and driver edges differ (inverting):     f0 & ~f1
+  DdNode *care = (input_rf == drvr_rf)
+    ? Cudd_bddAnd(cudd_mgr, f1, Cudd_Not(f0))
+    : Cudd_bddAnd(cudd_mgr, f0, Cudd_Not(f1));
+  Cudd_Ref(care);
+
   int *cube;
   CUDD_VALUE_TYPE value;
-  DdGen *cube_gen = Cudd_FirstCube(cudd_mgr, diff, &cube, &value);
+  DdGen *cube_gen = Cudd_FirstCube(cudd_mgr, care, &cube, &value);
-
+  if (!Cudd_IsGenEmpty(cube_gen)) {
-  LibertyPortSet ports = expr->ports();
+    LibertyPortSet ports = expr->ports();
-  for (const LibertyPort *port : ports) {
+    for (const LibertyPort *port : ports) {
-    if (port != input_port) {
+      if (port != input_port) {
-      DdNode *port_node = bdd_.findNode(port);
+        DdNode *port_node = bdd_.findNode(port);
-      int var_index = Cudd_NodeReadIndex(port_node);
+        int var_index = Cudd_NodeReadIndex(port_node);
-      LogicValue value;
+        LogicValue port_value;
-      switch (cube[var_index]) {
+        switch (cube[var_index]) {
-        case 0:
+          case 0:
-          value = LogicValue::zero;
+            port_value = LogicValue::zero;
-          break;
+            break;
-        case 1:
+          case 1:
-          value = LogicValue::one;
+            port_value = LogicValue::one;
-          break;
+            break;
-        case 2:
+          case 2:
-        default:
+          default:
-          value = LogicValue::unknown;
+            port_value = LogicValue::unknown;
-          break;
+            break;
+        }
+        port_values[port] = port_value;
       }
-      port_values[port] = value;
     }
   }
   Cudd_GenFree(cube_gen);
-  Cudd_Ref(diff);
+  Cudd_RecursiveDeref(cudd_mgr, care);
+  Cudd_RecursiveDeref(cudd_mgr, f0);
+  Cudd_RecursiveDeref(cudd_mgr, f1);
   bdd_.clearVarMap();
 }
 

spice/WriteSpice.hh

@@ -139,6 +139,7 @@ protected:
 
   void gatePortValues(const Pin *input_pin,
                       const Pin *drvr_pin,
+                      const RiseFall *input_rf,
                       const RiseFall *drvr_rf,
                       const Edge *gate_edge,
                       // Return values.
@@ -154,6 +155,8 @@ protected:
   void gatePortValues(const Instance *inst,
                       const FuncExpr *expr,
                       const LibertyPort *input_port,
+                      const RiseFall *input_rf,
+                      const RiseFall *drvr_rf,
                       // Return values.
                       LibertyPortLogicValues &port_values);
   void writeSubcktInstLoads(const Pin *drvr_pin,

test/regression_vars.tcl

@@ -175,6 +175,7 @@ record_public_tests {
   verilog_write_escape
   verilog_write_gzip
   verilog_unconnected_hpin
+  write_path_spice_arc_sense
 }
 
 define_test_group fast [group_tests all]

test/write_path_spice_arc_sense.cells.spice

@@ -0,0 +1,40 @@
+* Copyright 2020 The SkyWater PDK Authors
+*
+* Licensed under the Apache License, Version 2.0 (the "License");
+* you may not use this file except in compliance with the License.
+* You may obtain a copy of the License at
+*
+*     https://www.apache.org/licenses/LICENSE-2.0
+*
+* Unless required by applicable law or agreed to in writing, software
+* distributed under the License is distributed on an "AS IS" BASIS,
+* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+* See the License for the specific language governing permissions and
+* limitations under the License.
+*
+* SPDX-License-Identifier: Apache-2.0
+
+
+.subckt sky130_fd_sc_hd__xor2_1 A B VGND VNB VPB VPWR X
+X0 a_35_297# A VGND VNB sky130_fd_pr__nfet_01v8 w=650000u l=150000u
+X1 VGND B a_35_297# VNB sky130_fd_pr__nfet_01v8 w=650000u l=150000u
+X2 X a_35_297# VGND VNB sky130_fd_pr__nfet_01v8 w=650000u l=150000u
+X3 a_285_297# B VPWR VPB sky130_fd_pr__pfet_01v8_hvt w=1e+06u l=150000u
+X4 VPWR A a_285_297# VPB sky130_fd_pr__pfet_01v8_hvt w=1e+06u l=150000u
+X5 a_35_297# B a_117_297# VPB sky130_fd_pr__pfet_01v8_hvt w=1e+06u l=150000u
+X6 a_117_297# A VPWR VPB sky130_fd_pr__pfet_01v8_hvt w=1e+06u l=150000u
+X7 a_285_47# B X VNB sky130_fd_pr__nfet_01v8 w=650000u l=150000u
+X8 a_285_297# a_35_297# X VPB sky130_fd_pr__pfet_01v8_hvt w=1e+06u l=150000u
+X9 VGND A a_285_47# VNB sky130_fd_pr__nfet_01v8 w=650000u l=150000u
+.ends
+
+* Absorber stubs: write_path_spice's lib_subckt reader (findCellSubckts) treats
+* the last token of every device line as a subckt-call name, so a flat
+* transistor netlist makes it look for the parameter "l=150000u" and the
+* closing ".ends" as if they were cells.  These empty subckts satisfy that
+* lookup; only the sky130_fd_sc_hd__xor2_1 subckt above is real.  (Unrelated to
+* the arc-sense fix under test.)
+.subckt l=150000u
+.ends
+.subckt .ends
+.ends

test/write_path_spice_arc_sense.models.spice

@@ -0,0 +1,6 @@
+* Placeholder SPICE model file for the write_path_spice_arc_sense regression.
+*
+* write_path_spice requires a -model_file and emits it as a ".include" line in
+* the generated deck, but does not read its contents.  The regression only
+* diffs the written deck, so no transistor models are needed here.  Supply the
+* real SKY130 sky130_fd_pr models if you want to simulate the deck in ngspice.

test/write_path_spice_arc_sense.ok

@@ -0,0 +1,51 @@
+Warning 1171: write_path_spice_arc_sense.lib.gz line 23, default_fanout_load is 0.0.
+* Path from a v to x ^
+.include "write_path_spice_arc_sense.models.spice"
+.include "write_path_spice_arc_sense.sp_1.subckt"
+.tran 1e-13 3.33e-09
+
+.print tran v(a) v(x0/B) v(x0/X) v(x)
+
+**************
+* Input source
+**************
+
+v1 a 0 pwl(
++0.000e+00 1.800e+00
++1.667e-11 0.000e+00
++3.333e-09 0.000e+00
++)
+
+*****************
+* Stage instances
+*****************
+
+xstage1 a x0/B stage1
+xstage2 x0/B x0/X x stage2
+
+***************
+* Stage subckts
+***************
+
+.subckt stage1 a x0/B
+* Net a
+* Net has no parasitics.
+R1 a x0/B 1.000e-04
+.ends
+
+.subckt stage2 x0/B x0/X x
+* Gate x0 B -> X
+xx0 x0/A x0/B x0/VGND x0/VNB x0/VPB x0/VPWR x0/X sky130_fd_sc_hd__xor2_1
+v1 x0/A 0 1.800
+v2 x0/VGND 0 0.000
+v3 x0/VNB 0 0.000
+v4 x0/VPB 0 1.800
+v5 x0/VPWR 0 1.800
+
+* Load pins
+* Net x
+* Net has no parasitics.
+R1 x0/X x 1.000e-04
+.ends
+
+.end

test/write_path_spice_arc_sense.tcl

@@ -0,0 +1,20 @@
+# write_path_spice ties non-unate side inputs to the sensitized arc (issue #474)
+source helpers.tcl
+read_liberty write_path_spice_arc_sense.lib.gz
+read_verilog write_path_spice_arc_sense.v
+link_design repro
+create_clock -name vclk -period 10
+set_input_delay -clock vclk 0 [all_inputs]
+set_output_delay -clock vclk 0 [all_outputs]
+# Force the inverting arc B(fall) -> X(rise), which the liberty defines only
+# under "when A" (A=1).  The xor2 side input A is the unconstrained port s, so
+# a correct deck must tie x0/A high (v1 x0/A 0 1.800).  Before the fix the
+# Boolean-difference cube ignored the arc direction and tied it low (0.000).
+set spice_file [make_result_file "write_path_spice_arc_sense.sp"]
+write_path_spice -path_args {-path_delay max -fall_from [get_ports a] -rise_to [get_ports x]} \
+  -spice_file $spice_file \
+  -lib_subckt_file write_path_spice_arc_sense.cells.spice \
+  -model_file write_path_spice_arc_sense.models.spice \
+  -power VPWR -ground VGND \
+  -simulator ngspice
+report_file ${spice_file}_1.sp

test/write_path_spice_arc_sense.v

@@ -0,0 +1,7 @@
+// Minimal repro for the write_path_spice non-unate side-input tie bug.
+// One xor2: the timed path enters pin B, the side input A comes from an
+// unconstrained port, so STA knows no constant for it and write_path_spice
+// must pick a tie that matches the arc it sensitized.
+module repro (input a, input s, output x);
+  sky130_fd_sc_hd__xor2_1 x0 (.A(s), .B(a), .X(x));
+endmodule