diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-13 23:02:44 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-13 23:02:44 +0000 |
| commit | dc9ad1382ee548019e6ff546a24954057cdd8ff0 (patch) | |
| tree | 133d4f98e879354fab8eda31b07bac641fea3ade /src/hls/RTLParFUgen.v | |
| parent | 22322017770c9045657f0d3a43f186ab46b0e127 (diff) | |
| download | vericert-dc9ad1382ee548019e6ff546a24954057cdd8ff0.tar.gz vericert-dc9ad1382ee548019e6ff546a24954057cdd8ff0.zip | |
Add RTLPar with functional units
Diffstat (limited to 'src/hls/RTLParFUgen.v')
| -rw-r--r-- | src/hls/RTLParFUgen.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v new file mode 100644 index 0000000..389d76c --- /dev/null +++ b/src/hls/RTLParFUgen.v @@ -0,0 +1,21 @@ +Require Import Coq.micromega.Lia. + +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.RTLParFU. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.RTLPar. + +Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program := + transform_partial_program transl_fundef p. |