diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-20 21:40:53 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-20 21:40:53 +0100 |
| commit | 72384a6bf701f4e1c256bec8ed85605d444f5b61 (patch) | |
| tree | c00f2d392c9116df50383f8e7bd00bd941903706 /src/hls/RTLBlockInstr.v | |
| parent | 9148e1c52b3125da76a7e81aedab42c4d6e046dd (diff) | |
| download | vericert-kvx-72384a6bf701f4e1c256bec8ed85605d444f5b61.tar.gz vericert-kvx-72384a6bf701f4e1c256bec8ed85605d444f5b61.zip | |
Start adding hashing to RTLPargen
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 79e3149..8063fd2 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -193,7 +193,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) | Pnot (Pnot p') => match trans_pred n p' with | Some (exist _ p1' _) => Some (exist _ p1' _) @@ -212,7 +212,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - split; auto. destruct (a p') eqn:?; crush. + - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. - rewrite negb_involutive in H. apply i in H. auto. |