diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-30 21:42:52 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-30 21:42:52 +0100 |
commit | 6e2259a57b6ca00c068b176b9d5087ed632598c2 (patch) | |
tree | 20f2f9815c243dc13b9f93b352d20e8b92d9f16e /src/hls/Schedule.ml | |
parent | 81aa3b8c3e20f86a71607bea0c9aa9bdf090781f (diff) | |
download | vericert-6e2259a57b6ca00c068b176b9d5087ed632598c2.tar.gz vericert-6e2259a57b6ca00c068b176b9d5087ed632598c2.zip |
Fix compilation issues with new types
Diffstat (limited to 'src/hls/Schedule.ml')
-rw-r--r-- | src/hls/Schedule.ml | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 2389369..dd3e39f 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -26,6 +26,7 @@ open AST open Kildall open Op open RTLBlockInstr +open Predicate open RTLBlock open HTL open Verilog @@ -105,7 +106,7 @@ let print_instr = function | RBnop -> "" | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) - | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) + | RBsetpred (_, _, _, p) -> sprintf "setpred(%s)" (print_pred p) | RBop (_, op, args, d) -> (match op, args with | Omove, _ -> "mov" @@ -354,7 +355,7 @@ let rec find_all_next_dst_read i dst i' curr = | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' - | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' + | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr' let drop i lst = let rec drop' i' lst' = @@ -413,10 +414,11 @@ let accumulate_WAW_mem_deps instrs dfg curri = let rec in_predicate p p' = match p' with - | Pvar p'' -> P.to_int p = P.to_int p'' - | Pnot p'' -> in_predicate p p'' + | Plit p'' -> P.to_int p = P.to_int (snd p'') | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 + | Ptrue -> false + | Pfalse -> false let get_predicate = function | RBop (p, _, _, _) -> p @@ -426,7 +428,7 @@ let get_predicate = function let rec next_setpred p i = function | [] -> None - | RBsetpred (_, _, p') :: rst -> + | RBsetpred (_, _, _, p') :: rst -> if in_predicate p' p then Some i else @@ -459,7 +461,7 @@ let accumulate_RAW_pred_deps instrs dfg curri = let accumulate_WAR_pred_deps instrs dfg curri = let i, curr = curri in match curr with - | RBsetpred (_, _, p) -> ( + | RBsetpred (_, _, _, p) -> ( match next_preduse p 0 (take i instrs |> List.rev) with | None -> dfg | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) @@ -468,8 +470,8 @@ let accumulate_WAR_pred_deps instrs dfg curri = let accumulate_WAW_pred_deps instrs dfg curri = let i, curr = curri in match curr with - | RBsetpred (_, _, p) -> ( - match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with + | RBsetpred (_, _, _, p) -> ( + match next_setpred (Plit (true, p)) 0 (take i instrs |> List.rev) with | None -> dfg | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) | _ -> dfg @@ -512,18 +514,18 @@ let assigned_vars vars = function | RBop (_, _, _, dst) -> dst :: vars | RBload (_, _, _, _, dst) -> dst :: vars | RBstore (_, _, _, _, _) -> vars - | RBsetpred (_, _, _) -> vars + | RBsetpred (_, _, _, _) -> vars let get_pred = function | RBnop -> None | RBop (op, _, _, _) -> op | RBload (op, _, _, _, _) -> op | RBstore (op, _, _, _, _) -> op - | RBsetpred (_, _, _) -> None + | RBsetpred (_, _, _, _) -> None let independant_pred p p' = - match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with - | Some None -> true + match sat_pred_simple (Pand (p, p')) with + | None -> true | _ -> false let check_dependent op1 op2 = |