From e1508c94684718a906440fe82344be73e63956a1 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 20 Sep 2021 13:56:25 +0100 Subject: [WIP] Reset finish register after returning --- src/hls/HTL.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src/hls/HTL.v') 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 := -- cgit