diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
-rw-r--r-- | src/hls/HTLgenspec.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 7480231..387def0 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -75,12 +75,6 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) Hint Constructors tr_instr : htlspec. -Definition rtl_find_func (ge : RTL.genv) (symb : AST.ident) := - match Globalenvs.Genv.find_symbol ge symb with - | None => None - | Some b => Globalenvs.Genv.find_funct_ptr ge b - end. - Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : controllogic) (externctrl : AssocMap.t (ident * controlsignal)) (fin rtrn st stk : reg) : RTL.instruction -> Prop := | tr_code_single : |