From ea47e9e467da22a8118fdd95e3d36aaeb41c6961 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 26 Dec 2019 03:28:39 +0100 Subject: Update --- experiments/instructions.md | 74 +++++++++++++++++++++++++++++++++++++++----- experiments/instructions.org | 59 +++++++++++++++++++++++++++++++++-- 2 files changed, 123 insertions(+), 10 deletions(-) diff --git a/experiments/instructions.md b/experiments/instructions.md index 5134551..ca77ea6 100644 --- a/experiments/instructions.md +++ b/experiments/instructions.md @@ -1,13 +1,14 @@ # Table of Contents -1. [Introduction](#org2e88aa0) -2. [Finding failures in Yosys 0.8](#org7368fab) - 1. [Installing Yosys master](#orgd073682) +1. [Introduction](#org23031ec) +2. [Finding failures in Yosys 0.8](#org081925a) + 1. [Installing Yosys master](#orgb118ae3) + 2. [Running Verismith](#org8276594) - + # Introduction @@ -16,7 +17,7 @@ The version of Verismith that is assumed to be used is Verismith 0.6.0.2, which cabal install verismith - + # Finding failures in Yosys 0.8 @@ -25,14 +26,14 @@ Yosys 0.8 was found to fail about 30% of the time, which means that it should be However, to find failures in Yosys 0.8, a newer version of Yosys has to be used for the equivalence check. For this we can use Yosys master. An alternative for this is to use a simulator with a testbench, which is also supported by Verismith using Icarus Verilog. - + ## Installing Yosys master The first step is to install Yosys master (which will in this case be installed to `/opt/yosys/master`): git clone https://github.com/yosyshq/yosys && cd yosys - sed -i 's/^PREFIX ?=.*/PREFIX ?= /opt/yosys/master' + sed -i 's:^PREFIX ?=.*:PREFIX ?= /opt/yosys/master:' Makefile make -j4 sudo make install @@ -40,7 +41,64 @@ Then we want to install Yosys 0.8 (which will be installed to `/opt/yosys/0.8`): git clean -dfx && git reset --hard HEAD git checkout yosys-0.8 - sed -i 's/^PREFIX ?=.*/PREFIX ?= /opt/yosys/0.8' + sed -i 's:^PREFIX ?=.*:PREFIX ?= /opt/yosys/0.8:' Makefile make -j4 sudo make install + + + +## Running Verismith + +We are then ready to run Verismith using the two Yosys versions that were installed. + +Using the following config file: + + [info] + commit = "UNKNOWN" + version = "0.6.0.2" + + [probability] + expr.binary = 5 + expr.concatenation = 3 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 5 + moditem.combinational = 0 + moditem.instantiation = 1 + moditem.sequential = 1 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 1 + statement.nonblocking = 5 + + [property] + determinism = 1 + module.depth = 2 + module.max = 5 + nondeterminism = 0 + output.combine = false + sample.method = "hat" + sample.size = 10 + size = 20 + statement.depth = 3 + default.yosys = "/opt/yosys/master" + + [[synthesiser]] + bin = "/opt/yosys/0.8/bin" + description = "yosys_0_8" + name = "yosys" + output = "syn_yosys_0_8.v" + + [[synthesiser]] + bin = "/opt/yosys/master" + description = "yosys_master" + name = "yosys" + output = "syn_yosys_master.v" + diff --git a/experiments/instructions.org b/experiments/instructions.org index e7b1685..1b4cdcf 100644 --- a/experiments/instructions.org +++ b/experiments/instructions.org @@ -20,7 +20,7 @@ The first step is to install Yosys master (which will in this case be installed #+begin_src git clone https://github.com/yosyshq/yosys && cd yosys -sed -i 's/^PREFIX ?=.*/PREFIX ?= /opt/yosys/master' +sed -i 's:^PREFIX ?=.*:PREFIX ?= /opt/yosys/master:' Makefile make -j4 sudo make install #+end_src @@ -30,8 +30,63 @@ Then we want to install Yosys 0.8 (which will be installed to ~/opt/yosys/0.8~): #+begin_src git clean -dfx && git reset --hard HEAD git checkout yosys-0.8 -sed -i 's/^PREFIX ?=.*/PREFIX ?= /opt/yosys/0.8' +sed -i 's:^PREFIX ?=.*:PREFIX ?= /opt/yosys/0.8:' Makefile make -j4 sudo make install #+end_src +*** Running Verismith + +We are then ready to run Verismith using the two Yosys versions that were installed. + +Using the following config file: + +#+begin_src +[info] + commit = "UNKNOWN" + version = "0.6.0.2" + +[probability] + expr.binary = 5 + expr.concatenation = 3 + expr.number = 1 + expr.rangeselect = 5 + expr.signed = 5 + expr.string = 0 + expr.ternary = 5 + expr.unary = 5 + expr.unsigned = 5 + expr.variable = 5 + moditem.assign = 5 + moditem.combinational = 0 + moditem.instantiation = 1 + moditem.sequential = 1 + statement.blocking = 0 + statement.conditional = 1 + statement.forloop = 1 + statement.nonblocking = 5 + +[property] + determinism = 1 + module.depth = 2 + module.max = 5 + nondeterminism = 0 + output.combine = false + sample.method = "hat" + sample.size = 10 + size = 20 + statement.depth = 3 + default.yosys = "/opt/yosys/master" + +[[synthesiser]] + bin = "/opt/yosys/0.8/bin" + description = "yosys_0_8" + name = "yosys" + output = "syn_yosys_0_8.v" + +[[synthesiser]] + bin = "/opt/yosys/master" + description = "yosys_master" + name = "yosys" + output = "syn_yosys_master.v" +#+end_src -- cgit