<commit_before>// BlueCheck 0.21, <NAME>.

// Change log
// ==========
//
// 5  Nov 2012: Version 0.1
// 21 Nov 2014: Support for iterative deepening
// 28 Nov 2014: Version 0.2, with support for shrinking
// 6  Dec 2014: Save a counter-example to a file and replay it
// 16 Dec 2014: Let statements run in parallel using 'parallel' assertions

package BlueCheck;

import Randomizable  :: *;
import ModuleCollect :: *;
import StmtFSM       :: *;
import List          :: *;
import Clocks        :: *;
import FIFOF         :: *;
import ConfigReg     :: *;
import Vector        :: *;

// The max size of the log used for shrinking.  This is tricky to
// implement as a module parameter, hence it is a global parameter.
typedef 32 LogSize;
Integer logSize = valueOf(LogSize);

// The filename used to store a counter-example so it can be replayed
// in isolation in a future simulation run with debugging enabled.
String logFilename = "CounterExample.bin";

// BlueCheck module parameters
typedef struct {
  // Verbose output
  Bool verbose;

  // Display message when a chosen state does not fire
  Bool showNonFire;

  // Display message when a chosen state is a no-op
  Bool showNoOp;

  // Generate a checker based on an iterative deepening strategy
  // (If 'False', a single random state walk is performed)
  Bool useIterativeDeepening;
  // This must contain valid data if 'useIterativeDeepening' is 'True'
  ID_Params id; 

  // Interactive iterative deepening
  Bool interactive;

  // Attempt to shrink a counter example, if one is found
  // (This is only valid for iterative deepening)
  Bool useShrinking;

  // Number of testing iterations to perform. For iterative deepening,
  // this is the number of times to increase the depth before stopping
  // Otherwise, the it's the length of the random state walk
  Bit#(32) numIterations;
} BlueCheck_Params;

// Sub-parameters for iterative deepening
typedef struct {
  // Iterative deepening requires ability to reset the circuit under test
  MakeResetIfc rst;

  // The number of states to be explored in a single 'test'
  Bit#(32) initialDepth;

  // The number of tests to perform at each depth
  Bit#(32) testsPerDepth;

  // A function to increase the depth
  (function Bit#(32) f(Bit#(32) currentDepth)) incDepth;
} ID_Params;

// The maximum number of states in the equivalance checker.
// You will get a compile-time error message if this parameter
// is not big enough, but it's not likely, unless you use very
// large method frequencies.
typedef 16 LogMaxStates;
typedef UInt#(LogMaxStates) State;

// The frequency that the checker will move to particular state.
typedef Integer Frequency; // Range: 1 to 100.

// Serialise / Deserialise counter-examples ===================================

// When a counter-example is found in simulation, we can save it to a
// file so that it can be replayed in isolation in a subsequent run
// with debugging enabled.  This feature is not synthesisable, but
// it's very handy in simulation.  Thanks to <NAME> for this
// suggestion.

// Serialise data of type t to a sequence of bytes and append to a file
// (This definition is a bit obfusticated but it's the only way I
// found that doesn't introduce an ugly type constraint)
function Action putFile(File f, t data)
  provisos ( Bits#(t, width)
           , Div#(width, 8, nbytes) ) =
  action
    Bit#(TAdd#(width, 8)) block = zeroExtend(pack(data));
    Vector#(nbytes, Bit#(8)) bytes =
      unpack(block[valueOf(TMul#(nbytes, 8))-1:0]);
    for (Integer i = 0; i < valueOf(nbytes); i=i+1)
      $fwrite(f, "%c", bytes[i]);
  endaction;

// De-serialise a sequence of bytes from a file and convert to data of type t
function ActionValue#(t) getFile(File f)
  provisos ( Bits#(t, width)
           , Div#(width, 8, nbytes) ) =
    actionvalue
      Vector#(nbytes, Bit#(8)) bytes;
      for (Integer i = 0; i < valueOf(nbytes); i=i+1) begin
        int c <- $fgetc(f);
        bytes[i] = pack(c)[7:0];
      end
      return unpack(pack(bytes)[valueOf(width)-1:0]);
    endactionvalue;

// For displaying function applications =======================================

typedef struct {
  String name;
  List#(Fmt) args;
} App;

function String getName(App app) = app.name;

function Fmt formatApp(App app);
  if (app.args matches tagged Nil)
    return $format("%s", app.name);
  else 
    return ($format("%s", app.name) + fshow("(") +
            formatArgs(app.args) + fshow(")"));
endfunction

function Fmt formatArgs(List#(Fmt) args);
  if (List::tail(args) matches tagged Nil)
    return List::head(args);
  else
    return (List::head(args) + fshow(",") + formatArgs(List::tail(args)));
endfunction

function App appendArg(App app, Fmt arg) =
  App { name: app.name, args: List::append(app.args, Cons(arg, Nil)) };

// Functions for adding properties to the test bench ==========================

// A BlueCheck module implicitly collects actions, statements,
// invariants, random generators and loggers, an allowing automatic
// creation of an equivalance checker.
typedef ModuleCollect#(Item) BlueCheck;

typedef union tagged {
  Tuple3#(Frequency, App, Action) ActionItem;
  Tuple3#(Frequency, App, Stmt) StmtItem;
  Tuple2#(Bool, function Action gen(Bool replay)) RandomGenItem;
  Tuple2#(Fmt, Bool) InvariantItem;
  Tuple2#(Bool, Reg#(Bool)) EnsureItem;
  Tuple3#(Action, Action, Action) LogItem;
  (function Action save(File f)) SaveItem;
  (function Action restore(File f)) RestoreItem;
  Stmt PreStmtItem;
  Stmt PostStmtItem;
  Tuple2#(Frequency, List#(String)) ParallelItem;
} Item;

// Turn an item into a singleton action if it is an ActionItem.
function List#(Tuple3#(Frequency, App, Action)) getActionItem(Item item) =
  case (item) matches
    tagged ActionItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton action if it is an RandomGenItem.
function List#(Tuple2#(Bool, function Action gen(Bool replay)))
  getRandomGenItem(Item item) =
  case (item) matches
    tagged RandomGenItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton pair if it is an InvariantItem.
function List#(Tuple2#(Fmt, Bool)) getInvariantItem(Item item) =
  case (item) matches
    tagged InvariantItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is an StmtItem.
function List#(Tuple3#(Frequency, App, Stmt)) getStmtItem(Item item) =
  case (item) matches
    tagged StmtItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is an EnsureItem.
function List#(Tuple2#(Bool, Reg#(Bool))) getEnsureItem(Item item) =
  case (item) matches
    tagged EnsureItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is an LogItem.
function List#(Tuple3#(Action, Action, Action))
  getLogItem(Item item) =
  case (item) matches
    tagged LogItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn a save item into a singleton statement if it is a SaveItem.
function List#(function Action save(File f)) getSaveItem(Item item) =
  case (item) matches
    tagged SaveItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn a save item into a singleton statement if it is a SaveItem.
function List#(function Action restore(File f)) getRestoreItem(Item item) =
  case (item) matches
    tagged RestoreItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is a PreStmtItem.
function List#(Stmt) getPreStmtItem(Item item) =
  case (item) matches
    tagged PreStmtItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is a PostStmtItem.
function List#(Stmt) getPostStmtItem(Item item) =
  case (item) matches
    tagged PostStmtItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is a ParallelItem.
function List#(Tuple2#(Frequency, List#(String)))
    getParallelItem(Item item) =
  case (item) matches
    tagged ParallelItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// The following type class allows two functions of the same type to
// be applied to random inputs.  If the return values differ, the
// behaviour is to terminate with an error message (a counter-example
// has been found).  The probability that the equivalence will be
// checked on any given step can be specified.
typeclass Equiv#(type a);
  module [BlueCheck] eq#(App app, Frequency fr, a f, a g) ();
endtypeclass

module [BlueCheck] equiv#(String name, a f, a g) ()
    provisos(Equiv#(a));
  App app = App { name: name, args: Nil};
  eq(app, 1, f, g);
endmodule

module [BlueCheck] equivf#(Frequency fr, String name, a f, a g) ()
    provisos(Equiv#(a));
  App app = App { name: name, args: Nil};
  eq(app, fr, f, g);
endmodule

// Base case 1: execute two actions.
instance Equiv#(Action);
  module [BlueCheck] eq#(App app, Frequency fr, Action a, Action b) ();
    Action executeTwo =
      action
        a; b;
      endaction;
    addToCollection(tagged ActionItem
      (tuple3(fr, app, executeTwo)));
  endmodule
endinstance

// Base case 2: execute two action-values,
// and check equivalance of results.
instance Equiv#(ActionValue#(t))
  provisos(Eq#(t), Bits#(t, n), FShow#(t));
  module [BlueCheck] eq#(App app, Frequency fr
                                , ActionValue#(t) a
                                , ActionValue#(t) b) ();
    Wire#(Bool) success <- mkDWire(True);
    Wire#(t) aWire      <- mkDWire(?);
    Wire#(t) bWire      <- mkDWire(?);
    Fmt msg             =  fshow("Not equal: ") + fshow(aWire)
                        +  fshow(" versus ")    + fshow(bWire);

    Action executeTwoAndCheck =
      action
        t aVal <- a; aWire <= aVal;
        t bVal <- b; bWire <= bVal;
        if (aVal != bVal) success <= False;
      endaction;
      addToCollection(tagged ActionItem
        (tuple3(fr, app, executeTwoAndCheck)));
      addToCollection(tagged InvariantItem (tuple2(msg, success)));
  endmodule
endinstance

// Base case 3: execute two statements.
instance Equiv#(Stmt);
  module [BlueCheck] eq#(App app, Frequency fr, Stmt a, Stmt b) ();
    Stmt s = par a; b; endpar;
    addToCollection(tagged StmtItem (tuple3(fr, app, s)));
  endmodule
endinstance

// Recursive case: generate a random input,
// apply it to each function, and
// recurse on the resulting applications.
instance Equiv#(function b f(a x))
  provisos(Equiv#(b), Bits#(a, n), Bounded#(a), FShow#(a));
    module [BlueCheck] eq#(App app, Frequency fr
                                  , function b f(a x)
                                  , function b g(a y))();
      Reg#(Bool) init <- mkReg(True);
      Reg#(a) aReg <- mkRegU;
      Randomize#(a) aRandom <- mkGenericRandomizer;
      FIFOF#(a) aLog <- mkUGSizedFIFOF(logSize);

      function Action genRandom(Bool replay) =
        action
          let a <- aRandom.next;
          aReg <= replay ? aLog.first : a;
        endaction;

      rule initialise (init);
        aRandom.cntrl.init;
        init <= False;
      endrule

      Action logEnq   = aLog.enq(aReg);
      Action logRot   = action aLog.deq; aLog.enq(aLog.first); endaction;
      Action logClear = aLog.clear;

      function save(file) = putFile(file, aLog.first);
      function restore(file) =
        action let x <- getFile(file); aLog.enq(x); endaction;

      addToCollection(tagged RandomGenItem (tuple2(!init, genRandom)));
      addToCollection(tagged LogItem (tuple3(logEnq, logRot, logClear)));
      addToCollection(tagged SaveItem save);
      addToCollection(tagged RestoreItem restore);

      eq(appendArg(app, fshow(aReg)), fr, f(aReg), g(aReg));
    endmodule
endinstance

// Base case 4 (fall through): check that two values are equal.
instance Equiv#(a) provisos(Eq#(a), FShow#(a));
  module [BlueCheck] eq#(App app, Frequency fr, a x, a y) ();
    Wire#(Bool) success <- mkDWire(True);
    Fmt fmt = formatApp(app) + fshow(" failed: ")
            + fshow(x) + fshow(" v ") + fshow(y);

    rule check;
      if (x != y) success <= False;
    endrule
     
    addToCollection(tagged InvariantItem (tuple2(fmt, success)));
  endmodule
endinstance

// Like the Equiv type-class, except for a single method.
typeclass Prop#(type a);
  module [BlueCheck] pr#(App app, Frequency fr, a f) ();
endtypeclass

// Base case 1: execute statement.
instance Prop#(Stmt);
  module [BlueCheck] pr#(App app, Frequency fr, Stmt a) ();
    addToCollection(tagged StmtItem (tuple3(fr, app, a)));
  endmodule
endinstance

// Base case 2: execute action.
instance Prop#(Action);
  module [BlueCheck] pr#(App app, Frequency fr, Action a) ();
    addToCollection(tagged ActionItem (tuple3(fr, app, a)));
  endmodule
endinstance

// Base case 3: execute action-value
instance Prop#(ActionValue#(Bool));
  module [BlueCheck] pr#(App app,Frequency fr,ActionValue#(Bool) a) ();
    Wire#(Bool) success <- mkDWire(True);
    Fmt msg = fshow("Property failed");

    Action act =
      action
        Bool s <- a;
        if (!s) success <= False;
      endaction;
      addToCollection(tagged ActionItem (tuple3(fr, app, act)));
      addToCollection(tagged InvariantItem (tuple2(msg, success)));
  endmodule
endinstance

// Recursive case.
instance Prop#(function b f(a x))
  provisos(Prop#(b), Bits#(a, n), Bounded#(a), FShow#(a));
    module [BlueCheck] pr#(App app, Frequency fr, function b f(a x))();
      Reg#(Bool) init <- mkReg(True);
      Reg#(a) aReg <- mkRegU;
      Randomize#(a) aRandom <- mkGenericRandomizer;
      FIFOF#(a) aLog <- mkUGSizedFIFOF(logSize);

      function Action genRandom(Bool replay) =
        action
          let a <- aRandom.next;
          aReg <= replay ? aLog.first : a;
        endaction;

      rule initialise (init);
        aRandom.cntrl.init;
        init <= False;
      endrule

      Action logEnq   = aLog.enq(aReg);
      Action logRot   = action aLog.deq; aLog.enq(aLog.first); endaction;
      Action logClear = aLog.clear;

      function save(file) = putFile(file, aLog.first);
      function restore(file) =
        action let x <- getFile(file); aLog.enq(x); endaction;


      addToCollection(tagged RandomGenItem (tuple2(!init, genRandom)));
      addToCollection(tagged LogItem (tuple3(logEnq, logRot, logClear)));
      addToCollection(tagged SaveItem save);
      addToCollection(tagged RestoreItem restore);

      pr(appendArg(app, fshow(aReg)), fr, f(aReg));
    endmodule
endinstance

module [BlueCheck] prop#(String name, a f) ()
    provisos(Prop#(a));
  App app = App { name: name, args: Nil};
  pr(app, 1, f);
endmodule

module [BlueCheck] propf#(Frequency fr, String name, a f) ()
    provisos(Prop#(a));
  App app = App { name: name, args: Nil};
  pr(app, fr, f);
endmodule

// Ensure function -- for making assertions inside properties
typedef (function Action f(Bool cond)) Ensure;
typedef (function Action f(Bool cond, Fmt msg)) EnsureMsg;

module [BlueCheck] getEnsure (Ensure);
  // Create ensure function
  Wire#(Bool) ok <- mkDWire(True);
  Reg#(Bool) showMsg <- mkReg(False);
  function Action ensureFunc(Bool cond) = action ok <= cond; endaction;
  addToCollection(tagged EnsureItem (tuple2(ok, showMsg)));
  return ensureFunc;
endmodule

module [BlueCheck] getEnsureMsg (EnsureMsg);
  // Create ensure function
  Wire#(Bool) ok <- mkDWire(True);
  Reg#(Bool) showMsg <- mkReg(False);
  function Action ensureFunc(Bool cond, Fmt msg) =
    action ok <= cond; if (!cond && showMsg) $display(msg); endaction;
  addToCollection(tagged EnsureItem (tuple2(ok, showMsg)));
  return ensureFunc;
endmodule

function Action assignReg(t x, Reg#(t) r) = action r <= x; endaction;

// Allow user to add custom pre/post statements for each test
module [BlueCheck] addPreStmt#(Stmt pre) (Empty);
  addToCollection(tagged PreStmtItem pre);
endmodule

module [BlueCheck] addPostStmt#(Stmt post) (Empty);
  addToCollection(tagged PostStmtItem post);
endmodule

// "Parallel" assertions ======================================================

// Assert that a list of equivalences/properties can run in parallel.

module [BlueCheck] parallel#(List#(String) names) (Empty);
  addToCollection(tagged ParallelItem (tuple2(1, names)));
endmodule

module [BlueCheck] parallelf#(Frequency fr, List#(String) names) (Empty);
  addToCollection(tagged ParallelItem (tuple2(fr, names)));
endmodule

// The following type-class allows convenient construction of lists, e.g.
//
//   List#(String) xs = list("push", "pop", "top");

typeclass MkList#(type a, type b) dependencies (a determines b);
  function a mkList(List#(b) acc);
endtypeclass

instance MkList#(List#(a), a);
  function List#(a) mkList(List#(a) acc) = List::reverse(acc);
endinstance

instance MkList#(function b f(a elem), a) provisos (MkList#(b, a));
  function mkList(acc, elem) = mkList(Cons(elem, acc));
endinstance

function b list() provisos (MkList#(b, a));
  return mkList(Nil);
endfunction

// Is a list empty?
function Bool isEmpty(List#(a) xs);
  if (xs matches tagged Nil) return True; else return False;
endfunction

// Compute the condition for being in each state of the equivalance
// checker. Some states are visited more frequently than others.
function List#(Bool) stateConds(Reg#(State) s, Integer start,
                                         List#(Frequency) freqs);
  if (freqs matches tagged Nil) return Nil;
  else
    begin
      Frequency f = List::head(freqs);
      Bool cond;
      if (f == 1) cond = s == fromInteger(start);
      else cond = s >= fromInteger(start) && s < fromInteger(start+f);
      return (Cons(cond, stateConds(s, start+f, List::tail(freqs))));
    end
endfunction

// With the presence of 'conflict-free' assertions, it is possible to
// be in multiple states at the same time.  The following function
// will update the 'inState' mapping using the 'conflict-free' lists.<commit_msg>Update comments<commit_after>// BlueCheck 0.21, <NAME>.

// Change log
// ==========
//
// 5  Nov 2012: Version 0.1
// 21 Nov 2014: Support for iterative deepening
// 28 Nov 2014: Version 0.2, with support for shrinking
// 6  Dec 2014: Save a counter-example to a file and replay it
// 16 Dec 2014: Let statements run in parallel using 'parallel' assertions

package BlueCheck;

import Randomizable  :: *;
import ModuleCollect :: *;
import StmtFSM       :: *;
import List          :: *;
import Clocks        :: *;
import FIFOF         :: *;
import ConfigReg     :: *;
import Vector        :: *;

// The max size of the log used for shrinking.  This is tricky to
// implement as a module parameter, hence it is a global parameter.
typedef 32 LogSize;
Integer logSize = valueOf(LogSize);

// The filename used to store a counter-example so it can be replayed
// in isolation in a future simulation run with debugging enabled.
String logFilename = "CounterExample.bin";

// BlueCheck module parameters
typedef struct {
  // Verbose output
  Bool verbose;

  // Display message when a chosen state does not fire
  Bool showNonFire;

  // Display message when a chosen state is a no-op
  Bool showNoOp;

  // Generate a checker based on an iterative deepening strategy
  // (If 'False', a single random state walk is performed)
  Bool useIterativeDeepening;
  // This must contain valid data if 'useIterativeDeepening' is 'True'
  ID_Params id; 

  // Interactive iterative deepening
  Bool interactive;

  // Attempt to shrink a counter example, if one is found
  // (This is only valid for iterative deepening)
  Bool useShrinking;

  // Number of testing iterations to perform. For iterative deepening,
  // this is the number of times to increase the depth before stopping
  // Otherwise, the it's the length of the random state walk
  Bit#(32) numIterations;
} BlueCheck_Params;

// Sub-parameters for iterative deepening
typedef struct {
  // Iterative deepening requires ability to reset the circuit under test
  MakeResetIfc rst;

  // The number of states to be explored in a single 'test'
  Bit#(32) initialDepth;

  // The number of tests to perform at each depth
  Bit#(32) testsPerDepth;

  // A function to increase the depth
  (function Bit#(32) f(Bit#(32) currentDepth)) incDepth;
} ID_Params;

// The maximum number of states in the equivalance checker.
// You will get a compile-time error message if this parameter
// is not big enough, but it's not likely, unless you use very
// large method frequencies.
typedef 16 LogMaxStates;
typedef UInt#(LogMaxStates) State;

// The frequency that the checker will move to particular state.
typedef Integer Frequency; // Range: 1 to 100.

// Serialise / Deserialise counter-examples ===================================

// When a counter-example is found in simulation, we can save it to a
// file so that it can be replayed in isolation in a subsequent run
// with debugging enabled.  This feature is not synthesisable, but
// it's very handy in simulation.  Thanks to <NAME> for this
// suggestion.

// Serialise data of type t to a sequence of bytes and append to a file
// (This definition is a bit obfusticated but it's the only way I
// found that doesn't introduce an ugly type constraint)
function Action putFile(File f, t data)
  provisos ( Bits#(t, width)
           , Div#(width, 8, nbytes) ) =
  action
    Bit#(TAdd#(width, 8)) block = zeroExtend(pack(data));
    Vector#(nbytes, Bit#(8)) bytes =
      unpack(block[valueOf(TMul#(nbytes, 8))-1:0]);
    for (Integer i = 0; i < valueOf(nbytes); i=i+1)
      $fwrite(f, "%c", bytes[i]);
  endaction;

// De-serialise a sequence of bytes from a file and convert to data of type t
function ActionValue#(t) getFile(File f)
  provisos ( Bits#(t, width)
           , Div#(width, 8, nbytes) ) =
    actionvalue
      Vector#(nbytes, Bit#(8)) bytes;
      for (Integer i = 0; i < valueOf(nbytes); i=i+1) begin
        int c <- $fgetc(f);
        bytes[i] = pack(c)[7:0];
      end
      return unpack(pack(bytes)[valueOf(width)-1:0]);
    endactionvalue;

// For displaying function applications =======================================

typedef struct {
  String name;
  List#(Fmt) args;
} App;

function String getName(App app) = app.name;

function Fmt formatApp(App app);
  if (app.args matches tagged Nil)
    return $format("%s", app.name);
  else 
    return ($format("%s", app.name) + fshow("(") +
            formatArgs(app.args) + fshow(")"));
endfunction

function Fmt formatArgs(List#(Fmt) args);
  if (List::tail(args) matches tagged Nil)
    return List::head(args);
  else
    return (List::head(args) + fshow(",") + formatArgs(List::tail(args)));
endfunction

function App appendArg(App app, Fmt arg) =
  App { name: app.name, args: List::append(app.args, Cons(arg, Nil)) };

// Functions for adding properties to the test bench ==========================

// A BlueCheck module implicitly collects actions, statements,
// invariants, random generators and loggers, an allowing automatic
// creation of an equivalance checker.
typedef ModuleCollect#(Item) BlueCheck;

typedef union tagged {
  Tuple3#(Frequency, App, Action) ActionItem;
  Tuple3#(Frequency, App, Stmt) StmtItem;
  Tuple2#(Bool, function Action gen(Bool replay)) RandomGenItem;
  Tuple2#(Fmt, Bool) InvariantItem;
  Tuple2#(Bool, Reg#(Bool)) EnsureItem;
  Tuple3#(Action, Action, Action) LogItem;
  (function Action save(File f)) SaveItem;
  (function Action restore(File f)) RestoreItem;
  Stmt PreStmtItem;
  Stmt PostStmtItem;
  Tuple2#(Frequency, List#(String)) ParallelItem;
} Item;

// Turn an item into a singleton action if it is an ActionItem.
function List#(Tuple3#(Frequency, App, Action)) getActionItem(Item item) =
  case (item) matches
    tagged ActionItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton action if it is an RandomGenItem.
function List#(Tuple2#(Bool, function Action gen(Bool replay)))
  getRandomGenItem(Item item) =
  case (item) matches
    tagged RandomGenItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton pair if it is an InvariantItem.
function List#(Tuple2#(Fmt, Bool)) getInvariantItem(Item item) =
  case (item) matches
    tagged InvariantItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is an StmtItem.
function List#(Tuple3#(Frequency, App, Stmt)) getStmtItem(Item item) =
  case (item) matches
    tagged StmtItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is an EnsureItem.
function List#(Tuple2#(Bool, Reg#(Bool))) getEnsureItem(Item item) =
  case (item) matches
    tagged EnsureItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is an LogItem.
function List#(Tuple3#(Action, Action, Action))
  getLogItem(Item item) =
  case (item) matches
    tagged LogItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn a save item into a singleton statement if it is a SaveItem.
function List#(function Action save(File f)) getSaveItem(Item item) =
  case (item) matches
    tagged SaveItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn a save item into a singleton statement if it is a SaveItem.
function List#(function Action restore(File f)) getRestoreItem(Item item) =
  case (item) matches
    tagged RestoreItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is a PreStmtItem.
function List#(Stmt) getPreStmtItem(Item item) =
  case (item) matches
    tagged PreStmtItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is a PostStmtItem.
function List#(Stmt) getPostStmtItem(Item item) =
  case (item) matches
    tagged PostStmtItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// Turn an item into a singleton statement if it is a ParallelItem.
function List#(Tuple2#(Frequency, List#(String)))
    getParallelItem(Item item) =
  case (item) matches
    tagged ParallelItem .a: return Cons(a, Nil);
    default: return Nil;
  endcase;

// The following type class allows two functions of the same type to
// be applied to random inputs.  If the return values differ, the
// behaviour is to terminate with an error message (a counter-example
// has been found).  The probability that the equivalence will be
// checked on any given step can be specified.
typeclass Equiv#(type a);
  module [BlueCheck] eq#(App app, Frequency fr, a f, a g) ();
endtypeclass

module [BlueCheck] equiv#(String name, a f, a g) ()
    provisos(Equiv#(a));
  App app = App { name: name, args: Nil};
  eq(app, 1, f, g);
endmodule

module [BlueCheck] equivf#(Frequency fr, String name, a f, a g) ()
    provisos(Equiv#(a));
  App app = App { name: name, args: Nil};
  eq(app, fr, f, g);
endmodule

// Base case 1: execute two actions.
instance Equiv#(Action);
  module [BlueCheck] eq#(App app, Frequency fr, Action a, Action b) ();
    Action executeTwo =
      action
        a; b;
      endaction;
    addToCollection(tagged ActionItem
      (tuple3(fr, app, executeTwo)));
  endmodule
endinstance

// Base case 2: execute two action-values,
// and check equivalance of results.
instance Equiv#(ActionValue#(t))
  provisos(Eq#(t), Bits#(t, n), FShow#(t));
  module [BlueCheck] eq#(App app, Frequency fr
                                , ActionValue#(t) a
                                , ActionValue#(t) b) ();
    Wire#(Bool) success <- mkDWire(True);
    Wire#(t) aWire      <- mkDWire(?);
    Wire#(t) bWire      <- mkDWire(?);
    Fmt msg             =  fshow("Not equal: ") + fshow(aWire)
                        +  fshow(" versus ")    + fshow(bWire);

    Action executeTwoAndCheck =
      action
        t aVal <- a; aWire <= aVal;
        t bVal <- b; bWire <= bVal;
        if (aVal != bVal) success <= False;
      endaction;
      addToCollection(tagged ActionItem
        (tuple3(fr, app, executeTwoAndCheck)));
      addToCollection(tagged InvariantItem (tuple2(msg, success)));
  endmodule
endinstance

// Base case 3: execute two statements.
instance Equiv#(Stmt);
  module [BlueCheck] eq#(App app, Frequency fr, Stmt a, Stmt b) ();
    Stmt s = par a; b; endpar;
    addToCollection(tagged StmtItem (tuple3(fr, app, s)));
  endmodule
endinstance

// Recursive case: generate a random input,
// apply it to each function, and
// recurse on the resulting applications.
instance Equiv#(function b f(a x))
  provisos(Equiv#(b), Bits#(a, n), Bounded#(a), FShow#(a));
    module [BlueCheck] eq#(App app, Frequency fr
                                  , function b f(a x)
                                  , function b g(a y))();
      Reg#(Bool) init <- mkReg(True);
      Reg#(a) aReg <- mkRegU;
      Randomize#(a) aRandom <- mkGenericRandomizer;
      FIFOF#(a) aLog <- mkUGSizedFIFOF(logSize);

      function Action genRandom(Bool replay) =
        action
          let a <- aRandom.next;
          aReg <= replay ? aLog.first : a;
        endaction;

      rule initialise (init);
        aRandom.cntrl.init;
        init <= False;
      endrule

      Action logEnq   = aLog.enq(aReg);
      Action logRot   = action aLog.deq; aLog.enq(aLog.first); endaction;
      Action logClear = aLog.clear;

      function save(file) = putFile(file, aLog.first);
      function restore(file) =
        action let x <- getFile(file); aLog.enq(x); endaction;

      addToCollection(tagged RandomGenItem (tuple2(!init, genRandom)));
      addToCollection(tagged LogItem (tuple3(logEnq, logRot, logClear)));
      addToCollection(tagged SaveItem save);
      addToCollection(tagged RestoreItem restore);

      eq(appendArg(app, fshow(aReg)), fr, f(aReg), g(aReg));
    endmodule
endinstance

// Base case 4 (fall through): check that two values are equal.
instance Equiv#(a) provisos(Eq#(a), FShow#(a));
  module [BlueCheck] eq#(App app, Frequency fr, a x, a y) ();
    Wire#(Bool) success <- mkDWire(True);
    Fmt fmt = formatApp(app) + fshow(" failed: ")
            + fshow(x) + fshow(" v ") + fshow(y);

    rule check;
      if (x != y) success <= False;
    endrule
     
    addToCollection(tagged InvariantItem (tuple2(fmt, success)));
  endmodule
endinstance

// Like the Equiv type-class, except for a single method.
typeclass Prop#(type a);
  module [BlueCheck] pr#(App app, Frequency fr, a f) ();
endtypeclass

// Base case 1: execute statement.
instance Prop#(Stmt);
  module [BlueCheck] pr#(App app, Frequency fr, Stmt a) ();
    addToCollection(tagged StmtItem (tuple3(fr, app, a)));
  endmodule
endinstance

// Base case 2: execute action.
instance Prop#(Action);
  module [BlueCheck] pr#(App app, Frequency fr, Action a) ();
    addToCollection(tagged ActionItem (tuple3(fr, app, a)));
  endmodule
endinstance

// Base case 3: execute action-value
instance Prop#(ActionValue#(Bool));
  module [BlueCheck] pr#(App app,Frequency fr,ActionValue#(Bool) a) ();
    Wire#(Bool) success <- mkDWire(True);
    Fmt msg = fshow("Property failed");

    Action act =
      action
        Bool s <- a;
        if (!s) success <= False;
      endaction;
      addToCollection(tagged ActionItem (tuple3(fr, app, act)));
      addToCollection(tagged InvariantItem (tuple2(msg, success)));
  endmodule
endinstance

// Recursive case.
instance Prop#(function b f(a x))
  provisos(Prop#(b), Bits#(a, n), Bounded#(a), FShow#(a));
    module [BlueCheck] pr#(App app, Frequency fr, function b f(a x))();
      Reg#(Bool) init <- mkReg(True);
      Reg#(a) aReg <- mkRegU;
      Randomize#(a) aRandom <- mkGenericRandomizer;
      FIFOF#(a) aLog <- mkUGSizedFIFOF(logSize);

      function Action genRandom(Bool replay) =
        action
          let a <- aRandom.next;
          aReg <= replay ? aLog.first : a;
        endaction;

      rule initialise (init);
        aRandom.cntrl.init;
        init <= False;
      endrule

      Action logEnq   = aLog.enq(aReg);
      Action logRot   = action aLog.deq; aLog.enq(aLog.first); endaction;
      Action logClear = aLog.clear;

      function save(file) = putFile(file, aLog.first);
      function restore(file) =
        action let x <- getFile(file); aLog.enq(x); endaction;


      addToCollection(tagged RandomGenItem (tuple2(!init, genRandom)));
      addToCollection(tagged LogItem (tuple3(logEnq, logRot, logClear)));
      addToCollection(tagged SaveItem save);
      addToCollection(tagged RestoreItem restore);

      pr(appendArg(app, fshow(aReg)), fr, f(aReg));
    endmodule
endinstance

module [BlueCheck] prop#(String name, a f) ()
    provisos(Prop#(a));
  App app = App { name: name, args: Nil};
  pr(app, 1, f);
endmodule

module [BlueCheck] propf#(Frequency fr, String name, a f) ()
    provisos(Prop#(a));
  App app = App { name: name, args: Nil};
  pr(app, fr, f);
endmodule

// Ensure function -- for making assertions inside properties
typedef (function Action f(Bool cond)) Ensure;
typedef (function Action f(Bool cond, Fmt msg)) EnsureMsg;

module [BlueCheck] getEnsure (Ensure);
  // Create ensure function
  Wire#(Bool) ok <- mkDWire(True);
  Reg#(Bool) showMsg <- mkReg(False);
  function Action ensureFunc(Bool cond) = action ok <= cond; endaction;
  addToCollection(tagged EnsureItem (tuple2(ok, showMsg)));
  return ensureFunc;
endmodule

module [BlueCheck] getEnsureMsg (EnsureMsg);
  // Create ensure function
  Wire#(Bool) ok <- mkDWire(True);
  Reg#(Bool) showMsg <- mkReg(False);
  function Action ensureFunc(Bool cond, Fmt msg) =
    action ok <= cond; if (!cond && showMsg) $display(msg); endaction;
  addToCollection(tagged EnsureItem (tuple2(ok, showMsg)));
  return ensureFunc;
endmodule

function Action assignReg(t x, Reg#(t) r) = action r <= x; endaction;

// Allow user to add custom pre/post statements for each test
module [BlueCheck] addPreStmt#(Stmt pre) (Empty);
  addToCollection(tagged PreStmtItem pre);
endmodule

module [BlueCheck] addPostStmt#(Stmt post) (Empty);
  addToCollection(tagged PostStmtItem post);
endmodule

// "Parallel" assertions ======================================================

// Assert that a list of equivalences/properties can run in parallel.

module [BlueCheck] parallel#(List#(String) names) (Empty);
  addToCollection(tagged ParallelItem (tuple2(1, names)));
endmodule

module [BlueCheck] parallelf#(Frequency fr, List#(String) names) (Empty);
  addToCollection(tagged ParallelItem (tuple2(fr, names)));
endmodule

// The following type-class allows convenient construction of lists, e.g.
//
//   List#(String) xs = list("push", "pop", "top");

typeclass MkList#(type a, type b) dependencies (a determines b);
  function a mkList(List#(b) acc);
endtypeclass

instance MkList#(List#(a), a);
  function List#(a) mkList(List#(a) acc) = List::reverse(acc);
endinstance

instance MkList#(function b f(a elem), a) provisos (MkList#(b, a));
  function mkList(acc, elem) = mkList(Cons(elem, acc));
endinstance

function b list() provisos (MkList#(b, a));
  return mkList(Nil);
endfunction

// Is a list empty?
function Bool isEmpty(List#(a) xs);
  if (xs matches tagged Nil) return True; else return False;
endfunction

// Compute the condition for being in each state of the equivalance
// checker. Some states are visited more frequently than others.
function List#(Bool) stateConds(Reg#(State) s, Integer start,
                                         List#(Frequency) freqs);
  if (freqs matches tagged Nil) return Nil;
  else
    begin
      Frequency f = List::head(freqs);
      Bool cond;
      if (f == 1) cond = s == fromInteger(start);
      else cond = s >= fromInteger(start) && s < fromInteger(start+f);
      return (Cons(cond, stateConds(s, start+f, List::tail(freqs))));
    end
endfunction

// With the presence of 'parallel' assertions, it is possible to
// be in multiple states at the same time.  The following function
// will update the 'inState' mapping using the 'parallel' lists.
{'fraction_non_alphanumeric': 0.12576908153650018, 'fraction_numerical': 0.006152652292001552, 'mean_word_length': 3.4613006923837784, 'pattern_counts': {'":': 0, '<': 87, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7167908', 'n_tokens_mistral': 11807, 'n_tokens_neox': 11184, 'n_words': 3968}