Skip to content

Commit 91f8741

Browse files
dhower-qcdhower-qc
committed
docs: document schema conditions and idl implications
1 parent 60f2054 commit 91f8741

File tree

2 files changed

+273
-0
lines changed

2 files changed

+273
-0
lines changed

‎doc/idl.adoc

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -512,6 +512,32 @@ The result of a binary operation is signed if both operands are signed; otherwis
512512
`c` must be boolean, and `t` and `f` must be identical types.
513513
|===
514514

515+
=== Implications
516+
517+
Implications are used to specify dependencies that must hold among data.
518+
Implications cannot appear in general IDL code, and are used in specific contexts, for example when expression link:schema/conditions.adoc#_generic_constraints[generic constraints] in RISC-V Unified Database.
519+
520+
An implication takes the form:
521+
522+
[source,idl]
523+
----
524+
ANTECEDENT -> CONSEQUENT
525+
----
526+
527+
The antecedent and consequent can be any expression with a boolean type.
528+
529+
The implication passes whenever (1) the antecedent is false or (2) both the antecedent and consequent are true.
530+
531+
For example:
532+
533+
[source,idl]
534+
----
535+
false -> true; # passes
536+
false -> false; # passes
537+
true -> true; # passes
538+
true -> false; # fails
539+
----
540+
515541
== Variables and constants
516542

517543
=== Mutable variables

‎doc/schema/conditions.adoc

Lines changed: 247 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,247 @@
1+
// Copyright (c) Qualcomm Technologies, Inc. and/or its subsidiaries.
2+
// SPDX-License-Identifier: CC-BY-4.0
3+
4+
= Expressing Conditions in UDB Data
5+
6+
There are many instances where there is a conditional relation among data in UDB.
7+
For example:
8+
9+
* the `Zfinx` extension is only allowed if the `F` extension is not implemented.
10+
* the `C` extension only implies the `Zcd` extension if the `D` extension is also implemented.
11+
* the `MTVEC_BASE_ALIGNMENT_DIRECT` parameter only applies when `MTVEC_MODES` indicates support for 'direct'.
12+
* ... and many more
13+
14+
Conditions are consistently represented using a common subschema throughout UDB, regardless of the context that they appear.
15+
16+
== Condition Tests
17+
18+
There are three types of things that can be tested by a condition:
19+
20+
* an *extension requirement*
21+
** For example, extension `Sm`, version `>= 1.12`
22+
* a *parameter requirement*
23+
** For example, `MXLEN` equals `32`
24+
* a *generic constraint*
25+
** For example, if `MXLEN` is `32`, then `Sv39` must not be implemented
26+
27+
The three test types can be combined arbitrarily using link:#_boolean_operators[boolean operators].
28+
29+
=== Extension Requirements
30+
31+
An extension requirement is identified by the key `extension`.
32+
It expects an extension `name` and an optional `version`.
33+
If no `version` is given, then it defaults to all versions (`>= 0`).
34+
35+
The `version` is a list of range specifiers, using the following operators:
36+
37+
|===
38+
| op | Meaning | Example
39+
40+
| `=` | Exactly equals | `= 1.0`
41+
| `>` | Greater than | `> 1.0`
42+
| `<` | Less than | `< 1.0`
43+
| `>=` | Greater than or equal | `>= 1.0`
44+
| `<=` | Less than or equal | `<= 1.0`
45+
| '~>' | Compatible with | `~> 1.0`
46+
|===
47+
48+
The "compatible with" operator will accept any version that is greater than or equal to the target and that has not been marked as a breaking version change in the database.
49+
Note that RISC-V does not follow semantic versioning, so `2.0` may be compatible with `1.0` for a given extension as long as `2.0` (or any version between `1.0` and `2.0`) is not marked as a breaking version.
50+
51+
For example:
52+
53+
[source,yaml]
54+
----
55+
# require C, version >= 0
56+
extension:
57+
name: C
58+
----
59+
60+
[source,yaml]
61+
----
62+
# require D, version == 1.0
63+
extension:
64+
name: D
65+
version: = 1.0
66+
----
67+
68+
[source,yaml]
69+
----
70+
# require D, version _compatible with_ 1.0
71+
extension:
72+
name: D
73+
version: ~> 1.0
74+
----
75+
76+
[source,yaml]
77+
----
78+
# require D, version greater than or equal to 1.0 and less than 2.0
79+
extension:
80+
name: D
81+
version: [">= 1.0", "< 2.0"]
82+
----
83+
84+
Extension requirements can also take logic expression of multiple requrements using the `allOf`, `anyOf`, `noneOf`, or `not` operators. See link:#_boolean_operators[Boolean Operators] and <<Examples>>.
85+
86+
=== Parameter Requirements
87+
88+
A parameter requirement is identified by the key `param`.
89+
It expects a parameter `name`, a single comparison, and a `reason` description.
90+
91+
The comparison is one of:
92+
93+
|===
94+
| Key | Meaning | Example
95+
96+
| `equal` | Parameter value equals | `equal: 5`, `equal: "string value"`
97+
| `not_equal` | Parameter value is not equal to | `not_equal: 5`, `not_equal: "string value"`
98+
| `less_than` | Parameter value is less than | `less_than`: 5
99+
| `greater_than` | Parameter value is greater than | `greater_than`: 5
100+
| `less_than_or_equal` | Parameter value is less than or equal to | `less_than`: 5
101+
| `greater_than_or_equal` | Parameter value is greater than or equal to | `greater_than`: 5
102+
| `includes` | Array parameter includes a value | `includes: 5`, `includes: "string value"`
103+
|===
104+
105+
For example:
106+
107+
[source,yaml]
108+
----
109+
param:
110+
name: MXLEN
111+
equal: 32
112+
reason: Extension is only defined in RV32
113+
----
114+
115+
[source,yaml]
116+
----
117+
param:
118+
name: MTVEC_MODES
119+
includes: 0
120+
reason: Only relevant when direct mode is supported
121+
----
122+
123+
Like <<Extension Requirements>>, parameter requirements can be combined aribtrarily using boolean logic operations. See link:#_boolean_operators[Boolean Operators] and <<Examples>>
124+
125+
=== Generic Constraints
126+
127+
Generic constraints provide an escape hatch when a condition is difficult to express when using link:#_extension_requirements[Extension Requirements] or link:#_parameter_requirements[Parameter Requirements].
128+
A generic constraint is an IDL function containing one or more link:../idl.adoc#implications[implications].
129+
The constraint holds if all the implications are true.
130+
The constraint function does not return a value.
131+
132+
All global functions (for example, `implemented?(...)`) and parameters are in scope for the constraint function.
133+
134+
For example:
135+
136+
[source,yaml]
137+
----
138+
constraint:
139+
idl(): |
140+
implemented?(ExtensionName:Sv32) -> SV32X4_TRANSLATION;
141+
reason:
142+
`Shgatpa` mandates that or each supported virtual memory scheme SvNN supported in
143+
`satp`, the corresponding `hgatp` SvNNx4 mode must be supported.
144+
----
145+
146+
[source,yaml]
147+
----
148+
constraint:
149+
idl(): |
150+
for (U32 i = 3; i < 32; i++){
151+
HPM_COUNTER_EN[i] -> HCOUNTENABLE_EN[i];
152+
}
153+
reason:
154+
Shcounterenw requires that all non-read-only-0 counters can enabled with hcounteren.
155+
----
156+
157+
[reftext="boolean operators"]
158+
== Boolean Operators
159+
160+
UDB adopts the same schema used by link:https://json-schema.org[JSON Schema] for boolean logic.
161+
The logic can be applied either at the top level of a condition (before any `extension`, `param`, or `constraint` keys) or within a particular type.
162+
163+
The following operators are supported:
164+
165+
|===
166+
| Op | Meaning | Example
167+
168+
| `allOf` | Logical AND | `allOf: [ { name: C }, { name: D} ]`
169+
| `anyOf` | Logical OR | `anyOf: [ { name: C }, { name: D} ]`
170+
| `noneOf` | Logical NOR | `noneOf: [ { name: C }, { name: D} ]`
171+
| `not` | Logical NOT | `not: { name: C }`
172+
| `if`, `then` | Logical implicaiton | `if: { name: C }, then: { name: D }`
173+
|===
174+
175+
For example:
176+
177+
[source,yaml]
178+
----
179+
extension:
180+
allOf:
181+
- name: C
182+
- name: D
183+
----
184+
185+
[source,yaml]
186+
----
187+
allOf:
188+
- extension:
189+
name: C
190+
- param:
191+
name: MXLEN
192+
equal: 32
193+
reason: Only applies with RV32
194+
----
195+
196+
[source,yaml]
197+
----
198+
if:
199+
extension:
200+
name: F
201+
version: ~> 2.2
202+
then:
203+
name: Zcf
204+
version: = 1.0.0
205+
----
206+
207+
== Examples
208+
209+
The following are real examples from the database:
210+
211+
.mstatus CSR is defined by the Sm extension
212+
[source,yaml]
213+
----
214+
# mstatus.yaml
215+
definedBy:
216+
extension:
217+
name: Sm
218+
----
219+
220+
.C implies Zcf/d only if F/D are implemented
221+
[source,yaml]
222+
----
223+
# C.yaml
224+
versions:
225+
- version: "2.0.0"
226+
state: ratified
227+
ratification_date: 2019-12
228+
requires:
229+
extension:
230+
allOf:
231+
- name: Zca
232+
version: = 1.0.0
233+
- if:
234+
extension:
235+
name: F
236+
version: ~> 2.2
237+
then:
238+
name: Zcf
239+
version: = 1.0.0
240+
- if:
241+
extension:
242+
name: D
243+
version: ~> 2.2
244+
then:
245+
name: Zcd
246+
version: = 1.0.0
247+
----

0 commit comments

Comments
 (0)