Right. You might write
Implementation(out) ⇔
∃cout.
counter cout ∧ filter cout out
where
counter cout ⇔ ∀t. cout t = t
filter inp out ⇔ ∀t. out(t) ⇔ prime(inp(t))
as your description of the implementation (where the counter component is
indeed visible but "hidden" behind an existentially quantifier internal wire).
This is a slightly weird implementation because the internal cout wire carries
natural numbers at every tick and is thus "infinitely wide". By contrast, the
out wire carries more hardware-plausible Booleans at every tick.
Your spec might get to be the simpler
Specification(out) ⇔ ∀t. out(t) ⇔ prime(t)
And this hides the internal counter/register entirely.
Michael
On 24/4/18, 16:23, "Konrad Slind" <konrad.sl...@gmail.com> wrote:
In the way Mike and colleagues modelled hardware, a device is modelled
as a predicate over the external wires (ports) of the device.
Information hiding is achieved by existential quantification
(relational composition). The basics of this are laid out in
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf
There is a sequential circuit example in that tech. report, which may help.
Konrad.
On Mon, Apr 23, 2018 at 9:09 AM, Lawrence Paulson <l...@cam.ac.uk> wrote:
> Somebody asked me, how do we represent the state of a sequential device
in HOL? And I am not quite sure. Mike himself wrote that it is simply about
incorporating time into the model, so that if we have a counter then we can
describe it by C(t+1) = C(t)+1, where C is its (visible) output and t
represents time.
>
> But what if we have a primitive that doesn't expose its full state to the
outside? Imagine a device that contains a counter that increments with every
clock tick, but the counter value is hidden and the output is only a single bit
to tell us whether the value of the counter is a prime number or not. Surely in
such a case the counter itself would have to be visible in the formalisation
even if no device was allowed to connect to it?
>
> Larry Paulson
>
>
>
>
>
------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
