diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:02:14 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:02:14 +0100 |
| commit | 87fba8b56e25130519f7b4bea4b9887bc14ec31f (patch) | |
| tree | 10a742e88804c8325dd51ede561bf828fd4af458 | |
| parent | f7616136f1a2f3561500b1c28219ae725c4cda17 (diff) | |
| download | vericert-87fba8b56e25130519f7b4bea4b9887bc14ec31f.tar.gz vericert-87fba8b56e25130519f7b4bea4b9887bc14ec31f.zip | |
Add "join state is <=Int.max_unsigned" to HTLgenspec
| -rw-r--r-- | src/hls/HTLgen.v | 20 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 3 |
2 files changed, 13 insertions, 10 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 5babea0..ca202a2 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -195,15 +195,17 @@ Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := Definition create_state : mon node := fun s => let r := s.(st_freshstate) in - OK r (mkstate - s.(st_st) - (st_freshreg s) - (Pos.succ (st_freshstate s)) - (st_scldecls s) - (st_arrdecls s) - (st_externctrl s) - (st_datapath s) - (st_controllogic s)) ltac:(st_tac). + if Z.leb (Z.pos s.(st_freshstate)) Integers.Int.max_unsigned + then OK r (mkstate + s.(st_st) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_externctrl s) + (st_datapath s) + (st_controllogic s)) ltac:(st_tac) + else Error (Errors.msg "HTL.create_state"). 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 diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 0c15f53..7480231 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -103,7 +103,7 @@ Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datap (forall n arg, List.nth_error args n = Some arg -> exists r, In (r, arg) (List.combine fn_params args) /\ externctrl ! r = Some (fn, ctrl_param n)) /\ - + Z.pos pc2 <= Int.max_unsigned /\ stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ trans!pc = Some (state_goto st pc2) /\ stmnts!pc2 = Some (join fn_return fn_rst dst) /\ @@ -393,6 +393,7 @@ Proof. * intros. destruct (map_externctrl_params_spec _ _ _ _ _ _ _ _ EQ1 ltac:(eauto)) as [param [? ?]]. exists param; crush; trans_step s3 s'. + * monadInv EQ2. crush. + (* Icond *) tr_code_simple_tac. + (* Ireturn *) inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. |