Add example of customising the iterative-deepening parameters

Author: mn416

StackExample.bsv

@@ -248,6 +248,25 @@ module [Module] testStackID ();
   blueCheckID(checkStackWithReset(r.new_rst), r);
 endmodule
 
+// Iterative deepening version (with extra options)
+module [Module] testStackIDCustom ();
+  Clock clk <- exposeCurrentClock;
+  MakeResetIfc r <- mkReset(0, True, clk);
+
+  // Customise default BlueCheck parameters
+  BlueCheck_Params params = bcParamsID(r);
+  params.wedgeDetect      = True;
+  params.id.initialDepth  = 3;
+  function incr(x)        = x+1;
+  params.id.incDepth      = incr;
+  params.numIterations    = 25;
+  params.id.testsPerDepth = 100;
+
+  // Generate checker
+  Stmt s <- mkModelChecker(checkStackWithReset(r.new_rst), params);
+  mkAutoFSM(s);
+endmodule
+
 // Iterative deepening version & classification
 module [Module] testStackIDClassify ();
   Clock clk <- exposeCurrentClock;

clean.sh

@@ -38,6 +38,7 @@ rm -f *.cxx *.o *.h *.ba *.bo *.so
 rm -f State.txt
 rm -f testStack
 rm -f testStackID
+rm -f testStackIDCustom
 rm -f testStackAlg
 rm -f testStackAlgID
 rm -f testStackIDClassify

make.sh

@@ -53,6 +53,7 @@ echo "(7) Stack(algebraic)"
 echo "(8) Stack(algebraic) + ID"
 echo "(9) Stack(synthesisable)"
 echo "(10) Stack(synthesisable) + ID"
+echo "(11) Stack + ID + custom parameters"
 
 read OPTION
 case "$OPTION" in
@@ -88,6 +89,9 @@ case "$OPTION" in
      TOPMOD=testStackID
      SYNTH=1
      ;;
+ 11) TOPFILE=StackExample.bsv
+     TOPMOD=testStackIDCustom
+     ;;
   *) echo "Option not recognised"
      exit
      ;;