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 origi
Our apologies if you have received multiple copies.
SECOND CALL FOR PAPERS AND WORKSHOP PROPOSALS
12th International Conference on
Software Engineering and Formal Methods
(SEFM 2014)
http://sefm2014.inria.fr/
Grenoble, France
(( Apologies for multiple copies ))
** FINAL CALL FOR PAPERS **
- Note deadline extension -
IJCAR 2014 - The 7th International Joint Conference on Automated Reasoning
Vienna, Austria, July 19-22, 2014
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 p
