aboutsummaryrefslogtreecommitdiffstats
path: root/docs/proof/HTL.html
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-01-20 14:53:34 +0000
committerYann Herklotz <git@yannherklotz.com>2021-01-20 14:53:34 +0000
commit8588ebb4621d85b7ccc738622339b3aa53486c31 (patch)
tree89e78e3ec67f884f7062aebb81b68aa54cf5fc1c /docs/proof/HTL.html
parent34afd2f6ea0fc55cca1c674ab9b2f181be878291 (diff)
downloadvericert-8588ebb4621d85b7ccc738622339b3aa53486c31.tar.gz
vericert-8588ebb4621d85b7ccc738622339b3aa53486c31.zip
Delete documents folder and move to separate repository
Diffstat (limited to 'docs/proof/HTL.html')
-rw-r--r--docs/proof/HTL.html193
1 files changed, 0 insertions, 193 deletions
diff --git a/docs/proof/HTL.html b/docs/proof/HTL.html
deleted file mode 100644
index d1bb193..0000000
--- a/docs/proof/HTL.html
+++ /dev/null
@@ -1,193 +0,0 @@
-<?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>HTL.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 &lt;yann@yannherklotz.com&gt;</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 &lt;https://www.gnu.org/licenses/&gt;.</span>
-<span class="c"> *)</span>
-
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> Coq <span class="kn">Require Import</span> FSets.FMapPositive.</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> vericert <span class="kn">Require Import</span> Vericertlib ValueInt AssocMap Array.</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> vericert <span class="kn">Require</span> Verilog.</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require</span> Events Globalenvs Smallstep Integers Values.</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> Maps.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-<span class="sd">(** The purpose of the hardware transfer language (HTL) is to create a more</span>
-<span class="sd">hardware-like layout that is still similar to the register transfer language</span>
-<span class="sd">(RTL) that it came from. The main change is that function calls become module</span>
-<span class="sd">instantiations and that we now describe a state machine instead of a</span>
-<span class="sd">control-flow graph. *)</span>
-
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Local Open Scope</span> assocmap.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">reg</span> := positive.</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">node</span> := positive.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">datapath</span> := PTree.t Verilog.stmnt.</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">controllogic</span> := PTree.t Verilog.stmnt.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">map_well_formed</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">m</span> : PTree.t A) : <span class="kt">Prop</span> :=
- <span class="kr">forall</span> <span class="nv">p0</span> : positive,
- In p0 (map fst (Maps.PTree.elements m)) -&gt;
- Z.pos p0 &lt;= Integers.Int.max_unsigned.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Record</span> <span class="nf">module</span>: <span class="kt">Type</span> :=
- mkmodule {
- mod_params : list reg;
- mod_datapath : datapath;
- mod_controllogic : controllogic;
- mod_entrypoint : node;
- mod_st : reg;
- mod_stk : reg;
- mod_stk_len : nat;
- mod_finish : reg;
- mod_return : reg;
- mod_start : reg;
- mod_reset : reg;
- mod_clk : reg;
- mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
- mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
- mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
- }.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">fundef</span> := AST.fundef module.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">program</span> := AST.program fundef unit.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">init_regs</span> (<span class="nv">vl</span> : list value) (<span class="nv">rl</span> : list reg) {<span class="nv">struct</span> <span class="nv">rl</span>} :=
- <span class="kr">match</span> rl, vl <span class="kr">with</span>
- | r :: rl&#39;, v :: vl&#39; =&gt; AssocMap.<span class="nb">set</span> r v (init_regs vl&#39; rl&#39;)
- | _, _ =&gt; empty_assocmap
- <span class="kr">end</span>.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">empty_stack</span> (<span class="nv">m</span> : module) : Verilog.assocmap_arr :=
- (AssocMap.<span class="nb">set</span> m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-<span class="sd">(** * Operational Semantics *)</span>
-
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">genv</span> := Globalenvs.Genv.t fundef unit.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">stackframe</span> : <span class="kt">Type</span> :=
- Stackframe :
- <span class="kr">forall</span> (<span class="nv">res</span> : reg)
- (<span class="nv">m</span> : module)
- (<span class="nv">pc</span> : node)
- (<span class="nv">reg_assoc</span> : Verilog.assocmap_reg)
- (<span class="nv">arr_assoc</span> : Verilog.assocmap_arr),
- stackframe.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">state</span> : <span class="kt">Type</span> :=
-| State :
- <span class="kr">forall</span> (<span class="nv">stack</span> : list stackframe)
- (<span class="nv">m</span> : module)
- (<span class="nv">st</span> : node)
- (<span class="nv">reg_assoc</span> : Verilog.assocmap_reg)
- (<span class="nv">arr_assoc</span> : Verilog.assocmap_arr), state
-| Returnstate :
- <span class="kr">forall</span> (<span class="nv">res</span> : list stackframe)
- (<span class="nv">v</span> : value), state
-| Callstate :
- <span class="kr">forall</span> (<span class="nv">stack</span> : list stackframe)
- (<span class="nv">m</span> : module)
- (<span class="nv">args</span> : list value), state.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">step</span> : genv -&gt; state -&gt; Events.trace -&gt; state -&gt; <span class="kt">Prop</span> :=
-| step_module :
- <span class="kr">forall</span> <span class="nv">g</span> <span class="nv">m</span> <span class="nv">st</span> <span class="nv">sf</span> <span class="nv">ctrl</span> <span class="nv">data</span>
- <span class="nv">asr</span> <span class="nv">asa</span>
- <span class="nv">basr1</span> <span class="nv">basa1</span> <span class="nv">nasr1</span> <span class="nv">nasa1</span>
- <span class="nv">basr2</span> <span class="nv">basa2</span> <span class="nv">nasr2</span> <span class="nv">nasa2</span>
- <span class="nv">asr&#39;</span> <span class="nv">asa&#39;</span>
- <span class="nv">f</span> <span class="nv">pstval</span>,
- asr!(mod_reset m) = Some (ZToValue <span class="mi">0</span>) -&gt;
- asr!(mod_finish m) = Some (ZToValue <span class="mi">0</span>) -&gt;
- asr!(m.(mod_st)) = Some (posToValue st) -&gt;
- m.(mod_controllogic)!st = Some ctrl -&gt;
- m.(mod_datapath)!st = Some data -&gt;
- Verilog.stmnt_runp f
- (Verilog.mkassociations asr empty_assocmap)
- (Verilog.mkassociations asa (empty_stack m))
- ctrl
- (Verilog.mkassociations basr1 nasr1)
- (Verilog.mkassociations basa1 nasa1) -&gt;
- basr1!(m.(mod_st)) = Some (posToValue st) -&gt;
- Verilog.stmnt_runp f
- (Verilog.mkassociations basr1 nasr1)
- (Verilog.mkassociations basa1 nasa1)
- data
- (Verilog.mkassociations basr2 nasr2)
- (Verilog.mkassociations basa2 nasa2) -&gt;
- asr&#39; = Verilog.merge_regs nasr2 basr2 -&gt;
- asa&#39; = Verilog.merge_arrs nasa2 basa2 -&gt;
- asr&#39;!(m.(mod_st)) = Some (posToValue pstval) -&gt;
- Z.pos pstval &lt;= Integers.Int.max_unsigned -&gt;
- step g (State sf m st asr asa) Events.E0 (State sf m pstval asr&#39; asa&#39;)
-| step_finish :
- <span class="kr">forall</span> <span class="nv">g</span> <span class="nv">m</span> <span class="nv">st</span> <span class="nv">asr</span> <span class="nv">asa</span> <span class="nv">retval</span> <span class="nv">sf</span>,
- asr!(m.(mod_finish)) = Some (ZToValue <span class="mi">1</span>) -&gt;
- asr!(m.(mod_return)) = Some retval -&gt;
- step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
-| step_call :
- <span class="kr">forall</span> <span class="nv">g</span> <span class="nv">m</span> <span class="nv">args</span> <span class="nv">res</span>,
- step g (Callstate res m args) Events.E0
- (State res m m.(mod_entrypoint)
- (AssocMap.<span class="nb">set</span> (mod_reset m) (ZToValue <span class="mi">0</span>)
- (AssocMap.<span class="nb">set</span> (mod_finish m) (ZToValue <span class="mi">0</span>)
- (AssocMap.<span class="nb">set</span> (mod_st m) (posToValue m.(mod_entrypoint))
- (init_regs args m.(mod_params)))))
- (empty_stack m))
-| step_return :
- <span class="kr">forall</span> <span class="nv">g</span> <span class="nv">m</span> <span class="nv">asr</span> <span class="nv">asa</span> <span class="nv">i</span> <span class="nv">r</span> <span class="nv">sf</span> <span class="nv">pc</span> <span class="nv">mst</span>,
- mst = mod_st m -&gt;
- step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
- (State sf m pc ((asr # mst &lt;- (posToValue pc)) # r &lt;- i) asa).</span></span><span class="coq-wsp">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Constructors</span> step : htl.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">initial_state</span> (<span class="nv">p</span>: program): state -&gt; <span class="kt">Prop</span> :=
- | initial_state_intro: <span class="kr">forall</span> <span class="nv">b</span> <span class="nv">m0</span> <span class="nv">m</span>,
- <span class="kr">let</span> <span class="nv">ge</span> := Globalenvs.Genv.globalenv p <span class="kr">in</span>
- Globalenvs.Genv.init_mem p = Some m0 -&gt;
- Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -&gt;
- Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -&gt;
- initial_state p (Callstate nil m nil).</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">final_state</span> : state -&gt; Integers.int -&gt; <span class="kt">Prop</span> :=
-| final_state_intro : <span class="kr">forall</span> <span class="nv">retval</span> <span class="nv">retvali</span>,
- retvali = valueToInt retval -&gt;
- final_state (Returnstate nil retval) retvali.</span></span><span class="coq-wsp">
-</span></span><span class="coq-wsp"><span class="highlight">
-</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">semantics</span> (<span class="nv">m</span> : program) :=
- Smallstep.Semantics step (initial_state m) final_state
- (Globalenvs.Genv.globalenv m).</span></span></span></pre>
-</div>
-</div></body>
-</html>
generated by cgit (git 2.34.1) at 2024-07-12 19:29:09 +0000