diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-10-26 15:44:20 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-10-26 15:44:20 +0000 |
| commit | c1d0c0fefa6e341aa115591217d945dc366d1812 (patch) | |
| tree | ac5e979d70fc659b9e19b41f698af724752ba9fe /src/extraction | |
| parent | 4d82ea5f5930bcef8bd547f415c8c040165511e1 (diff) | |
| download | vericert-c1d0c0fefa6e341aa115591217d945dc366d1812.tar.gz vericert-c1d0c0fefa6e341aa115591217d945dc366d1812.zip | |
Add tbl_to_casestatement into extraction
Diffstat (limited to 'src/extraction')
| -rw-r--r-- | src/extraction/Extraction.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index d5cb9d7..879e752 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -22,7 +22,8 @@ From vericert Require Compiler RTLBlockgen RTLBlock - HTLSchedulegen. + HTLSchedulegen + HTLgen. From Coq Require DecidableClass. @@ -180,6 +181,7 @@ Separate Extraction Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls vericert.Compiler.transf_hls_temp RTLBlockgen.transl_program RTLBlock.successors_instr + HTLgen.tbl_to_case_expr Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state |