Re-structure project to be more like Blarney and remove temp files us…

…ed for writing diss

.gitignore

@@ -1,23 +1,2 @@
-dist
-dist-*
-cabal-dev
-*.o
 *.hi
-*.hie
-*.chi
-*.chs.h
-*.dyn_o
-*.dyn_hi
-.hpc
-.hsenv
-.cabal-sandbox/
-cabal.sandbox.config
-*.prof
-*.aux
-*.hp
-*.eventlog
-.stack-work/
-cabal.project.local
-cabal.project.local~
-.HTF/
-.ghc.environment.*
+*.o

.gitmodules

@@ -1,3 +1,4 @@
-[submodule "work/blarney"]
-	path = work/blarney
-	url = https://github.com/mn416/blarney
+[submodule "blarney"]
+	path = blarney
+	url = https://github.com/JonasAlaif/blarney.git
+	branch = jf613-change-test-script

Documentation/README.md

@@ -0,0 +1 @@
+A read-only copy of the source latex can be found at https://www.overleaf.com/project/5e30193d717c320001b14145

work/BuggySuite/ActoraStack.hs → Examples/ActoraStack/ActoraStack.hs

@@ -68,8 +68,8 @@ makeStackSpec = do
 
 testBench :: Module ()
 testBench = do
-  stkGolden :: Stack 3 (Bit 2) <- makeStackSpec
-  stkActora :: Stack 3 (Bit 2) <- makeStack
+  stkGolden :: Stack 3 (Bit 1) <- makeStackSpec
+  stkActora :: Stack 3 (Bit 1) <- makeStack
   -- Note 3: Cannot copy top two elements from stack
   maxSize :: Reg (Bit 3) <- makeReg 0
   topTwo :: Reg (Bit 2) <- makeReg 0
@@ -145,4 +145,4 @@ testBench = do
 -- ===============
 
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "ActoraStack-Verilog/"

Examples/ActoraStack/ActoraStack.out

@@ -0,0 +1,3 @@
+- All tests passed to depth 0 at time 0 -
+- All tests passed to depth 1 at time 76 -
+=== All tests passed to maximum specified depth of 2 at time 4408 ===

Examples/ActoraStack/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) ActoraStack.hs
+
+clean:
+	rm -rf *.o *.hi ActoraStack ActoraStack-Verilog

work/BuggySuite/BRAMStack.hs → Examples/BRAMStack/BRAMStack.hs

@@ -88,8 +88,8 @@ makeStackSpec logSize =
 -- Top-level module
 testBench :: Module ()
 testBench = do
-  stkGolden :: Stack (Bit 5) <- makeStackSpec 5
-  stkBRAM :: Stack (Bit 5) <- makeBRAMStack 5
+  stkGolden :: Stack (Bit 2) <- makeStackSpec 5
+  stkBRAM :: Stack (Bit 2) <- makeBRAMStack 5
 
   let topEq = stkGolden.top .==. stkBRAM.top
   let prop_TopEq = Assert' (stkGolden.isEmpty .|. topEq) (display_ (stkGolden.top) " v " (stkBRAM.top))
@@ -115,4 +115,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "BRAMStack-Verilog/"

Examples/BRAMStack/BRAMStack.out

@@ -0,0 +1,12 @@
+- All tests passed to depth 0 at time 0 -
+- All tests passed to depth 1 at time 10 -
+- All tests passed to depth 2 at time 85 -
+- All tests passed to depth 3 at time 585 -
+- All tests passed to depth 4 at time 3710 -
+=== Found failing case at depth 5 after 21722 ticks: TopEq {1 v 0} ===
+0: Push 0x1
+1: Push 0x0
+2: Push 0x0
+3: Pop
+4: Pop
+5: 'TopEq {1 v 0}' fails

Examples/BRAMStack/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) BRAMStack.hs
+
+clean:
+	rm -rf *.o *.hi BRAMStack BRAMStack-Verilog

work/BuggySuite/CPU.hs → Examples/CPU/CPU.hs

@@ -44,16 +44,21 @@ testBench = do
                             ]
 
   let prop_hazard = Forall \(StoreInstr si1 :: StoreInstr) -> Forall \(branchOffset :: Bit 4) ->
-                      Forall \(StoreInstr si2 :: StoreInstr) -> Forall \(two :: Bit 1) -> WhenRecipe true do
+                   -- Forall \(StoreInstr si2 :: StoreInstr) -- Takes too long to simulate
+                      Forall \(si2rD :: RegId)
+                      -> Forall \(two :: Bit 1) -> WhenRecipe true do
                         Seq [ Action do (instr <== si1)
                             , Action do (instr <== 0b10 # branchOffset # si1.rD) -- si1.rD => Data hazard
-                            , If two (Action (instr <== nop)) (Action noAction) -- Delay next instruction by either 0 or 1 clocks
-                            , Action do (instr <== si2) -- Branched? => Control hazard 1 or 2 cycles after branch
+                            , If two (Action (instr <== nop)) Skip -- Delay next instruction by either 0 or 1 clocks
+                         -- , Action do (instr <== si2) -- Branched? => Control hazard 1 or 2 cycles after branch
+                            , Action do (instr <== 0b00 # si2rD # (0b1111 :: Bit 4))
                             , Action do
                                 when (si1.imm .==. 0) do
                                   -- If didn't branch si2 must have an effect
-                                  correctVal <== si2.imm.zeroExtend
-                                  correctDest <== si2.rD
+                               -- correctVal <== si2.imm.zeroExtend
+                               -- correctDest <== si2.rD
+                                  correctVal <== 0b1111
+                                  correctDest <== si2rD
                                 -- Took (4 + two) cycles to execute, however flush sets pc back by 3 cycles, also subtract jump
                                 correctPc <== correctPc.val + two.zeroExtend + (si1.imm .==. 0 ? (4, 1 - branchOffset.zeroExtend))
                             ]
@@ -93,4 +98,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "CPU-Verilog/"

Examples/CPU/CPU.out

@@ -0,0 +1,2 @@
+- All tests passed to depth 0 at time 0 -
+=== All tests passed to maximum specified depth of 1 at time 127168 ===

Examples/CPU/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) CPU.hs
+
+clean:
+	rm -rf *.o *.hi CPU CPU-Verilog

work/BuggySuite/FirstHot.hs → Examples/FirstHot/FirstHot.hs

@@ -11,9 +11,9 @@ countOnes b = b.toBitList.(map zeroExtend).sumList
 
 testBench :: Module ()
 testBench = do
-  let prop_OneIsHot =     Forall \(x :: Bit 30) -> Assert ((x .==. 0 ? (0, 1)) .==. countOnes (firstHot x))
-  let prop_HotBitCommon = Forall \(x :: Bit 30) -> Assert (x .&. (firstHot x) .==. (firstHot x))
-  let prop_HotBitFirst =  Forall \(x :: Bit 30) -> Assert (x .&. ((firstHot x) - 1) .==. 0)
+  let prop_OneIsHot =     Forall \(x :: Bit 25) -> Assert ((x .==. 0 ? (0, 1)) .==. countOnes (firstHot x))
+  let prop_HotBitCommon = Forall \(x :: Bit 25) -> Assert (x .&. (firstHot x) .==. (firstHot x))
+  let prop_HotBitFirst =  Forall \(x :: Bit 25) -> Assert (x .&. ((firstHot x) - 1) .==. 0)
 
   let properties = [
           ("OneIsHot", prop_OneIsHot)
@@ -28,4 +28,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "FirstHot-Verilog/"

Examples/FirstHot/FirstHot.out

@@ -0,0 +1 @@
+--All tests passed at time 33554431--

Examples/FirstHot/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) FirstHot.hs
+
+clean:
+	rm -rf *.o *.hi FirstHot FirstHot-Verilog

Examples/Makefile

@@ -0,0 +1,15 @@
+top:
+
+.PHONY: clean
+clean:
+	make -C ActoraStack clean
+	make -C BRAMStack clean
+	make -C CPU clean
+	make -C FirstHot clean
+	make -C MemAddr clean
+	make -C RandomCheck clean
+	make -C Sorter clean
+	make -C Sums clean
+	make -C Sums_Parallel clean
+	make -C Synthesizable clean
+

Examples/MemAddr/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) MemAddr.hs
+
+clean:
+	rm -rf *.o *.hi MemAddr MemAddr-Verilog

work/BuggySuite/MemAddr.hs → Examples/MemAddr/MemAddr.hs

@@ -1,7 +1,7 @@
 import Blarney
 import BlarneyCheck
 
-newtype MemAddr = MemAddr (Bit 21) deriving (Generic, Bits)
+newtype MemAddr = MemAddr (Bit 32) deriving (Generic, Bits)
 
 instance Generator MemAddr where
   -- Initial value is 0x0...0FFF
@@ -11,7 +11,7 @@ instance Generator MemAddr where
   -- Done when all bits are ones
   isFinal current = pack current .==. ones
   -- Number of possible values = 2^(41-12)
-  range = 2^29
+  range = 2^20
 
 testBench :: Module ()
 testBench = do
@@ -25,4 +25,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "MemAddr-Verilog/"

Examples/MemAddr/MemAddr.out

@@ -0,0 +1 @@
+--All tests passed at time 1048575--

Examples/RandomCheck/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) RandomCheck.hs
+
+clean:
+	rm -rf *.o *.hi RandomCheck RandomCheck-Verilog

work/BuggySuite/RandomCheck.hs → Examples/RandomCheck/RandomCheck.hs

@@ -43,4 +43,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "RandomCheck-Verilog/"

Examples/RandomCheck/RandomCheck.out

@@ -0,0 +1,8 @@
+- All tests passed to depth 0 at time 0 -
+Custom Random Values:
+00, 01, c6, 5f, 1c, 8d, 82, 0b, 78, 59, 7e, f7, 14, 65, ba, 23, f0, b1, 36, 8f, 0c, 3d, f2, 3b, 68, 09, ee, 27, 04, 15, 2a, 53, e0, 61, a6, bf, fc, ed, 62, 6b, 58, b9, 5e, 57, f4, c5, 9a, 83, d0, 11, 16, ef, ec, 9d, d2, 9b, 48, 69, ce, 87, e4, 75, 0a, b3, c0, c1, 86, 1f, dc, 4d, 42, cb, 38, 19, 3e, b7, d4, 25, 7a, e3, b0, 71, f6, 4f, cc, fd, b2, fb, 28, c9, ae, e7, c4, d5, ea, 13, a0, 21, 66, 7f, bc, ad, 22, 2b, 18, 79, 1e, 17, b4, 85, 5a, 43, 90, d1, d6, af, ac, 5d, 92, 5b, 08, 29, 8e, 47, a4, 35, ca, 73, 80, 81, 46, df, 9c, 0d, 02, 8b, f8, d9, fe, 77, 94, e5, 3a, a3, 70, 31, b6, 0f, 8c, bd, 72, bb, e8, 89, 6e, a7, 84, 95, aa, d3, 60, e1, 26, 3f, 7c, 6d, e2, eb, d8, 39, de, d7, 74, 45, 1a, 03, 50, 91, 96, 6f, 6c, 1d, 52, 1b, c8, e9, 4e, 07, 64, f5, 8a, 33, 40, 41, 06, 9f, 5c, cd, c2, 4b, b8, 99, be, 37, 54, a5, fa, 63, 30, f1, 76, cf, 4c, 7d, 32, 7b, a8, 49, 2e, 67, 44, 55, 6a, 93, 20, a1, e6, ff, 3c, 2d, a2, ab, 98, f9, 9e, 97, 34, 05, da, c3, 10, 51, 56, 2f, 2c, dd, 12, db, 88, a9, 0e, c7, 24, b5, 4a, f3, 
+
+Builtin Random:
+=== Found failing case at depth 1 after 532 ticks: Fail only at large value ===
+0: Builtin_Random 0xe81de362a1f9f35f
+1: 'Fail only at large value' fails

Examples/Sorter/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) Sorter.hs
+
+clean:
+	rm -rf *.o *.hi Sorter Sorter-Verilog

work/BuggySuite/Sorter.hs → Examples/Sorter/Sorter.hs

@@ -107,7 +107,7 @@ allDifferent (x:xs) = allDifferent xs .&. different xs
 
 testBench :: Module ()
 testBench = do
-  let prop_Sorted = ForallList 27 \(xs :: [Bit 1]) -> Assert (xs.sort3.isSorted)
+  let prop_Sorted = ForallList 22 \(xs :: [Bit 1]) -> Assert (xs.sort3.isSorted)
 
   -- Useful for forcing error to be found for list with unique values:
 --let prop_Sorted = ForallList 8 \(xs :: [Bit 3]) -> Assert' (xs.allDifferent.inv .|. xs.sort2.isSorted) (display_ $ xs.sort2)
@@ -121,4 +121,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "Sorter-Verilog/"

Examples/Sorter/Sorter.out

@@ -0,0 +1 @@
+--All tests passed at time 4194303--

Examples/Sums/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) Sums.hs
+
+clean:
+	rm -rf *.o *.hi Sums Sums-Verilog

work/BuggySuite/Sums.hs → Examples/Sums/Sums.hs

@@ -3,8 +3,8 @@ import BlarneyCheck
 
 testBench :: Module ()
 testBench = do
-  let prop_Associativity = Forall \(x :: Bit 10) -> Forall \y -> Forall \z -> Assert ((x + y) + z .==. x + (y + z))
-  let prop_Commutativity = Forall \(x :: Bit 15) -> Forall \y ->              Assert (x + y .==. y + x)
+  let prop_Associativity = Forall \(x :: Bit  8) -> Forall \y -> Forall \z -> Assert ((x + y) + z .==. x + (y + z))
+  let prop_Commutativity = Forall \(x :: Bit 12) -> Forall \y ->              Assert (x + y .==. y + x)
   -- Flawed assumption of Commutativity of subtraction:
 --let prop_SubComm =       Forall \(x :: Bit 15) -> Forall \y ->              Assert (x - y .==. y - x)
 
@@ -20,4 +20,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "Sums-Verilog/"

Examples/Sums/Sums.out

@@ -0,0 +1 @@
+--All tests passed at time 16777215--

Examples/Sums_Parallel/Makefile

@@ -0,0 +1,6 @@
+.PHONY: all
+all:
+	blcc $(BLC_FLAGS) Sums_Parallel.hs
+
+clean:
+	rm -rf *.o *.hi Sums_Parallel Sums_Parallel-Verilog

work/BuggySuite/Sums_Parallel.hs → Examples/Sums_Parallel/Sums_Parallel.hs

@@ -30,10 +30,10 @@ instance KnownNat n => Generator (Upper n) where
 
 testBench :: Module ()
 testBench = do
-  let prop_Associativity1 = Forall \(Lower x) -> Forall \(y :: Bit 10) -> Forall \z -> Assert ((x + y) + z .==. x + (y + z))
-  let prop_Associativity2 = Forall \(Upper x) -> Forall \(y :: Bit 10) -> Forall \z -> Assert ((x + y) + z .==. x + (y + z))
-  let prop_Commutativity1 = Forall \(Lower x) -> Forall \(y :: Bit 15) ->              Assert (x + y .==. y + x)
-  let prop_Commutativity2 = Forall \(Upper x) -> Forall \(y :: Bit 15) ->              Assert (x + y .==. y + x)
+  let prop_Associativity1 = Forall \(Lower x) -> Forall \(y :: Bit  8) -> Forall \z -> Assert ((x + y) + z .==. x + (y + z))
+  let prop_Associativity2 = Forall \(Upper x) -> Forall \(y :: Bit  8) -> Forall \z -> Assert ((x + y) + z .==. x + (y + z))
+  let prop_Commutativity1 = Forall \(Lower x) -> Forall \(y :: Bit 12) ->              Assert (x + y .==. y + x)
+  let prop_Commutativity2 = Forall \(Upper x) -> Forall \(y :: Bit 12) ->              Assert (x + y .==. y + x)
 
   let properties = [
           ("Associativity1", prop_Associativity1)
@@ -49,4 +49,4 @@ testBench = do
 
 -- Code generation
 main :: IO ()
-main = writeVerilogTop testBench "top" "Out-Verilog/"
+main = writeVerilogTop testBench "top" "Sums_Parallel-Verilog/"

Examples/Sums_Parallel/Sums_Parallel.out

@@ -0,0 +1 @@
+--All tests passed at time 8388607--

Examples/Synthesizable/.gitignore

@@ -0,0 +1,24 @@
+
+/*.rpt
+/*.msg
+/*.summary
+/*.sld
+/*.sopcinfo
+/*.jdi
+/c5_pin_model_dump.txt
+/*.pin
+/*.done
+/*.qws
+/*.sof
+/*.csv
+/*.qws
+/*.smsg
+/*.qdf
+**/dse*
+**/db
+**/incremental_db
+**/SoC
+**/.qsys_edit
+**/reconfig_mif
+/*.mif
+

work/CheckFPGA_CPU/Makefile → Examples/Synthesizable/Makefile

@@ -2,21 +2,20 @@ ifndef QUARTUS_ROOTDIR
   $(error Please set QUARTUS_ROOTDIR)
 endif
 
-.PHONY: one
-one: 
-	make -C Src
+%.sof:
+	make -C Src Top-Verilog/$*.v
 	qsys-generate -syn SoC.qsys
 	quartus_sh --flow compile SoCKitTop.qpf
 
-.PHONY: dse
-dse:
-	make -C Src
+%.dse:
+	make -C Src Top-Verilog/$*.v
 	qsys-generate -syn SoC.qsys
-	"../../Temp/copy_bram_files.sh" &
+	"./copy_bram_files.sh" &
 	quartus_dse SoCKitTop.qpf    \
 	    --num-seeds 15              \
 	    --launcher local            \
 	    --num-concurrent 4
+
 .PHONY: report
 report:
 	quartus_dse SoCKitTop.qpf --report utilization

Examples/Synthesizable/Src/Makefile

@@ -0,0 +1,8 @@
+%.bin: %.hs
+	blcc -i"./../../$*" $< -o $@
+Top-Verilog/%.v: %.bin
+	./$<
+	#cp $@ Top-Verilog/Top.v ??
+
+clean:
+	rm -rf *.o *.hi *.bin Top-Verilog