diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-01 14:59:10 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-01 14:59:17 +0100 |
| commit | 0ad95850cf12bfecbb25af9721f0626d4f75c687 (patch) | |
| tree | 3d098cfe5d95a2c60a1b1f7cb7e43fd198fb5e76 | |
| parent | c689bcc4eaaaf052ecb35539dff653185192b5e9 (diff) | |
| download | vericert-kvx-0ad95850cf12bfecbb25af9721f0626d4f75c687.tar.gz vericert-kvx-0ad95850cf12bfecbb25af9721f0626d4f75c687.zip | |
Fix equivalence checking
Do not compare memories in standard operations
| -rw-r--r-- | src/hls/RTLPargen.v | 6 | ||||
| -rw-r--r-- | src/hls/Schedule.ml | 1 |
2 files changed, 2 insertions, 5 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 44a7721..2f24a42 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -594,8 +594,7 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false | Eop op1 el1 exp1, Eop op2 el2 exp2 => if operation_eq op1 op2 then - if beq_expression exp1 exp2 then - beq_expression_list el1 el2 else false else false + beq_expression_list el1 el2 else false | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => if memory_chunk_eq chk1 chk2 then if addressing_eq addr1 addr2 @@ -609,8 +608,7 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then beq_expression e1 e2 else false else false else false else false | Esetpred c1 el1 m1, Esetpred c2 el2 m2 => if condition_eq c1 c2 - then if beq_expression_list el1 el2 - then beq_expression m1 m2 else false else false + then beq_expression_list el1 el2 else false | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 26cd382..1052cb3 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -759,7 +759,6 @@ let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) in (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) - Printf.printf "%a\n" print_dfg (subgraph dfg (List.hd body)); let final_body2 = List.map (fun x -> subgraph dfg x |> (fun x -> all_dfs x |