Skip to content

Commit 6928ad8

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

File tree

2 files changed

+275
-0
lines changed

2 files changed

+275
-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: 249 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,249 @@
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 <<bool_ops,boolean operators>>.
28+
29+
[#ext_reqs]
30+
=== Extension Requirements
31+
32+
An extension requirement is identified by the key `extension`.
33+
It expects an extension `name` and an optional `version`.
34+
If no `version` is given, then it defaults to all versions (`>= 0`).
35+
36+
The `version` is a list of range specifiers, using the following operators:
37+
38+
|===
39+
| op | Meaning | Example
40+
41+
| `=` | Exactly equals | `= 1.0`
42+
| `>` | Greater than | `> 1.0`
43+
| `<` | Less than | `< 1.0`
44+
| `>=` | Greater than or equal | `>= 1.0`
45+
| `<=` | Less than or equal | `<= 1.0`
46+
| '~>' | Compatible with | `~> 1.0`
47+
|===
48+
49+
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.
50+
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.
51+
52+
For example:
53+
54+
[source,yaml]
55+
----
56+
# require C, version >= 0
57+
extension:
58+
name: C
59+
----
60+
61+
[source,yaml]
62+
----
63+
# require D, version == 1.0
64+
extension:
65+
name: D
66+
version: = 1.0
67+
----
68+
69+
[source,yaml]
70+
----
71+
# require D, version _compatible with_ 1.0
72+
extension:
73+
name: D
74+
version: ~> 1.0
75+
----
76+
77+
[source,yaml]
78+
----
79+
# require D, version greater than or equal to 1.0 and less than 2.0
80+
extension:
81+
name: D
82+
version: [">= 1.0", "< 2.0"]
83+
----
84+
85+
Extension requirements can also take logic expression of multiple requrements using the `allOf`, `anyOf`, `noneOf`, or `not` operators. See <<bool_ops,Boolean Operators>> and <<Examples>>.
86+
87+
[#param_reqs]
88+
=== Parameter Requirements
89+
90+
A parameter requirement is identified by the key `param`.
91+
It expects a parameter `name`, a single comparison, and a `reason` description.
92+
93+
The comparison is one of:
94+
95+
|===
96+
| Key | Meaning | Example
97+
98+
| `equal` | Parameter value equals | `equal: 5`, `equal: "string value"`
99+
| `not_equal` | Parameter value is not equal to | `not_equal: 5`, `not_equal: "string value"`
100+
| `less_than` | Parameter value is less than | `less_than`: 5
101+
| `greater_than` | Parameter value is greater than | `greater_than`: 5
102+
| `less_than_or_equal` | Parameter value is less than or equal to | `less_than`: 5
103+
| `greater_than_or_equal` | Parameter value is greater than or equal to | `greater_than`: 5
104+
| `includes` | Array parameter includes a value | `includes: 5`, `includes: "string value"`
105+
|===
106+
107+
For example:
108+
109+
[source,yaml]
110+
----
111+
param:
112+
name: MXLEN
113+
equal: 32
114+
reason: Extension is only defined in RV32
115+
----
116+
117+
[source,yaml]
118+
----
119+
param:
120+
name: MTVEC_MODES
121+
includes: 0
122+
reason: Only relevant when direct mode is supported
123+
----
124+
125+
Like <<Extension Requirements>>, parameter requirements can be combined aribtrarily using boolean logic operations. See <<bool_ops,Boolean Operators>> and <<Examples>>
126+
127+
=== Generic Constraints
128+
129+
Generic constraints provide an escape hatch when a condition is difficult to express when using <<ext_reqs,Extension Requirements>> or <<param_reqs,Parameter Requirements>>.
130+
A generic constraint is an IDL function containing one or more link:../idl.adoc#implications[implications].
131+
The constraint holds if all the implications are true.
132+
The constraint function does not return a value.
133+
134+
All global functions (for example, `implemented?(...)`) and parameters are in scope for the constraint function.
135+
136+
For example:
137+
138+
[source,yaml]
139+
----
140+
constraint:
141+
idl(): |
142+
implemented?(ExtensionName:Sv32) -> SV32X4_TRANSLATION;
143+
reason:
144+
`Shgatpa` mandates that or each supported virtual memory scheme SvNN supported in
145+
`satp`, the corresponding `hgatp` SvNNx4 mode must be supported.
146+
----
147+
148+
[source,yaml]
149+
----
150+
constraint:
151+
idl(): |
152+
for (U32 i = 3; i < 32; i++){
153+
HPM_COUNTER_EN[i] -> HCOUNTENABLE_EN[i];
154+
}
155+
reason:
156+
Shcounterenw requires that all non-read-only-0 counters can enabled with hcounteren.
157+
----
158+
159+
[#bool_ops]
160+
== Boolean Operators
161+
162+
UDB adopts the same schema used by link:https://json-schema.org[JSON Schema] for boolean logic.
163+
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.
164+
165+
The following operators are supported:
166+
167+
|===
168+
| Op | Meaning | Example
169+
170+
| `allOf` | Logical AND | `allOf: [ { name: C }, { name: D} ]`
171+
| `anyOf` | Logical OR | `anyOf: [ { name: C }, { name: D} ]`
172+
| `noneOf` | Logical NOR | `noneOf: [ { name: C }, { name: D} ]`
173+
| `not` | Logical NOT | `not: { name: C }`
174+
| `if`, `then` | Logical implicaiton | `if: { name: C }, then: { name: D }`
175+
|===
176+
177+
For example:
178+
179+
[source,yaml]
180+
----
181+
extension:
182+
allOf:
183+
- name: C
184+
- name: D
185+
----
186+
187+
[source,yaml]
188+
----
189+
allOf:
190+
- extension:
191+
name: C
192+
- param:
193+
name: MXLEN
194+
equal: 32
195+
reason: Only applies with RV32
196+
----
197+
198+
[source,yaml]
199+
----
200+
if:
201+
extension:
202+
name: F
203+
version: ~> 2.2
204+
then:
205+
name: Zcf
206+
version: = 1.0.0
207+
----
208+
209+
== Examples
210+
211+
The following are real examples from the database:
212+
213+
.mstatus CSR is defined by the Sm extension
214+
[source,yaml]
215+
----
216+
# mstatus.yaml
217+
definedBy:
218+
extension:
219+
name: Sm
220+
----
221+
222+
.C implies Zcf/d only if F/D are implemented
223+
[source,yaml]
224+
----
225+
# C.yaml
226+
versions:
227+
- version: "2.0.0"
228+
state: ratified
229+
ratification_date: 2019-12
230+
requires:
231+
extension:
232+
allOf:
233+
- name: Zca
234+
version: = 1.0.0
235+
- if:
236+
extension:
237+
name: F
238+
version: ~> 2.2
239+
then:
240+
name: Zcf
241+
version: = 1.0.0
242+
- if:
243+
extension:
244+
name: D
245+
version: ~> 2.2
246+
then:
247+
name: Zcd
248+
version: = 1.0.0
249+
----

0 commit comments

Comments
 (0)