diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-20 13:56:25 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-20 13:56:25 +0100 |
| commit | e1508c94684718a906440fe82344be73e63956a1 (patch) | |
| tree | 7f2c03fb01d33362685dafb713aee82a5699cbdc /src/hls/HTL.v | |
| parent | a56c0bd55f921f85ddbb8b02c2f4c7ac89bf3aaf (diff) | |
| download | vericert-e1508c94684718a906440fe82344be73e63956a1.tar.gz vericert-e1508c94684718a906440fe82344be73e63956a1.zip | |
[WIP] Reset finish register after returning
Diffstat (limited to 'src/hls/HTL.v')
| -rw-r--r-- | src/hls/HTL.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 1a23ef5..ce7d37e 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -308,7 +308,16 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Returnstate (Stackframe callerid caller pc asr asa :: sf) callee_id i) Events.E0 (State sf callerid caller pc (asr # mst <- (posToValue pc) # callee_finish <- (ZToValue 1) # callee_return <- i) - asa). + asa) +| step_finish_reset : + forall g sf mid mid' m st asr asa fin, + asr ! fin = Some (ZToValue 1) -> + (mod_externctrl m) ! fin = Some (mid', ctrl_finish) -> + step g + (State sf mid m st asr asa) Events.E0 + (State sf mid m st (asr # fin <- (ZToValue 0)) asa). + + Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := |