Make DVIT property normative

zicondops.adoc

@@ -78,7 +78,8 @@ Encoding::
 
 Description::
 This instruction behaves as if there is a conditional branch dependent on _rs2_ being equal to zero, wherein it branches to code that writes a 0 into _rd_ when the equivalence is true, and otherwise falls through to code that moves _rs1_ into _rd_.
-Accordingly, the syntactic dependency on _rs1_ is only propagated when the condition is false. +
+Accordingly, the syntactic dependency on _rs1_ is only propagated when the condition is false.
+Furthermore, this instruction's timing is independent of the data value of _rs1_ if the Zkt extension is implemented. +
 
 In effect, if the value of register _rs2_ is zero, place 0 (zero) into the register _rd_; otherwise, place the value of register _rs1_ into _rd_.
 
@@ -87,8 +88,6 @@ In effect, if the value of register _rs2_ is zero, place 0 (zero) into the regis
 These branch-based semantics do not prevent implementing this instruction as a simple select (e.g., "(rs2==0) ? 0 : rs1").
 Instead, they allow for more sophisticated implementations where a zero result can be returned when the condition (rs2==0) is true without waiting for _rs1_ to be available.
 Furthermore, implementations can predict the condition just as they might for branches.
-
-As a consequence of this instruction's equivalence to `mv rd, rs1` when _rs2_ is nonzero, this instruction's timing is independent of the data value of _rs1_ if the Zkt extension is implemented.
 ====
 
 SAIL code::
@@ -137,7 +136,8 @@ Encoding::
 
 Description::
 This instruction behaves as if there is a conditional branch dependent on _rs2_ being not equal to zero, wherein it branches to code that writes a 0 into _rd_ when the equivalence is true, and otherwise falls through to code that moves _rs1_ into _rd_.
-Accordingly, the syntactic dependency on _rs1_ is only propagated when the condition is false. +
+Accordingly, the syntactic dependency on _rs1_ is only propagated when the condition is false.
+Furthermore, this instruction's timing is independent of the data value of _rs1_ if the Zkt extension is implemented. +
 
 In effect, if the value of register _rs2_ is non-zero, place 0 (zero) into the register _rd_; otherwise, place the value of register _rs1_ into _rd_.
 
@@ -146,8 +146,6 @@ In effect, if the value of register _rs2_ is non-zero, place 0 (zero) into the r
 These branch-based semantics do not prevent implementing this instruction as a simple select (e.g., "(rs2!=0) ? 0 : rs1").
 Instead, they allow for more sophisticated implementations where a zero result can be returned when the condition (rs2!=0) is true without waiting for _rs1_ to be available.
 Furthermore, implementations can predict the condition just as they might for branches.
-
-As a consequence of this instruction's equivalence to `mv rd, rs1` when _rs2_ is zero, this instruction's timing is independent of the data value of _rs1_ if the Zkt extension is implemented.
 ====
 
 SAIL code::