From 9ba75dc996009a7a01960fce72a25d43c557f542 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 17 Apr 2020 14:55:23 +0100 Subject: Add Simulator.v --- Makefile | 2 +- src/Simulator.v | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 src/Simulator.v diff --git a/Makefile b/Makefile index 0c26d57..1d328ec 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,7 @@ COQMAKE := "$(COQBIN)coq_makefile" COQUPDIRS := translation common verilog VSSUBDIR := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) -VS := src/Compiler.v $(VSSUBDIR) +VS := src/Compiler.v src/Simulator.v $(VSSUBDIR) PREFIX ?= . diff --git a/src/Simulator.v b/src/Simulator.v new file mode 100644 index 0000000..3c5aca0 --- /dev/null +++ b/src/Simulator.v @@ -0,0 +1,32 @@ +(* -*- mode: coq -*- + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From Coq Require Import FSets.FMapPositive. + +From compcert Require Import Errors. + +From coqup Require Compiler Verilog Value. +From coqup Require Import Coquplib. + +Local Open Scope error_monad_scope. + +Definition simulate (n : nat) (m : Verilog.module) : res (list (positive * Value.value)) := + do map <- Verilog.module_run n m; + OK (PositiveMap.elements map). + +Local Close Scope error_monad_scope. -- cgit