From: lkcl Date: Fri, 17 Jul 2020 19:12:57 +0000 (+0100) Subject: (no commit message) X-Git-Tag: convert-csv-opcode-to-binary~2340 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f805910f235a19015bdb20db66d60e55359ebbbe;p=libreriscv.git --- diff --git a/Documentation/notes_on_formal_proofs.mdwn b/Documentation/notes_on_formal_proofs.mdwn index 01966058c..1186868c8 100644 --- a/Documentation/notes_on_formal_proofs.mdwn +++ b/Documentation/notes_on_formal_proofs.mdwn @@ -67,14 +67,15 @@ so I won't spend any more time on this. `CompALUOpSubset` is, ultimately, an `nmigen` [record](https://github.com/nmigen/nmigen/blob/master/nmigen/hdl/rec.py#L89) which contains a number of fields related to telling the pipeline stage -*what to do*. (Hence the *Op* in the class name.) I won't disclose +*what to do* and providing all the information it needs in order *to* +"do". (Hence the *Op* in the class name.) I won't disclose the fields here, because they're liable to change at any time. What is important to know here is that this record exists for one purpose: to ensure that when the interface to the ALU pipeline stage changes for any reason, *all* consumers of that interface are updated consistently. Because this is a record, its fields may be introspected. This happens -frequently; it is usually the case that an Op-type record is passed +frequently: it is the case that an Op-type record is passed unchanged from stage to stage. However, `nmigen` does not seem to support testing records for equality in formal assertions. (lkcl: it does) To express this constraint without needing to update a pile of use-sites