Permalink
Browse files

Uniforms (#131)

* Added uniforms and SMT checking
  • Loading branch information...
jameshegarty committed Dec 10, 2018
1 parent 45fb228 commit f47a72ef232fd6ca63da74d1c1655b9ded8cbc72
Showing with 1,710 additions and 496 deletions.
  1. +4 −1 examples/campipe_core.lua
  2. +1 −1 examples/conv_tr_handshake_4_1.lua
  3. +1 −1 examples/gold/soc_2in.terra.cycles.txt
  4. +1 −1 examples/gold/soc_convgen.terra.cycles.txt
  5. +1 −1 examples/gold/soc_convgenTaps.terra.cycles.txt
  6. +1 −1 examples/gold/soc_flip.terra.cycles.txt
  7. +1 −1 examples/gold/soc_parread.terra.cycles.txt
  8. +1 −1 examples/gold/soc_regin.terra.cycles.txt
  9. +1 −1 examples/gold/soc_regout.terra.cycles.txt
  10. +1 −1 examples/gold/soc_simple.terra.cycles.txt
  11. +1 −0 examples/gold/soc_simple_uniform.bmp
  12. +1 −0 examples/gold/soc_simple_uniform.regout.lua
  13. +1 −0 examples/gold/soc_simple_uniform.terra.cycles.txt
  14. +1 −1 examples/gold/soc_sort.terra.cycles.txt
  15. +1 −1 examples/gold/soc_tokencounter.terra.cycles.txt
  16. +1 −1 examples/gold/soc_unaligned.terra.cycles.txt
  17. +1 −1 examples/gold/soc_underflow.terra.cycles.txt
  18. +9 −8 examples/harness.lua
  19. +21 −5 examples/harnessSOC.lua
  20. +9 −27 examples/harnessTerraSOC.t
  21. +1 −1 examples/makefile
  22. +31 −0 examples/soc_simple_uniform.lua
  23. +2 −3 examples/triggeredCounter.lua
  24. +24 −3 misc/extractMetadata.lua
  25. +1 −1 misc/rigelSimple.lua
  26. +172 −53 {examples → modules}/examplescommon.lua
  27. 0 {examples → modules}/examplescommonTerra.t
  28. +10 −3 {src → modules}/generators.lua
  29. +201 −124 {src → modules}/modules.lua
  30. +15 −13 {src → modules}/modulesTerra.t
  31. +100 −47 modules/soc.lua
  32. +27 −31 modules/socTerra.t
  33. +2 −1 platform/axi/wrapper.lua
  34. +38 −5 platform/verilatorSOC/harness.cpp
  35. +59 −43 rigel.lua
  36. +9 −6 src/common.lua
  37. +15 −10 src/fpgamodules.lua
  38. +20 −8 src/sdf.lua
  39. +65 −27 src/sdfrate.lua
  40. +40 −19 src/systolic.lua
  41. +24 −20 src/systolicsugar.lua
  42. +71 −24 src/types.lua
  43. +700 −0 src/uniform.lua
  44. +24 −0 src/uniformTerra.t
@@ -127,7 +127,10 @@ end

function CC.makeGamma(g)
local gamma = {}
for i=0,255 do table.insert(gamma, math.pow(i/255,g)*255) end
for i=0,255 do
local v= math.pow(i/255,g)*255
table.insert(gamma, math.floor(v))
end
return gamma
end

@@ -22,7 +22,7 @@ function MAKE(T,ConvWidth,size1080p)
inputW, inputH = 1920, 1080
end

local PadRadius = J.upToNearest(T, ConvRadius)
local PadRadius = J.upToNearest(math.max(T,1), ConvRadius)

-- expand to include crop region
--W = upToNearest(T,128+ConvWidth-1)
@@ -1 +1 @@
1032
1035
@@ -1 +1 @@
2092819
2092822
@@ -1 +1 @@
2092819
2092822
@@ -1 +1 @@
1037
1040
@@ -1 +1 @@
534
537
@@ -1 +1 @@
1031
1034
@@ -1 +1 @@
8203
8206
@@ -1 +1 @@
1040
1043
@@ -0,0 +1 @@
return {readAddress=805339136,writeAddress=805347328}
@@ -1 +1 @@
1042
1045
@@ -1 +1 @@
8074
8077
@@ -1 +1 @@
153
156
@@ -1 +1 @@
8339
8342
@@ -6,6 +6,7 @@ local types = require("types")
local SDFRate = require "sdfrate"
local J = require "common"
local err = J.err
local Uniform = require "uniform"

local H = {}

@@ -40,8 +41,8 @@ function H.verilogOnly(filename, hsfn, inputFilename, tapType, tapValue, inputTy
assert( tapType==nil or types.isType(tapType) )
if tapType~=nil then tapType:checkLuaValue(tapValue) end
assert( types.isType(outputType) )
assert(type(inputW)=="number")
assert(type(outputH)=="number")
assert(Uniform(inputW):isNumber())
assert(Uniform(outputH):isNumber())
assert(type(inputFilename)=="string")
err(R.isFunction(hsfn), "second argument to harness.axi must be function")
--assert(earlyOverride==nil or type(earlyOverride)=="number")
@@ -104,9 +105,9 @@ function harnessTop(t)
err( R.isBasic(iover), "Harness error: iover ended up being handshake?")
err( R.isBasic(oover), "Harness error: oover ended up being handshake?")

err( (t.inSize[1]*t.inSize[2]) % inputP == 0, "Error, # of input tokens is non-integer, inSize={"..tostring(t.inSize[1])..","..tostring(t.inSize[2]).."}, inputP="..tostring(inputP))
err( Uniform((t.inSize[1]*t.inSize[2]) % inputP):eq(0):assertAlwaysTrue(), "Error, # of input tokens is non-integer, inSize={"..tostring(t.inSize[1])..","..tostring(t.inSize[2]).."}, inputP="..tostring(inputP))
local inputCount = (t.inSize[1]*t.inSize[2])/inputP
err( (t.outSize[1]*t.outSize[2]) % outputP == 0, "Error, # of output tokens is non-integer, outSize:"..tostring(t.outSize[1]).."x"..tostring(t.outSize[2]).." outputP:"..tostring(outputP) )
err( Uniform((t.outSize[1]*t.outSize[2]) % outputP):eq(0):assertAlwaysTrue(), "Error, # of output tokens is non-integer, outSize:"..tostring(t.outSize[1]).."x"..tostring(t.outSize[2]).." outputP:"..tostring(outputP) )

local outputCountFrac = {t.outSize[1]*t.outSize[2], outputP}

@@ -136,14 +137,14 @@ function harnessTop(t)

if fn.sdfInput~=nil then
assert(#fn.sdfInput==1)
MD.sdfInputN = fn.sdfInput[1][1]
MD.sdfInputD = fn.sdfInput[1][2]
MD.sdfInputN = Uniform(fn.sdfInput[1][1]):toUnescapedString()
MD.sdfInputD = Uniform(fn.sdfInput[1][2]):toUnescapedString()
end

if fn.sdfOutput~=nil then
assert(#fn.sdfOutput==1)
MD.sdfOutputN = fn.sdfOutput[1][1]
MD.sdfOutputD = fn.sdfOutput[1][2]
MD.sdfOutputN = Uniform(fn.sdfOutput[1][1]):toUnescapedString()
MD.sdfOutputD = Uniform(fn.sdfOutput[1][2]):toUnescapedString()
end

MD.earlyOverride=t.earlyOverride
@@ -4,6 +4,7 @@ local SOC = require "soc"
local J = require "common"
local SDF = require "sdfrate"
local types = require "types"
local Uniform = require "uniform"

return function(fn,t)
if R.isFunction(fn)==false then
@@ -49,20 +50,32 @@ return function(fn,t)
if fn.globalMetadata["MAXI"..i.."_read_filename"]~=nil then
local rlist = {}
table.insert(rlist,"filename='"..fn.globalMetadata["MAXI"..i.."_read_filename"].."'")
if fn.globalMetadata["MAXI"..i.."_read_W"]~=nil then table.insert(rlist,"W="..fn.globalMetadata["MAXI"..i.."_read_W"]) end
if fn.globalMetadata["MAXI"..i.."_read_H"]~=nil then table.insert(rlist,"H="..fn.globalMetadata["MAXI"..i.."_read_H"]) end
if fn.globalMetadata["MAXI"..i.."_read_W"]~=nil then table.insert(rlist,"W="..Uniform(fn.globalMetadata["MAXI"..i.."_read_W"]):toEscapedString()) end
if fn.globalMetadata["MAXI"..i.."_read_H"]~=nil then table.insert(rlist,"H="..Uniform(fn.globalMetadata["MAXI"..i.."_read_H"]):toEscapedString()) end
if fn.globalMetadata["MAXI"..i.."_read_bitsPerPixel"]~=nil then table.insert(rlist,"bitsPerPixel="..fn.globalMetadata["MAXI"..i.."_read_bitsPerPixel"]) end
if fn.globalMetadata["MAXI"..i.."_read_V"]~=nil then table.insert(rlist,"V="..fn.globalMetadata["MAXI"..i.."_read_V"]) end
J.err(fn.globalMetadata["MAXI"..i.."_read_address"]~=nil,"Error: AXI port "..tostring(i).." was given a filename, but no address?")
table.insert(rlist,"address=0x"..string.format("%x",fn.globalMetadata["MAXI"..i.."_read_address"]))

table.insert(rlist,"address="..Uniform(fn.globalMetadata["MAXI"..i.."_read_address"]):toEscapedString() )
table.insert(inputList, "{"..table.concat(rlist,",").."}")
end
end

local outputList = {}
for i=0,SOC.ports do
if fn.globalMetadata["MAXI"..i.."_write_filename"]~=nil then
table.insert(outputList,"{filename='"..fn.globalMetadata["MAXI"..i.."_write_filename"].."',W="..fn.globalMetadata["MAXI"..i.."_write_W"]..",H="..fn.globalMetadata["MAXI"..i.."_write_H"]..",bitsPerPixel="..fn.globalMetadata["MAXI"..i.."_write_bitsPerPixel"]..",V="..fn.globalMetadata["MAXI"..i.."_write_V"]..",address=0x"..string.format("%x",fn.globalMetadata["MAXI"..i.."_write_address"]).."}")
local wlist = {}

table.insert(wlist,"filename='"..fn.globalMetadata["MAXI"..i.."_write_filename"].."'")
if fn.globalMetadata["MAXI"..i.."_write_W"]~=nil then table.insert(wlist,"W="..fn.globalMetadata["MAXI"..i.."_write_W"]) end
if fn.globalMetadata["MAXI"..i.."_write_H"]~=nil then table.insert(wlist,"H="..fn.globalMetadata["MAXI"..i.."_write_H"]) end
if fn.globalMetadata["MAXI"..i.."_write_bitsPerPixel"]~=nil then table.insert(wlist,"bitsPerPixel="..fn.globalMetadata["MAXI"..i.."_write_bitsPerPixel"]) end
if fn.globalMetadata["MAXI"..i.."_write_V"]~=nil then table.insert(wlist,"V="..fn.globalMetadata["MAXI"..i.."_write_V"]) end

J.err(fn.globalMetadata["MAXI"..i.."_write_address"]~=nil,"Error: AXI write port "..tostring(i).." was given a filename, but no address?")
table.insert( wlist, "address="..Uniform(fn.globalMetadata["MAXI"..i.."_write_address"]):toEscapedString() )

table.insert(outputList, "{"..table.concat(wlist,",").."}")
end
end

@@ -86,8 +99,11 @@ return function(fn,t)

local cyc = (fn.sdfInput[1][2]/fn.sdfInput[1][1])
if t~=nil and t.cycles~=nil then cyc=t.cycles end

J.err( type(SOC.currentAddr)=="number","SOC.currentAddr should be a number?")
J.err(SOC.currentAddr ~= 0x30008000,"SOC.currentAddr should imply a segment size > 0?")

f:write( "return {inputs={"..table.concat(inputList,",").."},outputs={"..table.concat(outputList,",").."},topModule='"..fn.name.."',memoryStart=0x30008000,memoryEnd=0x"..string.format("%x",SOC.currentAddr)..",cycles="..cyc..registerList..registerNames.."}" )
f:write( "return {inputs={"..table.concat(inputList,",").."},outputs={"..table.concat(outputList,",").."},topModule='"..fn.name.."',memoryStart=0x30008000,memoryEnd=0x"..string.format("%x",SOC.currentAddr)..",cycles="..Uniform(cyc):toEscapedString()..registerList..registerNames.."}" )
f:close()
elseif backend=="terra" then
local doTerraSim = require("harnessTerraSOC")
@@ -4,6 +4,7 @@ local cstdlib = terralib.includec("stdlib.h")
local cstdio = terralib.includec("stdio.h")
local clocale = terralib.includec("locale.h")
local J = require "common"
local Uniform = require "uniform"

local data = macro(function(i) return `i._0 end)
local valid = macro(function(i) return `i._1 end)
@@ -39,7 +40,8 @@ void enableCommas(){setlocale(LC_NUMERIC, "");}
local currentTimeInSeconds = Ctmp.CurrentTimeInSecondsHT

return function(top, options)
local simCycles = top.sdfInput[1][2]/top.sdfInput[1][1]

local simCycles = (top.sdfInput[1][2]):toNumber()/(top.sdfInput[1][1]):toNumber()
if options~=nil and options.cycles~=nil then simCycles = options.cycles end
local extraCycles = math.max(math.floor(simCycles/10),1024)

@@ -129,14 +131,14 @@ return function(top, options)
local clearOutputs = {}
for i=0,SOC.ports do
if top.globalMetadata["MAXI"..i.."_read_filename"]~=nil then
table.insert( readS, quote V.loadFile([top.globalMetadata["MAXI"..i.."_read_filename"]], memory, [top.globalMetadata["MAXI"..i.."_read_address"]-MEMBASE]) end )
table.insert( readS, quote V.loadFile([top.globalMetadata["MAXI"..i.."_read_filename"]], memory, [Uniform(top.globalMetadata["MAXI"..i.."_read_address"]-MEMBASE):toTerra()]) end )
end

if top.globalMetadata["MAXI"..i.."_write_filename"]~=nil then
local bytes = (top.globalMetadata["MAXI"..i.."_write_W"]*top.globalMetadata["MAXI"..i.."_write_H"]*top.globalMetadata["MAXI"..i.."_write_bitsPerPixel"])/8
table.insert( writeS, quote V.saveFile([top.globalMetadata["MAXI"..i.."_write_filename"]..".terra.raw"], memory, [top.globalMetadata["MAXI"..i.."_write_address"]-MEMBASE],bytes) end )
table.insert( writeS, quote V.saveFile([top.globalMetadata["MAXI"..i.."_write_filename"]..".terra.raw"], memory, [Uniform(top.globalMetadata["MAXI"..i.."_write_address"]-MEMBASE):toTerra()],bytes) end )

table.insert( clearOutputs, quote for ii=0,[bytes],4 do @[&uint32](memory+[top.globalMetadata["MAXI"..i.."_write_address"]-MEMBASE]+ii)=0x0df0adba; end end )
table.insert( clearOutputs, quote for ii=0,[bytes],4 do @[&uint32](memory+[Uniform(top.globalMetadata["MAXI"..i.."_write_address"]-MEMBASE):toTerra()]+ii)=0x0df0adba; end end )
end
end

@@ -158,23 +160,6 @@ return function(top, options)
data([top:getGlobal("IP_SAXI0_WDATA"):terraValue()]) = writeData;
valid([top:getGlobal("IP_SAXI0_WDATA"):terraValue()]) = true;

--------------------------------------------------- step
--[=[
m:calculateReady()
m:process(nil,nil)
if verbose then V.printSlave(S0LIST); end
var found = V.checkSlaveWriteResponse(S0LIST);
if [top:getGlobal("IP_SAXI0_WDATA"):terraReady()]==false then
cstdio.printf("IP_SAXI0_WREADY should be true\n");
cstdlib.exit(1)
end
data([top:getGlobal("IP_SAXI0_WDATA"):terraValue()]) = writeData;
valid([top:getGlobal("IP_SAXI0_WDATA"):terraValue()]) = true;
]=]

--------------------------------------------------- step
m:calculateReady()
m:process(nil,nil)
@@ -233,15 +218,12 @@ return function(top, options)

var [memory] = [&uint8](cstdlib.malloc(MEMSIZE))

readS

V.init()

var ROUNDS = 2
for round=0,ROUNDS do
if verbose then cstdio.printf("ROUND %d\n",round) end

clearOutputs

V.deactivateMasterRead([MREAD_SLAVEOUT[0]])
V.deactivateMasterWrite([MWRITE_SLAVEOUT[0]])
@@ -251,9 +233,9 @@ return function(top, options)

var cycle = 0

-- if round==0 then
[setTaps]
-- end
[setTaps]
[clearOutputs]
[readS]

setReg( IP_CLK, IP_ARESET_N, m, 0xA0000000, 1 )

@@ -1,7 +1,7 @@
BUILDDIR ?= out

# soc_flipWrite.lua
SRCS_SOC = soc_simple.lua soc_2in.lua soc_convgen.lua soc_convgenTaps.lua soc_flip.lua soc_15x15.lua soc_15x15x15.lua soc_flipWrite.lua soc_regin.lua soc_regout.lua soc_convtest.lua soc_read.lua soc_redu1024.lua soc_redu2048.lua soc_redu4096.lua soc_redu8192.lua soc_redu16384.lua soc_redu32768.lua soc_sort.lua soc_filterseq.lua soc_filterseq8.lua soc_unaligned.lua soc_underflow.lua soc_parread.lua soc_tokencounter.lua
SRCS_SOC = soc_simple.lua soc_simple_uniform.lua soc_2in.lua soc_convgen.lua soc_convgenTaps.lua soc_flip.lua soc_15x15.lua soc_15x15x15.lua soc_flipWrite.lua soc_regin.lua soc_regout.lua soc_convtest.lua soc_read.lua soc_redu1024.lua soc_redu2048.lua soc_redu4096.lua soc_redu8192.lua soc_redu16384.lua soc_redu32768.lua soc_sort.lua soc_filterseq.lua soc_filterseq8.lua soc_unaligned.lua soc_underflow.lua soc_parread.lua soc_tokencounter.lua

VERILATOR_SOC = $(patsubst %.lua,$(BUILDDIR)/%.verilatorSOC.bit,$(SRCS_SOC))
VERILATOR_SOC += $(patsubst %.lua,$(BUILDDIR)/%.verilatorSOC.raw,$(SRCS_SOC))
@@ -0,0 +1,31 @@
local R = require "rigel"
local SOC = require "soc"
local C = require "examplescommon"
local harness = require "harnessSOC"
local G = require "generators"
local RS = require "rigelSimple"
local types = require "types"
types.export()

Regs = SOC.axiRegs{readAddress={u(32),0x30008000},writeAddress={u(32),0x30008000+(128*64)}}
regs = Regs:instantiate()

OffsetModule = G.Module{ "OffsetModule", R.HandshakeTrigger,
function(i)
local readStream = SOC.axiBurstReadN("frame_128.raw",128*64,0,Regs.readAddress.global)(i)
readStream = G.HS{C.bitcast(b(64),ar(u(8),8))}(readStream)
local offset = G.HS{G.Map{G.Add{200}}}(readStream)
offset = G.HS{C.bitcast(ar(u(8),8),b(64))}(offset)
return SOC.axiBurstWriteN("out/soc_simple_uniform",128*64,0,Regs.writeAddress.global)(offset)
end}

--print(OffsetModule)
--print(OffsetModule:toVerilog())

-- tell the system how much memory we want
SOC.currentAddr = 0x3000c000
print(OffsetModule)
OffsetModule.globalMetadata["MAXI0_write_W"]=128
OffsetModule.globalMetadata["MAXI0_write_H"]=64

harness{regs.start, OffsetModule, regs.done}
@@ -8,14 +8,13 @@ function top(inp)
local pos = HS(posSeq{size={W,H},V=1},false)()
pos.name="POSSEQ"
pos.sdfRateOverride={{1,1}}
print("POSDONE")

local start = liftMath(function(x) return x:index(1):index(0):index(0):removeMSBs(8) end)(inp,pos)
start.name="START"
print("LIFTDONE",start.type)

local tc = triggeredCounter(N)(start)
tc.name="TC"
return tc
-- return start
end


@@ -6,7 +6,9 @@ function basename(fn)
end

if arg[2]=="memoryStart" or arg[2]=="memoryEnd" then
print(string.format("%x",metadata[arg[2]]))
if metadata[arg[2]]~=nil then
print("--"..arg[2].." "..string.format("%x",metadata[arg[2]]))
end
elseif arg[2]=="__INPUT_HOST_FILES" or arg[2]=="__INPUT_DEVICE_FILES" then
local str = ""
for _,v in ipairs(metadata.inputs) do
@@ -23,7 +25,16 @@ elseif arg[2]=="__INPUTS" or arg[2]=="__INPUTS_ZYNQ" then
for _,v in ipairs(metadata.inputs) do
local fn = v.filename
if arg[2]=="__INPUTS_ZYNQ" then fn=basename(fn) end
str = str..fn.." 0x"..string.format("%x",v.address).." "

if type(v.address)=="number" then
str = str..fn.." 0x"..string.format("%x",v.address).." "
else
local regAddress = metadata.registers[v.address]
if regAddress==nil then print("Could not find register"); assert(false) end
--str = str..fn.." reg:0x"..string.format("%x",regAddress).." "
-- HACK: b/c this is set by the harness, just load the default address
str = str..fn.." 0x"..metadata.registerValues[regAddress].." "
end
end
print(str)
elseif arg[2]=="__OUTPUTS" or arg[2]=="__OUTPUTS_ZYNQ" then
@@ -32,7 +43,17 @@ elseif arg[2]=="__OUTPUTS" or arg[2]=="__OUTPUTS_ZYNQ" then
for _,v in ipairs(metadata.outputs) do
local fn = v.filename
if arg[2]=="__OUTPUTS_ZYNQ" then fn=basename(fn) end
str = str..fn.." 0x"..string.format("%x",v.address).." "..v.W.." "..v.H.." "..v.bitsPerPixel.." "
str = str..fn.." "

if type(v.address)=="number" then
str = str.."0x"..string.format("%x",v.address)
else
local regAddress = metadata.registers[v.address]
if regAddress==nil then print("Could not find register"); assert(false) end
str = str.." reg:0x"..string.format("%x",regAddress).." "
end

str = str.." "..v.W.." "..v.H.." "..v.bitsPerPixel.." "
end
print(str)
elseif arg[2]=="__REGISTERS" then
Oops, something went wrong.

0 comments on commit f47a72e

Please sign in to comment.