puff: implement PP5000 port power control

The EC watches current limiting on the USB and HDMI ports to keep system
load on the 5V rail within the limits of the regulator. The EC's goal is
to ensure that any single future state change (connecting or
disconnecting a port) doesn't push the 5V rail overcurrent.

Verification is done via symbolic execution with Klee; ensuring that
there exists no state where plugging something into a port with no
further changes would put us over the power budget. Sample verification
output:

> KLEE: Using Z3 solver backend
>
> KLEE: done: total instructions = 4439
> KLEE: done: completed paths = 30
> KLEE: done: generated tests = 30

v2: convert ad-hoc state space exploration for verification to symbolic
execution, allowing port control code to be reused for both.

BUG=b:143190102
TEST=make buildall
BRANCH=none

Change-Id: If06e319c8d38bd11b29a7e69499d40357176a97e
Signed-off-by: Peter Marheine <pmarheine@chromium.org>
Reviewed-on: https://chromium-review.googlesource.com/c/chromiumos/platform/ec/+/1911261
Reviewed-by: Andrew McRae <amcrae@chromium.org>

6 files changed, 262 insertions, 9 deletions

diff --git a/board/puff/Makefile b/board/puff/Makefile
new file mode 100644
index 0000000000..bc7435ed75
--- /dev/null
+++ b/board/puff/Makefile
@@ -0,0 +1,21 @@
+# Copyright 2019 The Chromium OS Authors. All rights reserved.
+# Use of this source code is governed by a BSD-style license that can be
+# found in the LICENSE file.
+CLANG:=clang-6.0
+KLEE:=klee
+KTEST_TOOL:=ktest-tool
+
+.PHONY: report
+report: klee-last
+	$(KTEST_TOOL) \
+		$(patsubst %.assert.err,%.ktest,$(wildcard klee-last/test*.assert.err))
+
+klee-last: validate_port_power.bc
+	$(KLEE) --emit-all-errors $^
+
+validate_port_power.bc: validate_port_power.c port-sm.c
+	$(CLANG) -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o $@ $<
+
+.PHONY: clean
+clean:
+	rm -rf validate_port_power.bc klee-last klee-out-*
diff --git a/board/puff/board.c b/board/puff/board.c
index 7e27178469..4e78186b6c 100644
--- a/board/puff/board.c
+++ b/board/puff/board.c
@@ -55,6 +55,61 @@ static void tcpc_alert_event(enum gpio_signal signal)
 		schedule_deferred_pd_interrupt(0);
 }
 
+#include "port-sm.c"
+
+static bool usbc_overcurrent;
+/*
+ * Update USB port power limits based on current state.
+ *
+ * Port power consumption is assumed to be negligible if not overcurrent,
+ * and we have two knobs: the front port power limit, and the USB-C power limit.
+ * Either one of the front ports may run at high power (one at a time) or we
+ * can limit both to low power. On USB-C we can similarly limit the port power,
+ * but there's only one port.
+ */
+void update_port_limits(void)
+{
+	struct port_states state = {
+		.bitfield = (!gpio_get_level(GPIO_USB_A0_OC_ODL)
+			     << PORTMASK_FRONT_A0) |
+			    (!gpio_get_level(GPIO_USB_A1_OC_ODL)
+			     << PORTMASK_FRONT_A1) |
+			    (!gpio_get_level(GPIO_USB_A2_OC_ODL)
+			     << PORTMASK_REAR_A0) |
+			    (!gpio_get_level(GPIO_USB_A3_OC_ODL)
+			     << PORTMASK_REAR_A1) |
+			    (!gpio_get_level(GPIO_USB_A4_OC_ODL)
+			     << PORTMASK_REAR_A2) |
+			    (!gpio_get_level(GPIO_HDMI_CONN0_OC_ODL)
+			     << PORTMASK_HDMI0) |
+			    (!gpio_get_level(GPIO_HDMI_CONN1_OC_ODL)
+			     << PORTMASK_HDMI1) |
+			    ((ppc_is_sourcing_vbus(0) && usbc_overcurrent)
+			     << PORTMASK_TYPEC),
+		.front_a_limited = gpio_get_level(GPIO_USB_A_LOW_PWR_OD),
+		/* Assume high-power; there's no way to poll this. */
+		/*
+		 * TODO(b/143190102) add a way to poll port power limit so we
+		 * can detect when it can be increased again if the port is
+		 * already active.
+		 */
+		.c_low_power = 0,
+	};
+
+	update_port_state(&state);
+
+	ppc_set_vbus_source_current_limit(0,
+		state.c_low_power ? TYPEC_RP_1A5 : TYPEC_RP_3A0);
+	/* Output high limits power */
+	gpio_set_level(GPIO_USB_A_LOW_PWR_OD, state.front_a_limited);
+}
+DECLARE_DEFERRED(update_port_limits);
+
+static void port_ocp_interrupt(enum gpio_signal signal)
+{
+	hook_call_deferred(&update_port_limits_data, 0);
+}
+
 #include "gpio_list.h" /* Must come after other header files. */
 
 /******************************************************************************/
@@ -227,6 +282,7 @@ const unsigned int ina3221_count = ARRAY_SIZE(ina3221);
 
 static void board_init(void)
 {
+	update_port_limits();
 }
 DECLARE_HOOK(HOOK_INIT, board_init, HOOK_PRIO_DEFAULT);
 
@@ -236,6 +292,11 @@ struct ppc_config_t ppc_chips[CONFIG_USB_PD_PORT_MAX_COUNT] = {
 };
 unsigned int ppc_cnt = ARRAY_SIZE(ppc_chips);
 
+/* USB-A port control */
+const int usb_port_enable[USB_PORT_COUNT] = {
+	GPIO_EN_PP5000_USB_VBUS,
+};
+
 /* Power Delivery and charging functions */
 void baseboard_tcpc_init(void)
 {
@@ -283,4 +344,5 @@ void board_overcurrent_event(int port, int is_overcurrented)
 	/* Sanity check the port. */
 	if ((port < 0) || (port >= CONFIG_USB_PD_PORT_MAX_COUNT))
 		return;
+	usbc_overcurrent = is_overcurrented;
 }
diff --git a/board/puff/board.h b/board/puff/board.h
index 81fe94f363..85337b55af 100644
--- a/board/puff/board.h
+++ b/board/puff/board.h
@@ -143,7 +143,9 @@
 #define CONFIG_USBC_VCONN_SWAP
 
 /* USB Type A Features */
-/* TODO: (b/143190102) Finish USB A config */
+#define CONFIG_USB_PORT_POWER_DUMB
+/* There are five ports, but power enable is ganged across all of them. */
+#define USB_PORT_COUNT 1
 
 /* I2C Bus Configuration */
 #define CONFIG_I2C
diff --git a/board/puff/gpio.inc b/board/puff/gpio.inc
index f578c2b6c9..d66cf09c2f 100644
--- a/board/puff/gpio.inc
+++ b/board/puff/gpio.inc
@@ -36,6 +36,15 @@ GPIO_INT(USB_C0_TCPPC_INT_ODL, PIN(E, 0), GPIO_INT_FALLING, ppc_interrupt)
 GPIO_INT(USB_C0_TCPC_INT_ODL,  PIN(6, 2), GPIO_INT_FALLING, tcpc_alert_event)
 GPIO_INT(H1_EC_RECOVERY_BTN_ODL, PIN(2, 4), GPIO_INT_BOTH, button_interrupt)
 
+/* Port power control interrupts */
+GPIO_INT(HDMI_CONN0_OC_ODL,    PIN(0, 7), GPIO_INT_BOTH, port_ocp_interrupt)
+GPIO_INT(HDMI_CONN1_OC_ODL,    PIN(0, 6), GPIO_INT_BOTH, port_ocp_interrupt)
+GPIO_INT(USB_A0_OC_ODL,        PIN(E, 4), GPIO_ODR_HIGH, port_ocp_interrupt)
+GPIO_INT(USB_A1_OC_ODL,        PIN(A, 2), GPIO_ODR_HIGH, port_ocp_interrupt)
+GPIO_INT(USB_A2_OC_ODL,        PIN(F, 5), GPIO_ODR_HIGH, port_ocp_interrupt)
+GPIO_INT(USB_A3_OC_ODL,        PIN(0, 3), GPIO_ODR_HIGH, port_ocp_interrupt)
+GPIO_INT(USB_A4_OC_ODL,        PIN(B, 0), GPIO_ODR_HIGH, port_ocp_interrupt)
+
 /* PCH/CPU signals */
 GPIO(EC_PCH_SYS_PWROK,         PIN(3, 7), GPIO_OUT_LOW)
 GPIO(EC_PCH_RSMRST_L,          PIN(A, 6), GPIO_OUT_LOW)
@@ -63,12 +72,7 @@ GPIO(BJ_ADP_PRESENT_L,         PIN(8, 2), GPIO_INPUT)
 
 /* USB type A */
 GPIO(EN_PP5000_USB_VBUS,       PIN(8, 3), GPIO_OUT_LOW)
-GPIO(USB_A_LOW_PWR_OD,         PIN(9, 4), GPIO_ODR_HIGH)
-GPIO(USB_A0_OC_ODL,            PIN(E, 4), GPIO_ODR_HIGH)
-GPIO(USB_A1_OC_ODL,            PIN(A, 2), GPIO_ODR_HIGH)
-GPIO(USB_A2_OC_ODL,            PIN(F, 5), GPIO_ODR_HIGH)
-GPIO(USB_A3_OC_ODL,            PIN(0, 3), GPIO_ODR_HIGH)
-GPIO(USB_A4_OC_ODL,            PIN(B, 0), GPIO_ODR_HIGH)
+GPIO(USB_A_LOW_PWR_OD,         PIN(9, 4), GPIO_ODR_LOW)
 
 /* USB type C */
 GPIO(USB_C0_TCPC_RST,          PIN(9, 7), GPIO_OUT_LOW)
@@ -77,8 +81,6 @@ GPIO(USB_C0_TCPC_RST,          PIN(9, 7), GPIO_OUT_LOW)
 GPIO(M2_SSD_PLN,               PIN(A, 0), GPIO_INPUT)
 GPIO(EC_ENTERING_RW,           PIN(E, 3), GPIO_OUT_LOW)
 GPIO(CCD_MODE_ODL,             PIN(E, 5), GPIO_ODR_HIGH)
-GPIO(HDMI_CONN0_OC_ODL,        PIN(0, 7), GPIO_ODR_HIGH)
-GPIO(HDMI_CONN1_OC_ODL,        PIN(0, 6), GPIO_ODR_HIGH)
 GPIO(EN_PP_MST_OD,             PIN(9, 6), GPIO_ODR_LOW)
 
 /* I2C pins - Alternate function below configures I2C module on these pins */
diff --git a/board/puff/port-sm.c b/board/puff/port-sm.c
new file mode 100644
index 0000000000..d549b5754b
--- /dev/null
+++ b/board/puff/port-sm.c
@@ -0,0 +1,126 @@
+/* Copyright 2019 The Chromium OS Authors. All rights reserved.
+ * Use of this source code is governed by a BSD-style license that can be
+ * found in the LICENSE file.
+ */
+
+struct port_states {
+	/* PORT_*n masks correspond to bits in this field */
+	uint8_t bitfield;
+	/* If 1, type C is RP_1A5 (otherwise assumed to be RP_3A0) */
+	uint8_t c_low_power;
+	/* If 1, front ports are current-limited */
+	uint8_t front_a_limited;
+};
+
+#define PORTMASK_FRONT_A0 0
+#define PORTMASK_FRONT_A1 1
+#define PORTMASK_REAR_A0 2
+#define PORTMASK_REAR_A1 3
+#define PORTMASK_REAR_A2 4
+#define PORTMASK_HDMI0 5
+#define PORTMASK_HDMI1 6
+#define PORTMASK_TYPEC 7
+
+#define PORT_FRONT_A0 (1 << PORTMASK_FRONT_A0)
+#define PORT_FRONT_A1 (1 << PORTMASK_FRONT_A1)
+#define PORT_REAR_A0 (1 << PORTMASK_REAR_A0)
+#define PORT_REAR_A1 (1 << PORTMASK_REAR_A1)
+#define PORT_REAR_A2 (1 << PORTMASK_REAR_A2)
+#define PORT_HDMI0 (1 << PORTMASK_HDMI0)
+#define PORT_HDMI1 (1 << PORTMASK_HDMI1)
+#define PORT_TYPEC (1 << PORTMASK_TYPEC)
+#define PORT_ENABLED(id) (!!(states->bitfield & (PORT_##id)))
+
+#define PWR_FRONT_HIGH 1603
+#define PWR_FRONT_LOW 963
+#define PWR_REAR 1075
+#define PWR_HDMI 562
+#define PWR_C_HIGH 3740
+#define PWR_C_LOW 2090
+
+/*
+ * Calculate the amount of power (in mA) available on the 5V rail.
+ *
+ * If negative, the system is at risk of browning out.
+ */
+int compute_headroom(const struct port_states *states)
+{
+	int headroom = 10000 - 1335; /* Capacity less base load */
+
+	headroom -= PWR_HDMI * (PORT_ENABLED(HDMI0) + PORT_ENABLED(HDMI1));
+	headroom -= PWR_REAR * (PORT_ENABLED(REAR_A0) + PORT_ENABLED(REAR_A1) +
+				PORT_ENABLED(REAR_A2));
+
+	switch (PORT_ENABLED(FRONT_A0) + PORT_ENABLED(FRONT_A1)) {
+	case 2:
+		headroom -= PWR_FRONT_LOW + (states->front_a_limited ?
+						     PWR_FRONT_LOW :
+						     PWR_FRONT_HIGH);
+		break;
+	case 1:
+		headroom -= states->front_a_limited ? PWR_FRONT_LOW :
+						      PWR_FRONT_HIGH;
+		break;
+	default:
+		break;
+	}
+
+	if (PORT_ENABLED(TYPEC))
+		headroom -= states->c_low_power ? PWR_C_LOW : PWR_C_HIGH;
+
+	return headroom;
+}
+
+/*
+ * Update states to stay within the 5V rail power budget.
+ *
+ * Only the current limits (c_low_power and front_a_limited) are effective.
+ *
+ * The goal here is to ensure that any single state change from what we set
+ * (specifically, something being plugged into a port) does not exceed the 5V
+ * power budget.
+ */
+void update_port_state(struct port_states *states)
+{
+	int headroom = compute_headroom(states);
+
+	if (!PORT_ENABLED(TYPEC)) {
+		/*
+		 * USB-C not in use, prefer to adjust it. We may still need
+		 * to limit front port power.
+		 *
+		 * We want to run the front type-A ports at high power, and they
+		 * may be limited so we need to account for the extra power
+		 * we may be allowing the front ports to draw.
+		 */
+		if (headroom >
+		    (PWR_C_HIGH + (PWR_FRONT_HIGH - PWR_FRONT_LOW))) {
+			states->front_a_limited = 0;
+			states->c_low_power = 0;
+		} else {
+			states->front_a_limited =
+				headroom <
+				(PWR_C_LOW + (PWR_FRONT_HIGH - PWR_FRONT_LOW));
+			states->c_low_power = 1;
+		}
+	} else {
+		/*
+		 * USB-C is in use, prefer to drop front port limits.
+		 * Pessimistically Assume C is currently in low-power mode.
+		 */
+		if (headroom > (PWR_C_HIGH - PWR_C_LOW + PWR_FRONT_HIGH)) {
+			/* Can still go full power */
+			states->front_a_limited = 0;
+			states->c_low_power = 0;
+		} else if (headroom >
+			   (PWR_C_HIGH - PWR_C_LOW + PWR_FRONT_LOW)) {
+			/* Reducing front allows C to go to full power */
+			states->front_a_limited = 1;
+			states->c_low_power = 0;
+		} else {
+			/* Must reduce both */
+			states->front_a_limited = 1;
+			states->c_low_power = 1;
+		}
+	}
+}
diff --git a/board/puff/validate_port_power.c b/board/puff/validate_port_power.c
new file mode 100644
index 0000000000..7afc870fc1
--- /dev/null
+++ b/board/puff/validate_port_power.c
@@ -0,0 +1,40 @@
+/* Copyright 2019 The Chromium OS Authors. All rights reserved.
+ * Use of this source code is governed by a BSD-style license that can be
+ * found in the LICENSE file.
+ */
+
+#include <klee/klee.h>
+
+#include "port-sm.c"
+
+int main(void)
+{
+	uint8_t bitfield = klee_range(0, 256, "port_bitmask");
+	uint8_t c_low_power = klee_range(0, 2, "c_low_power");
+	uint8_t front_a_limited = klee_range(0, 2, "front_a_limited");
+	struct port_states states = {
+		.bitfield = bitfield,
+		.c_low_power = c_low_power,
+		.front_a_limited = front_a_limited
+	};
+	/*
+	 * Assume illegal states with no headroom cannot be reached in the first
+	 * place.
+	 */
+	klee_assume(compute_headroom(&states) >= 0);
+
+	update_port_state(&states);
+
+	/*
+	 * Plug something into an unused port and ensure we still have
+	 * non-negative headroom.
+	 */
+	uint8_t enable_port = (uint8_t)klee_range(0, 8, "enable_port");
+	uint8_t enable_mask = 1 << enable_port;
+
+	klee_assume((states.bitfield & enable_mask) == 0);
+	states.bitfield |= enable_mask;
+	klee_assert(compute_headroom(&states) >= 0);
+
+	return 0;
+}