Add descriptions of assert and assume to PSA specification

p4-16/psa/PSA.mdk

@@ -2648,6 +2648,26 @@ ingress ports of packets that have not been seen before.
 ```
 
 
+## Error checking extern functions `assert` and `assume` {#sec-assert-assume}
+
+The extern function `assert` is provided for similar reasons as it is
+present in languages like C: to enable developers to check whether
+conditions that they believe should be true, are actually true,
+signaling an error if they are false.
+
+```
+[INCLUDE=psa.p4:assert_extern_function]
+```
+
+The extern function `assume` is similar to `assert`, but some
+development tools may treat it slightly differently than `assert`,
+e.g. formal verification tools, or tools that automatically generate
+test cases.
+
+```
+[INCLUDE=psa.p4:assume_extern_function]
+```
+
 
 # Atomicity of control plane API operations {#sec-atomicity-of-control-plane-api-operations}
 
@@ -3616,7 +3636,8 @@ provided in sub-sections below.
   `psa.p4` (all changes in file `psa.p4`).
 + Replace `@noWarnUnused` with standard `@noWarn("unused")`
   annotations in `psa.p4` (all changes in file `psa.p4`).
-+ Add `assert` and `assume` extern functions (all changes in file `psa.p4`).
++ Add `assert` and `assume` extern functions (section
+  [#sec-assert-assume]).
 
 TODO: The list above is complete up to the following commit.  Any
 later commits should be considered for describing as additional

p4-16/psa/psa.p4

@@ -337,6 +337,7 @@ extern bool psa_recirculate(in psa_egress_output_metadata_t istd,
                             in psa_egress_deparser_input_metadata_t edstd);
 
 
+// BEGIN:assert_extern_function
 /***
  * Calling assert when the argument is true has no effect, except any
  * effect that might occur due to evaluation of the argument (but see
@@ -350,6 +351,10 @@ extern bool psa_recirculate(in psa_egress_output_metadata_t istd,
  * name and line number of the assert statement to be printed, and
  * then the simple_switch_psa process exits.
  *
+ * It is expected that many hardware targets will compile PSA programs
+ * as if all calls to `assert` were not present.  Consult your target
+ * device's documentation for details.
+ *
  * If you use a P4 compiler whose front end is based on the open
  * source p4c front end, then providing the --ndebug command line
  * option to p4c causes the compiled program to behave as if all
@@ -365,13 +370,19 @@ extern bool psa_recirculate(in psa_egress_output_metadata_t istd,
  * same way when assert statements are removed.
  */
 extern void assert(in bool check);
+// END:assert_extern_function
 
+// BEGIN:assume_extern_function
 /***
  * For the purposes of compiling and executing P4 programs on a target
  * device, assert and assume are identical, including the use of the
  * --ndebug option to compilers based on the open source p4c front end
  * to elide them.  See documentation for assert.
  *
+ * It is expected that many hardware targets will compile PSA programs
+ * as if all calls to `assume` were not present.  Consult your target
+ * device's documentation for details.
+ *
  * The reason that assume exists as a separate function from assert is
  * because they are expected to be used differently by formal
  * verification tools.  For some formal tools, the goal is to try to
@@ -401,6 +412,7 @@ extern void assert(in bool check);
  * is likely that your assumption was wrong, and should be reexamined.
  */
 extern void assume(in bool check);
+// END:assume_extern_function
 
 // BEGIN:Match_kinds
 match_kind {