diff options
Diffstat (limited to 'src/hls/HTL.v')
-rw-r--r-- | src/hls/HTL.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index c22497f..3116af3 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -447,3 +447,17 @@ Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True} | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H end; unfold module_ordering; auto. Defined. + +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. |