diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:41 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:41 +0000 |
commit | fa4b252945a870100305c159d20e264be18973ce (patch) | |
tree | 435cbd07a2af45f3f08dc8ac892fa48044047eeb /docs/proof/Simulator.html | |
parent | 29bee524cccfe08c680f655b1969a4c421e0a969 (diff) | |
download | vericert-kvx-fa4b252945a870100305c159d20e264be18973ce.tar.gz vericert-kvx-fa4b252945a870100305c159d20e264be18973ce.zip |
Add proof documentation
Diffstat (limited to 'docs/proof/Simulator.html')
-rw-r--r-- | docs/proof/Simulator.html | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/docs/proof/Simulator.html b/docs/proof/Simulator.html new file mode 100644 index 0000000..3f10d9a --- /dev/null +++ b/docs/proof/Simulator.html @@ -0,0 +1,58 @@ +<?xml version="1.0" encoding="utf-8" ?> +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" /> +<title>Simulator.v</title> +<link rel="stylesheet" href="alectryon.css" type="text/css" /> +<link rel="stylesheet" href="docutils_basic.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" /> +<script type="text/javascript" src="alectryon.js"></script> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" /> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" /> +</head> +<body> +<div class="alectryon-root alectryon-floating"><div class="document"> + + +<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-wsp"><span class="highlight"><span class="c">(*</span> +<span class="c"> * Vericert: Verified high-level synthesis.</span> +<span class="c"> * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com></span> +<span class="c"> *</span> +<span class="c"> * This program is free software: you can redistribute it and/or modify</span> +<span class="c"> * it under the terms of the GNU General Public License as published by</span> +<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span> +<span class="c"> * (at your option) any later version.</span> +<span class="c"> *</span> +<span class="c"> * This program is distributed in the hope that it will be useful,</span> +<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span> +<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span> +<span class="c"> * GNU General Public License for more details.</span> +<span class="c"> *</span> +<span class="c"> * You should have received a copy of the GNU General Public License</span> +<span class="c"> * along with this program. If not, see <https://www.gnu.org/licenses/>.</span> +<span class="c"> *)</span> + +<span class="c">(*From Coq Require Import FSets.FMapPositive.</span> + +<span class="c">From compcert Require Import Errors.</span> + +<span class="c">From vericert Require Compiler Verilog Value.</span> +<span class="c">From vericert Require Import Vericertlib.</span> + +<span class="c">Local Open Scope error_monad_scope.</span> + +<span class="c">Definition simulate (n : nat) (m : Verilog.module) : res (Value.value * list (positive * Value.value)) :=</span> +<span class="c"> do map <- Verilog.module_run n m;</span> +<span class="c"> match PositiveMap.find (fst (Verilog.mod_return m)) map with</span> +<span class="c"> | Some v => OK (v, (PositiveMap.elements map))</span> +<span class="c"> | None => Error (msg "Could not find result.")</span> +<span class="c"> end.</span> + +<span class="c">Local Close Scope error_monad_scope.</span> +<span class="c">*)</span></span></span></pre> +</div> +</div></body> +</html> |