diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 01:20:58 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 01:20:58 +0100 |
| commit | d530dc044242efdd4c5fafe13456cd05ac65beee (patch) | |
| tree | 38cd442a0db5c648b9be28546144c65f1add196a /src | |
| parent | 4d409fe68c693dd083295f35bd5af8bdec6d2632 (diff) | |
| download | vericert-kvx-d530dc044242efdd4c5fafe13456cd05ac65beee.tar.gz vericert-kvx-d530dc044242efdd4c5fafe13456cd05ac65beee.zip | |
Refine test file
Diffstat (limited to 'src')
| -rw-r--r-- | src/verilog/Test.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/verilog/Test.v b/src/verilog/Test.v index d94467d..5cd6ec4 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -81,8 +81,6 @@ Definition test_output_module : module := (Some Vskip)); Vdecl 1%positive 32; Vdecl 7%positive 32] |}. -Search (_ <> _ -> _ = _). - Lemma valid_test_output : transf_program test_input_program = OK test_output_module. Proof. trivial. Qed. @@ -96,7 +94,6 @@ Lemma manual_simulation : empty_assoclist test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); - try (simpl; unfold ZToValue; simpl; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); - apply nevalue; apply weqb_false; trivial. - Unshelve. exact 0%nat. + try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); + apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat. Qed. |