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>

1 files changed, 40 insertions, 0 deletions

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;
+}