synth: test sha3 testbench

ekiwi · Nov 29, 2023 · 2beeace · 2beeace
1 parent 34719a0
commit 2beeace
Show file tree

Hide file tree

Showing 3 changed files with 1,218 additions and 2 deletions.
diff --git a/synthesizer/src/maltese/app/Btor2MC.scala b/synthesizer/src/maltese/app/Btor2MC.scala
@@ -5,9 +5,9 @@
 package maltese.app
 
 import java.io.File
-
 import maltese.mc._
 import maltese.smt
+import maltese.smt.BitwuzlaSMTLib
 
 /** simple interface to all supported model checkers */
 object Btor2MC extends App {
@@ -16,7 +16,8 @@ object Btor2MC extends App {
   } else {
     val filename = os.pwd / args.head
     val sys = Btor2.load(filename)
-    val checker = new BtormcModelChecker
+    //val checker = new BtormcModelChecker
+    val checker = new SMTModelChecker(BitwuzlaSMTLib)
     check(checker, sys, kMax = -1)
   }
 

diff --git a/synthesizer/test/synth/TestbenchSimulatorTests.scala b/synthesizer/test/synth/TestbenchSimulatorTests.scala
@@ -50,6 +50,22 @@ class TestbenchSimulatorTests extends AnyFlatSpec {
     Testbench.save(CirFixDir / "opencores" / "i2c" / "fixed_x_prop_tb.csv", fixed)
   }
 
+  it should "correctly execute the sha3 test" in {
+    val tb = Testbench.load(CirFixDir / "opencores" / "sha3" / "low_throughput_core" / "keccak_tb.csv")
+
+    assert(tb.length == 358)
+
+    val sys = Btor2.load(BenchmarkDir / "keccak.original.btor")
+
+    // initialize everything to zero
+    val seed: Long = 1
+    val rnd = new scala.util.Random(seed)
+    val initialized = initSys(sys, ZeroInit, rnd)
+
+    val r = Testbench.run(initialized, tb, verbose = true, vcd = Some(os.pwd / "dump.vcd"))
+    assert(!r.failed)
+  }
+
 }
 
 private object XInputConversion {