Skip to content
Permalink
Browse files

initial commit

  • Loading branch information
gokhankici committed May 9, 2019
0 parents commit 0e795bd29da233483082d4ebe7ec257ebaadf721
Showing 788 changed files with 193,604 additions and 0 deletions.
8 .ghci
@@ -0,0 +1,8 @@
:set -fwarn-unused-binds -fwarn-unused-imports -fwarn-orphans
:set -isrc:test:app-fp

:def docs_ const $ return $ unlines [":!stack haddock"]
:def docs const $ return $ unlines [":!stack haddock --open"]
:def test const $ return $ unlines ["Test.main"]

:set prompt "\ESC[34mλ> \ESC[m"
@@ -0,0 +1,54 @@
.stack-work/
.stack-work-profile/
/verylog-hs.cabal
configuration.sh
.*.pl
.*.preproc.v
.*.smt2
.log*
flycheck_*

/*.prof
/*.prof.html

.liquid/
.*.fq

[._]*.s[a-v][a-z]
[._]*.sw[a-p]
[._]s[a-v][a-z]
[._]sw[a-p]
Session.vim
.netrwhist
*~
tags
*~
\#*\#
/.emacs.desktop
/.emacs.desktop.lock
*.elc
auto-save-list
tramp
.\#*
.org-id-locations
*_archive
*_flymake.*
/eshell/history
/eshell/lastdir
/elpa/
*.rel
/auto/
.cask/
dist/
flycheck_*.el
/server/
.projectile
.dir-locals.el

/.test-report.txt

*.annot

cplex.json

.vscode/
@@ -0,0 +1,3 @@
[submodule "liquid-fixpoint"]
path = liquid-fixpoint
url = https://github.com/gokhankici/liquid-fixpoint.git
3 .hspec
@@ -0,0 +1,3 @@
--fail-fast
--failure-report=.test-report.txt
--print-cpu-time
@@ -0,0 +1 @@
/liquid-fixpoint/
@@ -0,0 +1,3 @@
# Changelog for verylog-hs

## Unreleased changes
@@ -0,0 +1,7 @@
Copyright 2018 Rami Gokhan Kici

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
@@ -0,0 +1,39 @@
# verylog

## Instructions

To build, you need to install
[stack](https://docs.haskellstack.org/en/stable/README/#how-to-install). When
installed, just run `./iodine`. For the test suite, run `./t`.

## Command Line Options

```
iodine v1.0, (C) Rami Gokhan Kici 2019
iodine [OPTIONS] FILE MODULE
Common flags:
--iverilog-dir=DIR path of the iverilog-parser directory
--ir just generate the IR file
-v --vcgen just generate the .fq file
-m --minimize run delta-debugging of fixpoint
--no-save --nosave do not save the fq file
-a --abduction run abduction algorithm
-t --time print the runtime
--no-output --nofpoutput disable the output from fixpoint
-h --help Display help message
-V --version Print version information
--numeric-version Print just the version number
Checks whether the given Verilog file runs in constant time.
First argument is the path the to the verilog file.
Second argument is the name of the root Verilog module in that file.
```

### Example

```sh
./iodine -- examples/verilog/stall.v stalling_cpu
```
@@ -0,0 +1,6 @@
module Main where

import qualified Verylog.Runner as R (main)

main :: IO ()
main = R.main
@@ -0,0 +1,71 @@
# ##############################################################################
# emacs
# ##############################################################################
*~
\#*\#
/.emacs.desktop
/.emacs.desktop.lock
*.elc
auto-save-list
tramp
.\#*

# Org-mode
.org-id-locations
*_archive

# flymake-mode
*_flymake.*

# eshell files
/eshell/history
/eshell/lastdir

# elpa packages
/elpa/

# reftex files
*.rel

# AUCTeX auto folder
/auto/

# cask packages
.cask/
dist/

# Flycheck
flycheck_*.el

# server auth directory
/server/

# projectiles files
.projectile

# directory configuration
.dir-locals.el
# ##############################################################################

# ##############################################################################
# vim
# ##############################################################################
# Swap
[._]*.s[a-v][a-z]
[._]*.sw[a-p]
[._]s[a-v][a-z]
[._]sw[a-p]

# Session
Session.vim

# Temporary
.netrwhist
*~
# Auto-generated tag files
tags
# ##############################################################################

.*.pl
.*.dot
.*.pdf
@@ -0,0 +1,8 @@
pipelined/*
tmp*
work*
transcript
*.bak
*.mti
*.mpf
*.wlf
@@ -0,0 +1,149 @@
// simplified version of the processor in
// https://github.com/russellhaering/472-mips-pipelined/blob/master/mips_pipeline.v .
// Includes stalls (no reset).

`include "alu_stub.v"
`include "alu_ctl_stub.v"
`include "control_pipeline.v"

module mips_pipeline(clk, reset);
input clk, reset;

// @annot{taint_source(IF_instr)}
// @annot{taint_sink(ID_instr)}

// @annot{sanitize_glob(IF_instr)}

// @annot{sanitize(Stall, IF_instr, ID_instr, EX_ALUOp, EX_extend, EX_MemRead, MEM_ALUOut, WB_ALUOut, EX_rt)}

//=============
// Definitions
//=============

reg [1:0] Stall;
reg [31:0] IF_instr;
reg [31:0] ID_instr;
reg [1:0] EX_ALUOp;
reg [31:0] EX_extend;
reg EX_MemRead;

reg [31:0] MEM_ALUOut;
reg [31:0] WB_ALUOut;
reg [4:0] EX_rt;

wire [4:0] ID_rs, ID_rt;

wire [5:0] ID_op;
wire [1:0] ID_ALUOp;
wire [15:0] ID_immed;
wire [31:0] ID_extend;
wire [5:0] EX_funct;
wire [2:0] EX_Operation;
wire [31:0] EX_ALUOut;
wire ID_MemRead, ID_MemRead_v;

wire ID_RegWrite_v, ID_MemWrite_v, ID_Branch_v, ID_Jump_v, ID_RegDst, ID_MemtoReg, ID_ALUSrc;
//=============
// IF stage
//=============

// -- magic happens here
always @(posedge clk)
if (Stall)
ID_instr <= ID_instr;
else
ID_instr <= IF_instr;

// Hazard detection
always @(*)
if (EX_MemRead && ((EX_rt == ID_rs) || (EX_rt == ID_rt)))
Stall = 1;
else
Stall = 0;

// wiring
assign ID_op = ID_instr[31:26];
assign ID_MemRead = Stall ? 1'b0 : ID_MemRead_v;

//--------------------------------------
// Map OP-code to internal control code.
//--------------------------------------
// Don't expand; treat as uninterpreted funciton of inputs.
// This seems fine as output is fully determined by ID_op.
// Easy to spot as modules declare inputs and outputs.

// @annot{sanitize_mod(control_pipeline, ALUOp)}
// @annot{sanitize_mod(control_pipeline, ALUSrc)}
// @annot{sanitize_mod(control_pipeline, Branch)}
// @annot{sanitize_mod(control_pipeline, Jump)}
// @annot{sanitize_mod(control_pipeline, MemRead)}
// @annot{sanitize_mod(control_pipeline, MemWrite)}
// @annot{sanitize_mod(control_pipeline, MemtoReg)}
// @annot{sanitize_mod(control_pipeline, RegDst)}
// @annot{sanitize_mod(control_pipeline, RegWrite)}
control_pipeline CTL
(.opcode(ID_op),
.RegDst(ID_RegDst),
.ALUSrc(ID_ALUSrc),
.MemtoReg(ID_MemtoReg),
.RegWrite(ID_RegWrite_v),
.MemRead(ID_MemRead_v),
.MemWrite(ID_MemWrite_v),
.Branch(ID_Branch_v),
.ALUOp(ID_ALUOp),
.Jump(ID_Jump_v)
);

//=============
// DEC stage
//=============

// treat all of those as uninterpreted functions of ID_instr.
assign ID_immed = ID_instr[15:0];
assign ID_extend = { {16{ID_immed[15]}}, ID_immed };
assign ID_rt = ID_instr[20:16];
assign ID_rs = ID_instr[25:21];

always @(posedge clk) // ID/EX Pipeline Register
begin
EX_ALUOp <= ID_ALUOp;
EX_extend <= ID_extend;
EX_MemRead <= ID_MemRead;
EX_rt <= ID_rt;
end

//=============
// EXEC stage
//=============

assign EX_funct = EX_extend[5:0];

// Same as before: simplifying assumption.
//
// @annot{sanitize_mod(alu_ctl_stub, ALUOperation)}
alu_ctl_stub EX_ALUCTL(EX_ALUOp, EX_funct, EX_Operation);


wire zero;
reg a; // @annot{sanitize(a)}
reg b; // @annot{sanitize(b)}
// @annot{sanitize_mod(alu_stub, result)}
// @annot{sanitize_mod(alu_stub, zero)}
alu_stub EX_ALU(EX_Operation, a, b, EX_ALUOut, zero);

always @(posedge clk)
MEM_ALUOut <= EX_ALUOut;

//=============
// MEM stage
//=============

always @(posedge clk)
WB_ALUOut <= MEM_ALUOut;

//=============
// WB stage
//=============


endmodule

0 comments on commit 0e795bd

Please sign in to comment.
You can’t perform that action at this time.