diff options
| -rw-r--r-- | src/hls/RTLBlock.v | 5 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 3 |
2 files changed, 6 insertions, 2 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index e5ce9a7..117d21b 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -76,7 +76,7 @@ Definition successors_instr (i : control_flow_inst) : list node := | RBgoto n => n :: nil end. -Definition genv := Genv.t fundef unit. +(* Definition genv := Genv.t fundef unit. Definition regset := Regmap.t val. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := @@ -165,3 +165,6 @@ Inductive step : state -> trace -> state -> Prop := step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C) E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N) . + +End RELSEM. +*) diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 038ae32..0e94fd5 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -76,7 +76,7 @@ Definition successors_instr (i : control_flow_inst) : list node := | RPgoto n => n :: nil end. -Inductive state : Type := +(*Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r current function *) @@ -96,3 +96,4 @@ Inductive state : Type := (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. +*) |