CPC G06F 9/44589 (2013.01) [G06F 8/51 (2013.01); G06F 11/3604 (2013.01); G06F 11/3608 (2013.01); G06F 11/3636 (2013.01); H04L 45/745 (2013.01)] | 18 Claims |
1. A non-transitory machine-readable medium storing a verification program for execution by a set of processing units, the verification program for verifying the correctness of a forwarding-element program to be executed by a control-plane circuit to configure a data-plane circuit of a forwarding element to forward data messages, the forwarding-element program specifying at least one element that is populated during execution by a control plane circuit, the verification program comprising a set of instructions that when executed by the set of processing units results in performance of operations comprising:
receiving the forwarding-element program;
annotating the forwarding-element program to reflect assumptions regarding control-plane behavior;
translating the forwarding-element program and annotations into a different programming language that incorporates non-deterministic choice based on the assumptions regarding control plane behavior; and
using the translated program to verify the correctness of the forwarding-element program and assumptions regarding the control plane behavior;
wherein:
the data-plane circuit comprises a plurality of programmable packet processing stages that comprise match-action tables that are to be configured by the control-plane circuit for use in forwarding the data messages; and
the using the translated program to verify the correctness of the forwarding-element program and the assumptions regarding the control-plane behavior comprises verifying whether entries in the match-action tables depend on each other.
|