Define RTLPar semantics

These semantics are similar to the RTLBlock semantics, except that more
states are needed to reason about the parallel execution in multiple
cycles.

1 files changed, 0 insertions, 86 deletions

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 23aa8c2..32d7674 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -186,89 +186,3 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-(*
-
-Inductive stackframe : Type :=
-  | Stackframe:
-      forall (res: reg)            (**r where to store the result *)
-             (f: function)         (**r calling function *)
-             (sp: val)             (**r stack pointer in calling function *)
-             (pc: node)            (**r program point in calling function *)
-             (rs: regset),         (**r register state in calling function *)
-      stackframe.
-
-Inductive cont : Type :=
-  | C
-  | N.
-
-Inductive state : Type :=
-  | State:
-      forall (stack: list stackframe) (**r call stack *)
-             (f: function)            (**r current function *)
-             (sp: val)                (**r stack pointer *)
-             (pc: node)               (**r current program point in [c] *)
-             (rs: regset)             (**r register state *)
-             (m: mem)                 (**r memory state *)
-             (bblock: bblock)         (**r bblock being executed *)
-             (c : cont),
-      state
-  | Callstate:
-      forall (stack: list stackframe) (**r call stack *)
-             (f: fundef)              (**r function to call *)
-             (args: list val)         (**r arguments to the call *)
-             (m: mem),                (**r memory state *)
-      state
-  | Returnstate:
-      forall (stack: list stackframe) (**r call stack *)
-             (v: val)                 (**r return value for the call *)
-             (m: mem),                (**r memory state *)
-      state.
-
-Section RELSEM.
-
-Variable ge: genv.
-
-Definition find_function
-      (ros: reg + ident) (rs: regset) : option fundef :=
-  match ros with
-  | inl r => Genv.find_funct ge rs#r
-  | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
-      end
-  end.
-
-Inductive step : state -> trace -> state -> Prop :=
-  | exec_RBnop :
-      forall s f sp pc rs m ls ci,
-      step (State s f sp pc rs m (mk_bblock (RBnop :: ls) ci) C) E0
-           (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C)
-  | exec_RBop :
-      forall s f sp pc rs m ls args op res ci v,
-      eval_operation ge sp op rs##args m = Some v ->
-      step (State s f sp pc rs m (mk_bblock (RBop op args res :: ls) ci) C) E0
-           (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C)
-  | exec_RBload:
-      forall s f sp pc rs m chunk addr args dst a v ls ci,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      step (State s f sp pc rs m (mk_bblock (RBload chunk addr args dst :: ls) ci) C)
-        E0 (State s f sp (Pos.succ pc) (rs#dst <- v) m (mk_bblock ls ci) C)
-  | exec_RBstore:
-      forall s f sp pc rs m chunk addr args src a m' ls ci,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a rs#src = Some m' ->
-      step (State s f sp pc rs m (mk_bblock (RBstore chunk addr args src :: ls) ci) C)
-        E0 (State s f sp (Pos.succ pc) rs m' (mk_bblock ls ci) C)
-  | exec_RBcond:
-      forall s f sp pc rs m cond args ifso ifnot b pc',
-      eval_condition cond rs##args m = Some b ->
-      pc' = (if b then ifso else ifnot) ->
-      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.
-*)