Hi Oliver,
Yes, the approach of the former ARMv7 model doesn’t translate naturally to the
new L3 setting. That is, it’s not possible to call co-processor “hook”
functions within the L3 specification itself.
I can think of two options:
1. If you want to model a specific co-processor then it’s probably a good idea
to specify this directly in L3. By way of an example, this is how the
floating-point co-processor is currently modelled. An “accept” function isn’t
really needed in this case. Floating-point instructions are either successfully
decoded and run, or they decode as “undefined” and a processor “undefined
instruction” exception occurs.
2. If you’re after something more generic (similar to before) then the best
approach is probably to extend the exiting model within HOL. That is, you can
augment the L3 exported “next state” function
|- ∀state.
Next state =
(let (v,s) = Fetch state
in
ITAdvance () (let (v,s) = Decode v s in SND (Run v s))):
with custom HOL4 code. As such you'd augment the state-space with additional
co-processor components/hooks (as you see fit). You’d end up with something
roughly like:
CP-Next (cp-state, state) =
if is-co-processor-instruction (FST (Fetch state)) then
do-something (cp-state, state)
else
(cp-state, Next state)
Hope this helps.
Anthony
On 13 Jan 2014, at 18:13, Oliver Schwarz <[email protected]> wrote:
> Dear L3-experts,
>
> in the former model of ARMv7, coprocessors were defined in a placeholder
> fashion like
>
> val _ = Hol_datatype `Coprocessors =
> <| state : coproc_state;
> accept : CPinstruction -> coproc_state -> (bool # coproc_state);
> .
> .
> .
>
> where the behavior of accept was originally not defined, but could be
> specified later on by assigning/initializing an implementation my_accept
> to state.coprocessors.accept.
>
> I would like to achieve something similar in L3.
> However, from what I understand from the documentation and some
> experiments, assigning some function/operation to a record member is not
> possible in L3, since the language is first order. Did I get that right?
>
> One workaround I can think of is to do the definition (of Coprocessors,
> possibly even of my_accept) in L3, but initialize/assign later in HOL4.
>
> Now:
> 1. Do you see any reason why I should not use that workaround?
> 2. Is there something else I can consider?
>
>
> I hope I was able to make my chaotic thoughts clear and am thankful for
> any help.
> Thanks!
>
> Oliver
>
>
> ------------------------------------------------------------------------------
> CenturyLink Cloud: The Leader in Enterprise Cloud Services.
> Learn Why More Businesses Are Choosing CenturyLink Cloud For
> Critical Workloads, Development Environments & Everything In Between.
> Get a Quote or Start a Free Trial Today.
> http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
CenturyLink Cloud: The Leader in Enterprise Cloud Services.
Learn Why More Businesses Are Choosing CenturyLink Cloud For
Critical Workloads, Development Environments & Everything In Between.
Get a Quote or Start a Free Trial Today.
http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
