diff options
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. |