Skip to content
Permalink
Browse files

Adding example files

  • Loading branch information
makaimann committed Aug 22, 2017
1 parent 2a5e49d commit be6435fdb7723d0c50187bc7ee1d7a08a3d0cfa7
Showing with 212 additions and 0 deletions.
  1. +30 −0 smtlib/andreg.smt2
  2. +86 −0 smtlib/counters.json
  3. 0 smtlib/counters.v
  4. +86 −0 smtlib/counters_flattened.json
  5. +10 −0 smtlib/parse_coreir.py
@@ -0,0 +1,30 @@
;; smt-lib for very simple circuit
;;
;; a -->
;; And --> Reg -->
;; b -->


(declare-fun and.a () (_BitVec 1))
(declare-fun and.b () (_ BitVec 1))
(declare-fun and.o () (_ BitVec 1))
(declare-fun and.a_N () (_ BitVec 1))
(declare-fun and.b_N () (_ BitVec 1))
(declare-fun and.o_N () (_ BitVec 1))

(declare-fun reg.clk () (_ BitVec 1))
(declare-fun reg.clk_N () (_ BitVec 1))
(declare-fun reg.in () (_ BitVec 1))
(declare-fun reg.in_N () (_ BitVec 1))
(declare-fun reg.out () (_ BitVec 1))
(declare-fun reg.out_N () (_ BitVec 1))

(assert (= (bvand and.a and.b) and.o))
(assert (= (bvand and.a_N and.b_N) and.o_N))

(assert (= and.o reg.in))
(assert (= and.o_N reg.in_N))

(assert (=> ((bvand (bvnot reg.clk) reg.clk_N))
(= reg.o_N reg.in)
))
@@ -0,0 +1,86 @@
{"top":"global.counterTestBench",
"namespaces":{
"global":{
"modules":{
"counterTestBench":{
"type":["Record",{

}],
"instances":{
"c0":{
"modref":"global.counter_U1"
},
"c1":{
"modref":"global.counter_U0"
}
},
"connections":[
["c0.out.16","c1.en"]
]
},
"counter_U0":{
"type":["Record",{
"en":"BitIn",
"out":["Array",23,"Bit"],
"clk":["Named","coreir.clkIn"]
}],
"instances":{
"ai":{
"genref":"coreir.add",
"genargs":{"width":23}
},
"ci":{
"genref":"coreir.const",
"genargs":{"width":23},
"configargs":{"value":1}
},
"ri":{
"genref":"coreir.reg",
"genargs":{"clr":false, "rst":false, "en":true, "width":23},
"configargs":{"init":0}
}
},
"connections":[
["self.out","ri.out"],
["self.en","ri.en"],
["self.clk","ri.clk"],
["ri.out","ai.in1"],
["ri.in","ai.out"],
["ci.out","ai.in0"]
]
},
"counter_U1":{
"type":["Record",{
"en":"BitIn",
"out":["Array",17,"Bit"],
"clk":["Named","coreir.clkIn"]
}],
"instances":{
"ai":{
"genref":"coreir.add",
"genargs":{"width":17}
},
"ci":{
"genref":"coreir.const",
"genargs":{"width":17},
"configargs":{"value":1}
},
"ri":{
"genref":"coreir.reg",
"genargs":{"clr":false, "rst":false, "en":true, "width":17},
"configargs":{"init":0}
}
},
"connections":[
["self.out","ri.out"],
["self.en","ri.en"],
["self.clk","ri.clk"],
["ri.out","ai.in1"],
["ri.in","ai.out"],
["ci.out","ai.in0"]
]
}
}
}
}
}
No changes.
@@ -0,0 +1,86 @@
{"top":"global.counterTestBench",
"namespaces":{
"global":{
"modules":{
"counterTestBench":{
"type":["Record",{

}],
"instances":{
"c0":{
"modref":"global.counter_U1"
},
"c1":{
"modref":"global.counter_U0"
}
},
"connections":[
["c0.out.16","c1.en"]
]
},
"counter_U0":{
"type":["Record",{
"out":["Array",23,"Bit"],
"clk":["Named","coreir.clkIn"],
"en":"BitIn"
}],
"instances":{
"ai":{
"genref":"coreir.add",
"genargs":{"width":23}
},
"ci":{
"genref":"coreir.const",
"genargs":{"width":23},
"configargs":{"value":1}
},
"ri":{
"genref":"coreir.reg",
"genargs":{"clr":false, "rst":false, "en":true, "width":23},
"configargs":{"init":0}
}
},
"connections":[
["self.out","ri.out"],
["self.en","ri.en"],
["self.clk","ri.clk"],
["ri.out","ai.in1"],
["ri.in","ai.out"],
["ci.out","ai.in0"]
]
},
"counter_U1":{
"type":["Record",{
"out":["Array",17,"Bit"],
"clk":["Named","coreir.clkIn"],
"en":"BitIn"
}],
"instances":{
"ai":{
"genref":"coreir.add",
"genargs":{"width":17}
},
"ci":{
"genref":"coreir.const",
"genargs":{"width":17},
"configargs":{"value":1}
},
"ri":{
"genref":"coreir.reg",
"genargs":{"clr":false, "rst":false, "en":true, "width":17},
"configargs":{"init":0}
}
},
"connections":[
["self.out","ri.out"],
["self.en","ri.en"],
["self.clk","ri.clk"],
["ri.out","ai.in1"],
["ri.in","ai.out"],
["ci.out","ai.in0"]
]
}
}
}
}
}
@@ -0,0 +1,10 @@
import coreir

def load_core(f, *libs):
context = coreir.Context()
for lib in libs:
context.load_library(lib)

top_module = context.load_from_file(f)
# top_def = top_module.definition

0 comments on commit be6435f

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