diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 13:02:04 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 13:02:04 +0000 |
| commit | 00ebd4125f46e4b21e18f907fc0498c078f38e95 (patch) | |
| tree | 03eb9d901aaa177ce2ef21e277121ce15e68bc87 /src/hls/RTLPar.v | |
| parent | db2bdf8563bbb89fc953b758f53d8861dcf5c831 (diff) | |
| download | vericert-00ebd4125f46e4b21e18f907fc0498c078f38e95.tar.gz vericert-00ebd4125f46e4b21e18f907fc0498c078f38e95.zip | |
Fix RTLPar to use instr list list list
Diffstat (limited to 'src/hls/RTLPar.v')
| -rw-r--r-- | src/hls/RTLPar.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index be9ff22..2e78d36 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -30,7 +30,7 @@ Require Import compcert.verilog.Op. Require Import vericert.hls.RTLBlockInstr. -Definition bb := list (list instr). +Definition bb := list (list (list instr)). Definition bblock := @bblock bb. Definition code := @code bb. @@ -56,11 +56,22 @@ Section RELSEM. forall state sp, step_instr_list sp state nil state. + Inductive step_instr_seq (sp : val) + : instr_state -> list (list instr) -> instr_state -> Prop := + | exec_instr_seq_cons: + forall state i state' state'' instrs, + step_instr_list sp state i state' -> + step_instr_seq sp state' instrs state'' -> + step_instr_seq sp state (i :: instrs) state'' + | exec_instr_seq_nil: + forall state, + step_instr_seq sp state nil state. + Inductive step_instr_block (sp : val) : instr_state -> bb -> instr_state -> Prop := | exec_instr_block_cons: forall state i state' state'' instrs, - step_instr_list sp state i state' -> + step_instr_seq sp state i state' -> step_instr_block sp state' instrs state'' -> step_instr_block sp state (i :: instrs) state'' | exec_instr_block_nil: @@ -113,7 +124,7 @@ Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) := - let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in + let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in max_reg_cfi max_body bb.(bb_exit). Definition max_reg_function (f: function) := |