Skip to content
Permalink
Browse files

Integrated verification analysis with new structure

  • Loading branch information
cristian-mattarei committed Sep 27, 2017
1 parent a60bce6 commit ebe090648410606d4c35e24632c84829423dff6c
@@ -23,7 +23,7 @@ CXX = g++-4.9
endif

CFLAGS = -Wall -fPIC
CXXFLAGS = -std=c++11 -Wall -fPIC -Werror
CXXFLAGS = -std=c++11 -Wall -fPIC #-Werror

ifdef COREDEBUG
CXXFLAGS += -O0 -g3 -D_GLIBCXX_DEBUG
@@ -1,5 +1,5 @@
#include "coreir.h"
#include "coreir-passes/analysis/helloa.h"
#include "coreir/passes/analysis/helloa.h"

using namespace CoreIR;

@@ -1,11 +1,13 @@
{
"top" : "global.counters",
"namespaces": {
"global": {
"properties": [["exec_to_30","invar","out != 0ud16_10"],
["out_plus_1","invar","(!B(clk) & next(B(clk)) & B(en)) -> (next(out) = (out + 0ud16_1))"],
["reset","ltl","G(F((!B(clk) & next(B(clk)) & B(en)) -> (next(out) = 0ud16_0)))"]],
"modules": {
"counters": {
"metadata" : {"properties": [["exec_to_30","invar","out != 0ud16_10"],
["out_plus_1","invar","(!B(clk) & next(B(clk)) & B(en)) -> (next(out) = (out + 0ud16_1))"],
["reset","ltl","G(F((!B(clk) & next(B(clk)) & B(en)) -> (next(out) = 0ud16_0)))"]]
},
"type": ["Record",{
}],
"instances": {
@@ -1,96 +1,98 @@
{
"namespaces": {
"global": {
"properties": [["exec_to_30","invar","out != 0ud16_10"],
["out_plus_1","invar","(!B(clk) & next(B(clk)) & B(en)) -> (next(out) = (out + 0ud16_1))"],
["reset","ltl","G(F((!B(clk) & next(B(clk)) & B(en)) -> (next(out) = 0ud16_0)))"]],
"modules": {
"counters": {
"type": ["Record",{
}],
"instances": {
"count0": {"modref": "global.counter"},
"count1": {"modref": "global.counter"},
"slice0": {
"genref": "coreir.slice",
"genargs": {"width":16, "lo":0,"hi":8}
},
"slice1": {
"genref": "coreir.slice",
"genargs": {"width":16, "lo":8,"hi":16}
},
"cat": {
"genref": "coreir.concat",
"genargs": {"width0":8, "width1":8}
},
"neg": {
"genref": "coreir.neg",
"genargs": {"width":16}
},
"term": {
"genref": "coreir.term",
"genargs": {"width":16}
"top" : "global.counters",
"namespaces": {
"global": {
"modules": {
"counters": {
"metadata" : {"properties": [["exec_to_30","invar","out != 0ud16_10"],
["out_plus_1","invar","(!B(clk) & next(B(clk)) & B(en)) -> (next(out) = (out + 0ud16_1))"],
["reset","ltl","G(F((!B(clk) & next(B(clk)) & B(en)) -> (next(out) = 0ud16_0)))"]]
},
"type": ["Record",{
}],
"instances": {
"count0": {"modref": "global.counter"},
"count1": {"modref": "global.counter"},
"slice0": {
"genref": "coreir.slice",
"genargs": {"width":16, "lo":0,"hi":8}
},
"slice1": {
"genref": "coreir.slice",
"genargs": {"width":16, "lo":8,"hi":16}
},
"cat": {
"genref": "coreir.concat",
"genargs": {"width0":8, "width1":8}
},
"neg": {
"genref": "coreir.neg",
"genargs": {"width":16}
},
"term": {
"genref": "coreir.term",
"genargs": {"width":16}
}
},
"connections": [
["count0.out.4","count1.en"],
["count1.out.8","count0.en"],
["count0.out","slice0.in"],
["count1.out","slice1.in"],
["slice0.out","cat.in0"],
["slice1.out","cat.in1"],
["cat.out","neg.in"],
["neg.out","term.in"]
]
},
"counter": {
"type": ["Record",{
"en": "BitIn",
"out": ["Array",16,"Bit"]
}],
"instances": {
"c1": {
"genref": "coreir.const",
"genargs": {"width":16},
"configargs": {"value":1}
},
"r": {
"genref": "coreir.reg",
"genargs": {"width":16,"en":true}
},
"a": {
"genref": "coreir.add",
"genargs": {"width":16}
},
"c2": {
"genref": "coreir.const",
"genargs": {"width":15},
"configargs": {"value":0}
},
"a2": {
"genref": "coreir.add",
"genargs": {"width":16}
},
"cc": {
"genref": "coreir.concat",
"genargs": {"width0":15, "width1":1}
}
},
"connections": [
["c1.out","a.in0"],
["r.out","a.in1"],
["a.out","a2.in0"],
["cc.out","a2.in1"],
["c2.out","cc.in0"],
["a.out.6","cc.in1.0"],
["a2.out","r.in"],
["r.out","self.out"],
["self.en","r.en"]
]
}
}
},
"connections": [
["count0.out.4","count1.en"],
["count1.out.8","count0.en"],
["count0.out","slice0.in"],
["count1.out","slice1.in"],
["slice0.out","cat.in0"],
["slice1.out","cat.in1"],
["cat.out","neg.in"],
["neg.out","term.in"]
]
},
"counter": {
"type": ["Record",{
"en": "BitIn",
"out": ["Array",16,"Bit"]
}],
"instances": {
"c1": {
"genref": "coreir.const",
"genargs": {"width":16},
"configargs": {"value":1}
},
"r": {
"genref": "coreir.reg",
"genargs": {"width":16,"en":true}
},
"a": {
"genref": "coreir.add",
"genargs": {"width":16}
},
"c2": {
"genref": "coreir.const",
"genargs": {"width":15},
"configargs": {"value":0}
},
"a2": {
"genref": "coreir.add",
"genargs": {"width":16}
},
"cc": {
"genref": "coreir.concat",
"genargs": {"width0":15, "width1":1}
}
},
"connections": [
["c1.out","a.in0"],
["r.out","a.in1"],
["a.out","a2.in0"],
["cc.out","a2.in1"],
["c2.out","cc.in0"],
["a.out.6","cc.in1.0"],
["a2.out","r.in"],
["r.out","self.out"],
["self.en","r.en"]
]
}
}
}
}
}


@@ -5,6 +5,7 @@

namespace CoreIR {

using namespace std;
static const string SEP = "$";

class Pass {
File renamed without changes.
@@ -21,7 +21,7 @@ class SmtLib2 : public InstanceGraphPass {
SmtLib2() : InstanceGraphPass(ID,"Creates SmtLib2 representation of IR",true) {}
bool runOnInstanceGraphNode(InstanceGraphNode& node) override;
void setAnalysisInfo() override {
addDependency("strongverify");
addDependency("verifyconnectivity");
addDependency("verifyflattenedtypes");
addDependency("verifyflatcoreirprims");
}
@@ -17,6 +17,7 @@


using namespace CoreIR; //TODO get rid of this
using namespace std;

class SmtBVVar {
string instname = "";
@@ -2,10 +2,11 @@
#define SMTOPERATORS_HPP_

#include "coreir.h"
#include "coreir-passes/analysis/smtmodule.hpp"
#include "coreir/passes/analysis/smtmodule.hpp"
#include <ostream>

using namespace CoreIR;
using namespace std;
namespace CoreIR {
namespace Passes {
typedef std::pair<string, SmtBVVar> named_var;
@@ -11,7 +11,7 @@
namespace CoreIR {
namespace Passes {

class SMV : public InstanceGraphPass {
class SMV : public InstanceGraphPass { // ModulePass
unordered_map<Instantiable*,SMVModule*> modMap;
unordered_map<string, PropDef> properties;
unordered_set<Instantiable*> external;
@@ -20,9 +20,9 @@ class SMV : public InstanceGraphPass {
public :
static std::string ID;
SMV() : InstanceGraphPass(ID,"Creates SMV representation of IR",true) {}
bool runOnInstanceGraphNode(InstanceGraphNode& node) override;
bool runOnInstanceGraphNode(InstanceGraphNode& node) override; // runOnModule(Module* module)
void setAnalysisInfo() override {
addDependency("strongverify");
addDependency("verifyconnectivity");
addDependency("verifyflattenedtypes");
// addDependency("verifyflatten");
}
@@ -17,6 +17,7 @@


using namespace CoreIR; //TODO get rid of this
using namespace std;

class SmvBVVar {
string instname = "";
@@ -2,10 +2,11 @@
#define SMVOPERATORS_HPP_

#include "coreir.h"
#include "coreir-passes/analysis/smvmodule.hpp"
#include "coreir/passes/analysis/smvmodule.hpp"
#include <ostream>

using namespace CoreIR;
using namespace std;
namespace CoreIR {
namespace Passes {
typedef std::pair<string, SmvBVVar> named_var;
@@ -6,10 +6,10 @@
#include "analysis/createinstancegraph.h"
#include "analysis/firrtl.h"
#include "analysis/verilog.h"
#include "analysis/smtlib2.h"
#include "analysis/smv.h"
#include "coreir/passes/analysis/smtlib2.h"
#include "coreir/passes/analysis/smv.h"
#include "coreir/passes/analysis/verifyflatcoreirprims.h"
#include "analysis/coreirjson.h"
#include "analysis/verifyflatcoreirprims.h"
#include "analysis/verifyconnectivity.h"
#include "analysis/verifyinputconnections.h"
#include "analysis/verifyflattenedtypes.h"
@@ -40,7 +40,7 @@ namespace CoreIR {
pm.addPass(new Passes::Verilog());
pm.addPass(new Passes::SmtLib2());
pm.addPass(new Passes::SMV());
pm.addPass(new Passes::VerifyFlatCoreirPrims());
pm.addPass(new Passes::VerifyFlatCoreirPrims());
pm.addPass(new Passes::VerifyInputConnections());
pm.addPass(new Passes::VerifyConnectivity(true,true));
pm.addPass(new Passes::VerifyConnectivity(true,false));
@@ -3,8 +3,8 @@
#include <dlfcn.h>
#include <fstream>

#include "coreir-passes/analysis/smtlib2.h"
#include "coreir-passes/analysis/smv.h"
#include "coreir/passes/analysis/smtlib2.h"
#include "coreir/passes/analysis/smv.h"
#include "coreir/passes/analysis/firrtl.h"
#include "coreir/passes/analysis/coreirjson.h"
#include "coreir/passes/analysis/verilog.h"
@@ -68,7 +68,7 @@ bool loadFromFile(Context* c, string filename,Module** top) {
for (auto jnsmap : j.at("namespaces").get<jsonmap>() ) {
string nsname = jnsmap.first;
json jns = jnsmap.second;
checkJson(jns,{"namedtypes","namedtypegens","modules","generators","properties"});
checkJson(jns,{"namedtypes","namedtypegens","modules","generators"});
Namespace* ns;
if (c->hasNamespace(nsname) ) ns = c->getNamespace(nsname);
else ns = c->newNamespace(nsname);
@@ -120,9 +120,6 @@ bool loadFromFile(Context* c, string filename,Module** top) {
for (auto nsq : nsqueue) {
Namespace* ns = nsq.first;
json jns = nsq.second;
if (jns.count("properties")) {
// ns->setProperty(jns["properties"]);
}
//Load Modules
if (jns.count("modules")) {
for (auto jmodmap : jns.at("modules").get<jsonmap>()) {
@@ -135,7 +132,7 @@ bool loadFromFile(Context* c, string filename,Module** top) {
}

json jmod = jmodmap.second;
checkJson(jmod,{"type","configparams","defaultconfigargs","instances","connections"});
checkJson(jmod,{"type","configparams","defaultconfigargs","instances","connections","metadata"});
Type* t = json2Type(c,jmod.at("type"));

Params configparams;
@@ -187,7 +187,7 @@ bool inlineInstance(Instance* inst) {
addPassthrough(defInline->getInterface(),"_insidePT");


string inlinePrefix = inst->getInstname() + SEP;
string inlinePrefix = inst->getInstname() + "$";

//First add all the instances of defInline into def with a new name
for (auto instmap : defInline->getInstances()) {

This file was deleted.

0 comments on commit ebe0906

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