From 741d254d2d697cd9cd9da2edb9cd49462695092f Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 3 May 2021 17:29:20 +0100 Subject: Add externctrl props to HTLgen's st_prop --- src/hls/HTLgen.v | 85 +++++++++++++++++++++++++++++--------------------------- 1 file changed, 44 insertions(+), 41 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index ea6c545..68080e2 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -66,17 +66,18 @@ Module HTLState <: State. Definition st := state. Inductive st_incr: state -> state -> Prop := - state_incr_intro: + | state_incr_intro: forall (s1 s2: state), - st_st s1 = st_st s2 -> - Ple s1.(st_freshreg) s2.(st_freshreg) -> - Ple s1.(st_freshstate) s2.(st_freshstate) -> - (forall n, - s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> - (forall n, - s1.(st_controllogic)!n = None - \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> - st_incr s1 s2. + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, s1.(st_datapath)!n = None \/ + s2.(st_datapath)!n = s1.(st_datapath)!n) -> + (forall n, s1.(st_controllogic)!n = None \/ + s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + (forall n, s1.(st_externctrl)!n = None \/ + s2.(st_externctrl)!n = s1.(st_externctrl)!n) -> + st_incr s1 s2. Hint Constructors st_incr : htlh. Definition st_prop := st_incr. @@ -87,9 +88,9 @@ Module HTLState <: State. Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. Proof. - intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence. - - destruct H4 with n; destruct H8 with n; intuition congruence. - - destruct H5 with n; destruct H9 with n; intuition congruence. + intros. inv H. inv H0. + apply state_incr_intro; eauto using Ple_trans; intros; try congruence; + specialize_all n; intuition congruence. Qed. End HTLState. @@ -136,21 +137,20 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -(** Used for discharging the st_incr proof in simple operations *) -Ltac htl_st_tac := constructor; intros; simpl; auto with htlh. +Definition check_unmapped_externctrl: + forall (s: state) (n: reg), { s.(st_externctrl)!n = None } + { True }. +Proof. + intros. case (s.(st_externctrl)!n); tauto. +Defined. -(** Used for discharging the st_incr proof in operations that add instructions. - Assumes that check_empty_node_(datapath|controllogic) has been used and matched - on. *) -Ltac add_instr_st_tac := - htl_st_tac; +(** Used for discharging the st_incr proof in simple operations *) +Local Ltac st_tac := + constructor; intros; simpl; auto with htlh; match goal with - | [ STM : (st_datapath ?s) ! ?n = None, TRANS : (st_controllogic ?s) ! ?n = None, n0 : positive |- _] => - destruct (peq n n0) + | [ H : (?map ?s) ! ?n = None, n' : positive |- _] => destruct (peq n n') end; subst; auto with htlh. - Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => OK tt (mkstate (st_st s) @@ -160,7 +160,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := (st_arrdecls s) (st_externctrl s) (st_datapath s) - (st_controllogic s)) ltac:(htl_st_tac). + (st_controllogic s)) ltac:(st_tac). Definition create_reg (i : option io) (sz : nat) : mon reg := fun s => let r := s.(st_freshreg) in @@ -172,19 +172,22 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := (st_arrdecls s) (st_externctrl s) (st_datapath s) - (st_controllogic s)) ltac:(htl_st_tac). + (st_controllogic s)) ltac:(st_tac). Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := do r <- create_reg None (controlsignal_sz ctrl); - fun s => OK r (mkstate - s.(st_st) - (st_freshreg s) - (st_freshstate s) - (st_scldecls s) - (st_arrdecls s) - (AssocMap.set r (othermod, ctrl) (st_externctrl s)) - (st_datapath s) - (st_controllogic s)) ltac:(htl_st_tac). + fun s => match check_unmapped_externctrl s r with + | left CTRL => OK r (mkstate + (st_st s) + (st_freshreg s) + (st_freshstate s) + (st_scldecls s) + (st_arrdecls s) + (AssocMap.set r (othermod, ctrl) (st_externctrl s)) + (st_datapath s) + (st_controllogic s)) ltac:(st_tac) + | right CTRL => Error (Errors.msg "HTL.map_externctrl") + end. Definition create_state : mon node := fun s => let r := s.(st_freshstate) in @@ -196,7 +199,7 @@ Definition create_state : mon node := (st_arrdecls s) (st_externctrl s) (st_datapath s) - (st_controllogic s)) ltac:(htl_st_tac). + (st_controllogic s)) ltac:(st_tac). Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with @@ -209,7 +212,7 @@ Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := s.(st_arrdecls) (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) ltac:(add_instr_st_tac) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) ltac:(st_tac) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -224,7 +227,7 @@ Definition add_instr_wait (wait_reg : reg) (n : node) (n' : node) (st : datapath s.(st_arrdecls) (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_wait (st_st s) wait_reg n') s.(st_controllogic))) ltac:(add_instr_st_tac) + (AssocMap.set n (state_wait (st_st s) wait_reg n') s.(st_controllogic))) ltac:(st_tac) | _, _ => Error (Errors.msg "HTL.add_instr_wait") end. @@ -239,7 +242,7 @@ Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := s.(st_arrdecls) (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))) ltac:(add_instr_st_tac) + (AssocMap.set n Vskip s.(st_controllogic))) ltac:(st_tac) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -254,7 +257,7 @@ Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := s.(st_arrdecls) (st_externctrl s) (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))) ltac:(add_instr_st_tac) + (AssocMap.set n st s.(st_controllogic))) ltac:(st_tac) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -401,7 +404,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := s.(st_arrdecls) (st_externctrl s) (AssocMap.set n Vskip (st_datapath s)) - (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) ltac:(add_instr_st_tac) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) ltac:(st_tac) | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") end. @@ -538,7 +541,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_externctrl s) (st_datapath s) - (st_controllogic s)) ltac:(htl_st_tac). + (st_controllogic s)) ltac:(st_tac). Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz