diff options
Diffstat (limited to 'src/hls/ApplyExternctrl.v')
-rw-r--r-- | src/hls/ApplyExternctrl.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index ef056cf..bd48adb 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -142,20 +142,6 @@ Section APPLY_EXTERNCTRL. do l <- xassocmap_apply_externctrl (AssocMap.elements regmap); OK (AssocMap_Properties.of_list l). - Definition option_ram_wf (clk : reg) (mr : option HTL.ram) : - option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive). - refine ( - match mr with - | Some r => - match (plt clk (ram_addr r)) with - | left LE => Some _ - | _ => None - end - | None => None - end). - crush. - Defined. - Definition module_apply_externctrl : res HTL.module := do mod_start' <- reg_apply_externctrl (HTL.mod_start m); do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m); |