Skip to content
Iodine: Verifying Constant-Time Execution of Hardware
C++ Verilog C Yacc Haskell Python Other
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
app
benchmarks
examples added annotation files for every unit test Jun 12, 2019
iverilog-parser update May 9, 2019
liquid-fixpoint @ 2e459c1 initial commit May 9, 2019
scripts script finds qualifiers needed for FPU automatically Jun 19, 2019
src/Iodine script finds qualifiers needed for FPU automatically Jun 19, 2019
test
.ghci initial commit May 9, 2019
.gitignore renamed verylog to iodine May 10, 2019
.gitmodules initial commit May 9, 2019
.hspec initial commit May 9, 2019
.ignore
ChangeLog.md initial commit May 9, 2019
LICENSE initial commit May 9, 2019
README.md fixed name May 9, 2019
annotation-schema.json blacklist -> blocklist Jun 17, 2019
iodine fix Jun 18, 2019
package.yaml added minimal example for qualifiers Jun 18, 2019
stack.yaml initial commit May 9, 2019
t python3.6 -> python3 Jun 18, 2019

README.md

Iodine

Instructions

To build, you need to install stack. 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

./iodine -- examples/verilog/stall.v stalling_cpu
You can’t perform that action at this time.