From f805910f235a19015bdb20db66d60e55359ebbbe Mon Sep 17 00:00:00 2001 From: lkcl Date: Fri, 17 Jul 2020 20:12:57 +0100 Subject: [PATCH] --- Documentation/notes_on_formal_proofs.mdwn | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.30.2