diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 22:25:06 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 22:25:06 +0000 |
| commit | d460696e02f02ae25752678652757da11a44f50a (patch) | |
| tree | 4e3459da825a6920c342ff6c5445023c83fb6507 /src/hls/HTLgenproof.v | |
| parent | 929ca73f8aed8c122b93527c545a38dd82d52647 (diff) | |
| download | vericert-d460696e02f02ae25752678652757da11a44f50a.tar.gz vericert-d460696e02f02ae25752678652757da11a44f50a.zip | |
Add match_states for RTLPargen proof
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index f2de2d9..9a7e272 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -17,10 +17,24 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require RTL Registers AST. -From compcert Require Import Integers Globalenvs Memory Linking. -From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. -From vericert Require HTL Verilog. +Require compcert.backend.RTL. +Require compcert.backend.Registers. +Require compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Linking. +Require Import compcert.common.Memory. +Require Import compcert.lib.Integers. + +Require Import vericert.common.IntegerExtra. +Require Import vericert.common.Vericertlib. +Require Import vericert.common.ZExtra. +Require Import vericert.hls.Array. +Require Import vericert.hls.AssocMap. +Require vericert.hls.HTL. +Require Import vericert.hls.HTLgen. +Require Import vericert.hls.HTLgenspec. +Require Import vericert.hls.ValueInt. +Require vericert.hls.Verilog. Require Import Lia. |