Día 7La otra mitad, y el cierre

// The virtual sequencer: it has no queue, it arbitrates no items, it talks to no
// driver. It is a component that exists for two things:
//
//   1. to hold the HANDLES to the real sequencers, somewhere the sequence can
//      reach without looking up by string;
//   2. to be a uvm_component, that is, to live in the tree and have a name.
//
// That is why it extends uvm_sequencer WITHOUT parameters: the default item is
// uvm_sequence_item, and none is ever sent.
class virtual_sequencer extends uvm_sequencer;
   `uvm_component_utils(virtual_sequencer)

   sequencer clase_sequencer_h;
   sequencer modulo_sequencer_h;

   function new(string name, uvm_component parent);
      super.new(name, parent);
   endfunction : new

endclass : virtual_sequencer

// The env of the Sequences section with TWO changes, and no more:
//
//   1. the second agent is UVM_ACTIVE instead of UVM_PASSIVE;
//   2. there is a virtual_sequencer, and connect_phase hands it the handles of
//      the two real sequencers.
//
// The rest --agents, scoreboards, coverage, the config_db scope-- is
// identical. That is the point: a virtual sequence does not change the structure
// of the testbench, it only adds who coordinates it.
class env extends uvm_env;
   `uvm_component_utils(env);

   vtalu_agent        clase_agent_h, modulo_agent_h;
   vtalu_agent_config clase_cfg_h, modulo_cfg_h;

   scoreboard clase_scoreboard_h, modulo_scoreboard_h;
   coverage   clase_coverage_h, modulo_coverage_h;

   virtual_sequencer virtual_sequencer_h;

   function new(string name, uvm_component parent);
      super.new(name, parent);
   endfunction : new

   function void build_phase(uvm_phase phase);
      env_config env_config_h;

      if (!uvm_config_db#(env_config)::get(this, "", "config", env_config_h))
         `uvm_fatal("ENV", "Failed to get env config")

      // Both active: each with its own sequencer and driver.
      clase_cfg_h  = new(.bfm(env_config_h.clase_bfm),  .is_active(UVM_ACTIVE));
      modulo_cfg_h = new(.bfm(env_config_h.modulo_bfm), .is_active(UVM_ACTIVE));

      uvm_config_db#(vtalu_agent_config)::set(this, "clase_agent_h*", "config", clase_cfg_h);
      uvm_config_db#(vtalu_agent_config)::set(this, "modulo_agent_h*", "config", modulo_cfg_h);

      clase_agent_h  = vtalu_agent::type_id::create("clase_agent_h", this);
      modulo_agent_h = vtalu_agent::type_id::create("modulo_agent_h", this);

      virtual_sequencer_h = virtual_sequencer::type_id::create("virtual_sequencer_h", this);

      clase_scoreboard_h  = scoreboard::type_id::create("clase_scoreboard_h", this);
      modulo_scoreboard_h = scoreboard::type_id::create("modulo_scoreboard_h", this);
      clase_coverage_h    = coverage::type_id::create("clase_coverage_h", this);
      modulo_coverage_h   = coverage::type_id::create("modulo_coverage_h", this);
   endfunction : build_phase

   function void connect_phase(uvm_phase phase);
      // The handles are passed HERE and not looked up by string: in connect_phase
      // both agents already exist, and if somebody renames a component this does
      // not compile instead of returning null at simulation time.
      virtual_sequencer_h.clase_sequencer_h  = clase_agent_h.sequencer_h;
      virtual_sequencer_h.modulo_sequencer_h = modulo_agent_h.sequencer_h;

      clase_agent_h.command_ap.connect(clase_scoreboard_h.cmd_f.analysis_export);
      clase_agent_h.command_ap.connect(clase_coverage_h.analysis_export);
      clase_agent_h.result_ap.connect(clase_scoreboard_h.analysis_export);

      modulo_agent_h.command_ap.connect(modulo_scoreboard_h.cmd_f.analysis_export);
      modulo_agent_h.command_ap.connect(modulo_coverage_h.analysis_export);
      modulo_agent_h.result_ap.connect(modulo_scoreboard_h.analysis_export);
   endfunction : connect_phase

endclass : env

// THE virtual sequence.
//
// Two things set it apart from every sequence in the Sequences section:
//
//   1. It has NO items of its own. It extends uvm_sequence without parameters
//      and never calls start_item(): all it does is start OTHER sequences.
//      Hence "virtual" -- it is tied to no item type and no sequencer.
//   2. It runs on more than one sequencer, and that is where the one thing no
//      single sequence can do comes from: coordinating two interfaces.

// `uvm_declare_p_sequencer declares `p_sequencer` with the type above and casts
// it on its own inside m_set_p_sequencer. Without it, get_sequencer() returns a
// uvm_sequencer_base and every use would need a cast by hand.
class coordinada_sequence extends uvm_sequence;
   `uvm_object_utils(coordinada_sequence)
   `uvm_declare_p_sequencer(virtual_sequencer)

   int unsigned count = 1000;

   function new(string name = "coordinada_sequence");
      super.new(name);
   endfunction : new

   task body();
      reset_sequence   reset_a, reset_b;
      maxmult_sequence maxmult;
      random_sequence  random_b;
      un_op_sequence   primera, segunda;

      reset_a  = reset_sequence::type_id::create("reset_a");
      reset_b  = reset_sequence::type_id::create("reset_b");
      maxmult  = maxmult_sequence::type_id::create("maxmult");
      random_b = random_sequence::type_id::create("random_b");
      primera  = un_op_sequence::type_id::create("primera");
      segunda  = un_op_sequence::type_id::create("segunda");

      random_b.count = count;

      // --- 1. Both ALUs get reset at the same time -----------------------------
      // fork/join over TWO sequencers. Each branch blocks on its own driver, and
      // the join waits for both: that cannot be written inside a normal
      // sequence, which only knows the sequencer that started it.
      fork
         reset_a.start(p_sequencer.clase_sequencer_h);
         reset_b.start(p_sequencer.modulo_sequencer_h);
      join

      // --- 2. Parallel traffic, different on each interface -------------------
      // A does the directed overflow case while B sends at random.
      fork
         maxmult.start(p_sequencer.clase_sequencer_h);
         random_b.start(p_sequencer.modulo_sequencer_h);
      join

      // --- 3. What no single sequence can do ----------------------------------
      // The result of VTALU A is the operand of B. It is a dependency BETWEEN
      // interfaces: the second one cannot even start being built until the
      // first one answered.
      primera.A  = 8'h0F;
      primera.B  = 8'h07;
      primera.op = mul_op;
      primera.start(p_sequencer.clase_sequencer_h);

      `uvm_info("COORDINADA", $sformatf(
                "A returned %0d: it goes as an operand into B", primera.result), UVM_LOW)

      segunda.A  = primera.result[7:0];
      segunda.B  = 8'h01;
      segunda.op = add_op;
      segunda.start(p_sequencer.modulo_sequencer_h);

      `uvm_info("COORDINADA", $sformatf(
                "B returned %0d", segunda.result), UVM_LOW)
   endtask : body

endclass : coordinada_sequence

// THE virtual sequence.
//
// Two things set it apart from every sequence in the Sequences section:
//
//   1. It has NO items of its own. It extends uvm_sequence without parameters
//      and never calls start_item(): all it does is start OTHER sequences.
//      Hence "virtual" -- it is tied to no item type and no sequencer.
//   2. It runs on more than one sequencer, and that is where the one thing no
//      single sequence can do comes from: coordinating two interfaces.

// `uvm_declare_p_sequencer declares `p_sequencer` with the type above and casts
// it on its own inside m_set_p_sequencer. Without it, get_sequencer() returns a
// uvm_sequencer_base and every use would need a cast by hand.
class coordinada_sequence extends uvm_sequence;
   `uvm_object_utils(coordinada_sequence)
   `uvm_declare_p_sequencer(virtual_sequencer)

   int unsigned count = 1000;

   function new(string name = "coordinada_sequence");
      super.new(name);
   endfunction : new

   task body();
      reset_sequence   reset_a, reset_b;
      maxmult_sequence maxmult;
      random_sequence  random_b;
      un_op_sequence   primera, segunda;

      reset_a  = reset_sequence::type_id::create("reset_a");
      reset_b  = reset_sequence::type_id::create("reset_b");
      maxmult  = maxmult_sequence::type_id::create("maxmult");
      random_b = random_sequence::type_id::create("random_b");
      primera  = un_op_sequence::type_id::create("primera");
      segunda  = un_op_sequence::type_id::create("segunda");

      random_b.count = count;

      // --- 1. Both ALUs get reset at the same time -----------------------------
      // fork/join over TWO sequencers. Each branch blocks on its own driver, and
      // the join waits for both: that cannot be written inside a normal
      // sequence, which only knows the sequencer that started it.
      fork
         reset_a.start(p_sequencer.clase_sequencer_h);
         reset_b.start(p_sequencer.modulo_sequencer_h);
      join

      // --- 2. Parallel traffic, different on each interface -------------------
      // A does the directed overflow case while B sends at random.
      fork
         maxmult.start(p_sequencer.clase_sequencer_h);
         random_b.start(p_sequencer.modulo_sequencer_h);
      join

      // --- 3. What no single sequence can do ----------------------------------
      // The result of VTALU A is the operand of B. It is a dependency BETWEEN
      // interfaces: the second one cannot even start being built until the
      // first one answered.
      primera.A  = 8'h0F;
      primera.B  = 8'h07;
      primera.op = mul_op;
      primera.start(p_sequencer.clase_sequencer_h);

      `uvm_info("COORDINADA", $sformatf(
                "A returned %0d: it goes as an operand into B", primera.result), UVM_LOW)

      segunda.A  = primera.result[7:0];
      segunda.B  = 8'h01;
      segunda.op = add_op;
      segunda.start(p_sequencer.modulo_sequencer_h);

      `uvm_info("COORDINADA", $sformatf(
                "B returned %0d", segunda.result), UVM_LOW)
   endtask : body

endclass : coordinada_sequence

// THE virtual sequence.
//
// Two things set it apart from every sequence in the Sequences section:
//
//   1. It has NO items of its own. It extends uvm_sequence without parameters
//      and never calls start_item(): all it does is start OTHER sequences.
//      Hence "virtual" -- it is tied to no item type and no sequencer.
//   2. It runs on more than one sequencer, and that is where the one thing no
//      single sequence can do comes from: coordinating two interfaces.

// `uvm_declare_p_sequencer declares `p_sequencer` with the type above and casts
// it on its own inside m_set_p_sequencer. Without it, get_sequencer() returns a
// uvm_sequencer_base and every use would need a cast by hand.
class coordinada_sequence extends uvm_sequence;
   `uvm_object_utils(coordinada_sequence)
   `uvm_declare_p_sequencer(virtual_sequencer)

   int unsigned count = 1000;

   function new(string name = "coordinada_sequence");
      super.new(name);
   endfunction : new

   task body();
      reset_sequence   reset_a, reset_b;
      maxmult_sequence maxmult;
      random_sequence  random_b;
      un_op_sequence   primera, segunda;

      reset_a  = reset_sequence::type_id::create("reset_a");
      reset_b  = reset_sequence::type_id::create("reset_b");
      maxmult  = maxmult_sequence::type_id::create("maxmult");
      random_b = random_sequence::type_id::create("random_b");
      primera  = un_op_sequence::type_id::create("primera");
      segunda  = un_op_sequence::type_id::create("segunda");

      random_b.count = count;

      // --- 1. Both ALUs get reset at the same time -----------------------------
      // fork/join over TWO sequencers. Each branch blocks on its own driver, and
      // the join waits for both: that cannot be written inside a normal
      // sequence, which only knows the sequencer that started it.
      fork
         reset_a.start(p_sequencer.clase_sequencer_h);
         reset_b.start(p_sequencer.modulo_sequencer_h);
      join

      // --- 2. Parallel traffic, different on each interface -------------------
      // A does the directed overflow case while B sends at random.
      fork
         maxmult.start(p_sequencer.clase_sequencer_h);
         random_b.start(p_sequencer.modulo_sequencer_h);
      join

      // --- 3. What no single sequence can do ----------------------------------
      // The result of VTALU A is the operand of B. It is a dependency BETWEEN
      // interfaces: the second one cannot even start being built until the
      // first one answered.
      primera.A  = 8'h0F;
      primera.B  = 8'h07;
      primera.op = mul_op;
      primera.start(p_sequencer.clase_sequencer_h);

      `uvm_info("COORDINADA", $sformatf(
                "A returned %0d: it goes as an operand into B", primera.result), UVM_LOW)

      segunda.A  = primera.result[7:0];
      segunda.B  = 8'h01;
      segunda.op = add_op;
      segunda.start(p_sequencer.modulo_sequencer_h);

      `uvm_info("COORDINADA", $sformatf(
                "B returned %0d", segunda.result), UVM_LOW)
   endtask : body

endclass : coordinada_sequence

interface vtalu_bfm;
   import uvm_pkg::*;
   import vtalu_pkg::*;
   `include "uvm_macros.svh"

   byte unsigned          A;
   byte unsigned          B;
   bit                    clk;
   bit                    reset_n;
   bit                    start;
   wire                   done;
   wire            [15:0] result;
   wire                   ovf;
   operation_t            op_set;

   command_monitor        command_monitor_h;

   function operation_t op2enum();
      case (op_set)
         3'b000:  return no_op;
         3'b001:  return add_op;
         3'b010:  return sub_op;
         3'b011:  return and_op;
         3'b100:  return xor_op;
         3'b101:  return mul_op;
         default: $fatal(1, "Illegal operation on op bus");
      endcase  // case (op_set)
   endfunction : op2enum

   always @(posedge clk) begin : op_monitor
      static bit in_command = 0;
      // The null guard rst_monitor already had, now here too. With two BFMs in
      // the top, one can be left without a monitor while the testbench is being
      // built -- or forever, if someone forgets to instantiate the passive
      // agent. Without the guard that is a simulator crash instead of a
      // testbench that sees nothing.
      if (command_monitor_h != null) begin : con_monitor
         if (start) begin : start_high
            if (!in_command) begin : new_command
               command_monitor_h.write_to_monitor(A, B, op2enum());
               in_command = (op2enum() != no_op);
            end : new_command
         end : start_high
         else  // start low
            in_command = 0;
      end : con_monitor
   end : op_monitor

   always @(negedge reset_n) begin : rst_monitor
      if (command_monitor_h != null)  //guard against VCS time 0 negedge
         command_monitor_h.write_to_monitor(A, B, rst_op);
   end : rst_monitor

   result_monitor result_monitor_h;

   initial begin : result_monitor_thread
      forever begin : result_monitor
         @(posedge clk);
         // Same guard as op_monitor and rst_monitor: with two BFMs in the top,
         // one can be left without a monitor. Without this, forgetting the
         // passive agent is a simulator "Null pointer dereferenced" instead of
         // the checker's message -- which is exactly where exercise d6 starts.
         if (done && result_monitor_h != null) result_monitor_h.write_to_monitor(result, ovf);
      end : result_monitor
   end : result_monitor_thread

   initial begin
      clk = 0;
      forever begin
         #10;
         clk = ~clk;
      end
   end


   // --- the protocol, in the BFM ---
   // Everything that knows HOW the DUT is talked to lives here, in one place:
   // the rest of the testbench asks for an operation and never touches a wire.
   // That is the idea of the interfaces-and-BFM section, and it holds to the end of the course.

   task reset_alu();
      reset_n = 1'b0;
      @(negedge clk);
      @(negedge clk);
      reset_n = 1'b1;
      start   = 1'b0;
   endtask : reset_alu

   // NEW with the sequences: the fourth argument. The protocol did not change; the only
   // thing added is reading result on the edge where done is already up.
   bit bug_operandos;
   initial bug_operandos = $test$plusargs("BUG");

   task send_op(input byte iA, input byte iB, input operation_t iop,
                output shortint unsigned oresult);
      oresult = 0;
      if (iop == rst_op) begin
         @(posedge clk);
         reset_n = 1'b0;
         start   = 1'b0;
         @(posedge clk);
         #1;
         reset_n = 1'b1;
      end else begin
         @(negedge clk);
         op_set = iop;
         A = iA;
         B = iB;
         start = 1'b1;
         if (iop == no_op) begin
            @(posedge clk);
            #1;
            start = 1'b0;
         end else begin
            // +BUG=1: changes B halfway through the multiplication. The
            // multiplier already latched A and B on the first edge, so the
            // RESULT DOES NOT CHANGE: the scoreboard stays green. The only
            // thing that sees it is the assertion. That is the whole section.
            if (bug_operandos && iop == mul_op) begin
               @(negedge clk);
               @(negedge clk);
               B = ~iB;
            end
            do @(negedge clk); while (done == 0);
            oresult   = result;
            start = 1'b0;
         end
      end  // else: !if(iop == rst_op)
   endtask : send_op


   // ==========================================================================
   //  The protocol, checked where it happens
   // ==========================================================================
   //
   // The properties live HERE, with the signals, and not in the testbench: they
   // plug themselves in, nobody connects them, and the passive agent of the Agents
   // section gets them for free. All they need in order to run is --assert.

   // TWO CLOCKS, and it is not an implementation detail: the BFM drives on
   // negedge and the DUT registers on posedge. An assertion samples in the
   // preponed region of the edge it is given, so a signal written ON the negedge
   // is not seen on that negedge: it is seen on the next one. With everything on
   // posedge, two consecutive no_op -- start goes down at t=111 and back up at
   // t=120, between two posedges -- read as ONE transaction with the operands
   // changing: 145 false positives every 1000 operations. With everything on
   // negedge, the false positives move to the done properties.
   //
   //   stimulus (start, A, B, op_set)  -> negedge, where the BFM writes
   //   response (done, result)         -> posedge, where the DUT registers

   default disable iff (!reset_n);

   // --- The stimulus ---

   // The rule from slide 1 of day 1, executable at last: while start is up, the
   // operands and the operation are not touched.
   property p_operandos_estables;
      @(negedge clk) start |=> $stable(A) && $stable(B) && $stable(op_set);
   endproperty : p_operandos_estables

   a_operandos_estables :
   assert property (p_operandos_estables)
   else
      `uvm_error("SVA", $sformatf(
                 "%m: operand changed with start up: A=%0d B=%0d op=%s", A, B, op2enum().name()))

   // --- The DUT's answer ---

   // The variable latency from the VTALU spec section, in one line: one cycle for the
   // one-cycle ops, four edges for the multiplication.
   property p_done_llega;
      @(posedge clk) start && (op_set != no_op) |-> ##[1:5] done;
   endproperty : p_done_llega

   a_done_llega :
   assert property (p_done_llega)
   else `uvm_error("SVA", $sformatf("%m: start con op=%s y done no llego en 5 ciclos", op2enum().name()))

   // The fine print: no_op is the only operation that does not answer.
   property p_no_op_sin_done;
      @(posedge clk) start && (op_set == no_op) |=> !done;
   endproperty : p_no_op_sin_done

   a_no_op_sin_done :
   assert property (p_no_op_sin_done)
   else `uvm_error("SVA", $sformatf("%m: done subio para una no_op"))

   // --- Every assertion comes with its cover property ---
   //
   // An assertion whose antecedent never happens PASSES, and checks nothing.
   // The cover is the antidote. And it also debunks mental models: the
   // "three-cycle" multiplication takes FOUR edges (done3 -> done2 ->
   // done1 -> done_mult), so c_mult_3ciclos stays at 0 forever.
   // --- VTALU rev2: the output the scoreboard only glances at ---

   // ovf belongs to sub and to nobody else. An assertion, because it is a rule of
   // the spec and not arithmetic: the scoreboard checks WHAT it computes, this
   // checks that it does not invent a flag where none belongs.
   property p_ovf_solo_en_sub;
      @(posedge clk) done && (op_set != sub_op) |-> !ovf;
   endproperty : p_ovf_solo_en_sub

   a_ovf_solo_en_sub :
   assert property (p_ovf_solo_en_sub)
   else `uvm_error("SVA", $sformatf("%m: ovf arriba con op=%s, que no puede desbordar", op2enum().name()))

   // And the cover that goes with it: without this, a regression where the random
   // never subtracted too much leaves the assertion green having checked nothing.
   c_ovf : cover property (@(posedge clk) done && ovf);
   c_sub_sin_borrow : cover property (@(posedge clk) done && (op_set == sub_op) && !ovf);

   c_mult_3ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##3 done);
   c_mult_4ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##4 done);
   c_un_ciclo : cover property (@(posedge clk) $rose(start) && (op_set inside {add_op, sub_op, and_op, xor_op}) ##1 done);

endinterface : vtalu_bfm

interface vtalu_bfm;
   import uvm_pkg::*;
   import vtalu_pkg::*;
   `include "uvm_macros.svh"

   byte unsigned          A;
   byte unsigned          B;
   bit                    clk;
   bit                    reset_n;
   bit                    start;
   wire                   done;
   wire            [15:0] result;
   wire                   ovf;
   operation_t            op_set;

   command_monitor        command_monitor_h;

   function operation_t op2enum();
      case (op_set)
         3'b000:  return no_op;
         3'b001:  return add_op;
         3'b010:  return sub_op;
         3'b011:  return and_op;
         3'b100:  return xor_op;
         3'b101:  return mul_op;
         default: $fatal(1, "Illegal operation on op bus");
      endcase  // case (op_set)
   endfunction : op2enum

   always @(posedge clk) begin : op_monitor
      static bit in_command = 0;
      // The null guard rst_monitor already had, now here too. With two BFMs in
      // the top, one can be left without a monitor while the testbench is being
      // built -- or forever, if someone forgets to instantiate the passive
      // agent. Without the guard that is a simulator crash instead of a
      // testbench that sees nothing.
      if (command_monitor_h != null) begin : con_monitor
         if (start) begin : start_high
            if (!in_command) begin : new_command
               command_monitor_h.write_to_monitor(A, B, op2enum());
               in_command = (op2enum() != no_op);
            end : new_command
         end : start_high
         else  // start low
            in_command = 0;
      end : con_monitor
   end : op_monitor

   always @(negedge reset_n) begin : rst_monitor
      if (command_monitor_h != null)  //guard against VCS time 0 negedge
         command_monitor_h.write_to_monitor(A, B, rst_op);
   end : rst_monitor

   result_monitor result_monitor_h;

   initial begin : result_monitor_thread
      forever begin : result_monitor
         @(posedge clk);
         // Same guard as op_monitor and rst_monitor: with two BFMs in the top,
         // one can be left without a monitor. Without this, forgetting the
         // passive agent is a simulator "Null pointer dereferenced" instead of
         // the checker's message -- which is exactly where exercise d6 starts.
         if (done && result_monitor_h != null) result_monitor_h.write_to_monitor(result, ovf);
      end : result_monitor
   end : result_monitor_thread

   initial begin
      clk = 0;
      forever begin
         #10;
         clk = ~clk;
      end
   end


   // --- the protocol, in the BFM ---
   // Everything that knows HOW the DUT is talked to lives here, in one place:
   // the rest of the testbench asks for an operation and never touches a wire.
   // That is the idea of the interfaces-and-BFM section, and it holds to the end of the course.

   task reset_alu();
      reset_n = 1'b0;
      @(negedge clk);
      @(negedge clk);
      reset_n = 1'b1;
      start   = 1'b0;
   endtask : reset_alu

   // NEW with the sequences: the fourth argument. The protocol did not change; the only
   // thing added is reading result on the edge where done is already up.
   bit bug_operandos;
   initial bug_operandos = $test$plusargs("BUG");

   task send_op(input byte iA, input byte iB, input operation_t iop,
                output shortint unsigned oresult);
      oresult = 0;
      if (iop == rst_op) begin
         @(posedge clk);
         reset_n = 1'b0;
         start   = 1'b0;
         @(posedge clk);
         #1;
         reset_n = 1'b1;
      end else begin
         @(negedge clk);
         op_set = iop;
         A = iA;
         B = iB;
         start = 1'b1;
         if (iop == no_op) begin
            @(posedge clk);
            #1;
            start = 1'b0;
         end else begin
            // +BUG=1: changes B halfway through the multiplication. The
            // multiplier already latched A and B on the first edge, so the
            // RESULT DOES NOT CHANGE: the scoreboard stays green. The only
            // thing that sees it is the assertion. That is the whole section.
            if (bug_operandos && iop == mul_op) begin
               @(negedge clk);
               @(negedge clk);
               B = ~iB;
            end
            do @(negedge clk); while (done == 0);
            oresult   = result;
            start = 1'b0;
         end
      end  // else: !if(iop == rst_op)
   endtask : send_op


   // ==========================================================================
   //  The protocol, checked where it happens
   // ==========================================================================
   //
   // The properties live HERE, with the signals, and not in the testbench: they
   // plug themselves in, nobody connects them, and the passive agent of the Agents
   // section gets them for free. All they need in order to run is --assert.

   // TWO CLOCKS, and it is not an implementation detail: the BFM drives on
   // negedge and the DUT registers on posedge. An assertion samples in the
   // preponed region of the edge it is given, so a signal written ON the negedge
   // is not seen on that negedge: it is seen on the next one. With everything on
   // posedge, two consecutive no_op -- start goes down at t=111 and back up at
   // t=120, between two posedges -- read as ONE transaction with the operands
   // changing: 145 false positives every 1000 operations. With everything on
   // negedge, the false positives move to the done properties.
   //
   //   stimulus (start, A, B, op_set)  -> negedge, where the BFM writes
   //   response (done, result)         -> posedge, where the DUT registers

   default disable iff (!reset_n);

   // --- The stimulus ---

   // The rule from slide 1 of day 1, executable at last: while start is up, the
   // operands and the operation are not touched.
   property p_operandos_estables;
      @(negedge clk) start |=> $stable(A) && $stable(B) && $stable(op_set);
   endproperty : p_operandos_estables

   a_operandos_estables :
   assert property (p_operandos_estables)
   else
      `uvm_error("SVA", $sformatf(
                 "%m: operand changed with start up: A=%0d B=%0d op=%s", A, B, op2enum().name()))

   // --- The DUT's answer ---

   // The variable latency from the VTALU spec section, in one line: one cycle for the
   // one-cycle ops, four edges for the multiplication.
   property p_done_llega;
      @(posedge clk) start && (op_set != no_op) |-> ##[1:5] done;
   endproperty : p_done_llega

   a_done_llega :
   assert property (p_done_llega)
   else `uvm_error("SVA", $sformatf("%m: start con op=%s y done no llego en 5 ciclos", op2enum().name()))

   // The fine print: no_op is the only operation that does not answer.
   property p_no_op_sin_done;
      @(posedge clk) start && (op_set == no_op) |=> !done;
   endproperty : p_no_op_sin_done

   a_no_op_sin_done :
   assert property (p_no_op_sin_done)
   else `uvm_error("SVA", $sformatf("%m: done subio para una no_op"))

   // --- Every assertion comes with its cover property ---
   //
   // An assertion whose antecedent never happens PASSES, and checks nothing.
   // The cover is the antidote. And it also debunks mental models: the
   // "three-cycle" multiplication takes FOUR edges (done3 -> done2 ->
   // done1 -> done_mult), so c_mult_3ciclos stays at 0 forever.
   // --- VTALU rev2: the output the scoreboard only glances at ---

   // ovf belongs to sub and to nobody else. An assertion, because it is a rule of
   // the spec and not arithmetic: the scoreboard checks WHAT it computes, this
   // checks that it does not invent a flag where none belongs.
   property p_ovf_solo_en_sub;
      @(posedge clk) done && (op_set != sub_op) |-> !ovf;
   endproperty : p_ovf_solo_en_sub

   a_ovf_solo_en_sub :
   assert property (p_ovf_solo_en_sub)
   else `uvm_error("SVA", $sformatf("%m: ovf arriba con op=%s, que no puede desbordar", op2enum().name()))

   // And the cover that goes with it: without this, a regression where the random
   // never subtracted too much leaves the assertion green having checked nothing.
   c_ovf : cover property (@(posedge clk) done && ovf);
   c_sub_sin_borrow : cover property (@(posedge clk) done && (op_set == sub_op) && !ovf);

   c_mult_3ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##3 done);
   c_mult_4ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##4 done);
   c_un_ciclo : cover property (@(posedge clk) $rose(start) && (op_set inside {add_op, sub_op, and_op, xor_op}) ##1 done);

endinterface : vtalu_bfm

interface vtalu_bfm;
   import uvm_pkg::*;
   import vtalu_pkg::*;
   `include "uvm_macros.svh"

   byte unsigned          A;
   byte unsigned          B;
   bit                    clk;
   bit                    reset_n;
   bit                    start;
   wire                   done;
   wire            [15:0] result;
   wire                   ovf;
   operation_t            op_set;

   command_monitor        command_monitor_h;

   function operation_t op2enum();
      case (op_set)
         3'b000:  return no_op;
         3'b001:  return add_op;
         3'b010:  return sub_op;
         3'b011:  return and_op;
         3'b100:  return xor_op;
         3'b101:  return mul_op;
         default: $fatal(1, "Illegal operation on op bus");
      endcase  // case (op_set)
   endfunction : op2enum

   always @(posedge clk) begin : op_monitor
      static bit in_command = 0;
      // The null guard rst_monitor already had, now here too. With two BFMs in
      // the top, one can be left without a monitor while the testbench is being
      // built -- or forever, if someone forgets to instantiate the passive
      // agent. Without the guard that is a simulator crash instead of a
      // testbench that sees nothing.
      if (command_monitor_h != null) begin : con_monitor
         if (start) begin : start_high
            if (!in_command) begin : new_command
               command_monitor_h.write_to_monitor(A, B, op2enum());
               in_command = (op2enum() != no_op);
            end : new_command
         end : start_high
         else  // start low
            in_command = 0;
      end : con_monitor
   end : op_monitor

   always @(negedge reset_n) begin : rst_monitor
      if (command_monitor_h != null)  //guard against VCS time 0 negedge
         command_monitor_h.write_to_monitor(A, B, rst_op);
   end : rst_monitor

   result_monitor result_monitor_h;

   initial begin : result_monitor_thread
      forever begin : result_monitor
         @(posedge clk);
         // Same guard as op_monitor and rst_monitor: with two BFMs in the top,
         // one can be left without a monitor. Without this, forgetting the
         // passive agent is a simulator "Null pointer dereferenced" instead of
         // the checker's message -- which is exactly where exercise d6 starts.
         if (done && result_monitor_h != null) result_monitor_h.write_to_monitor(result, ovf);
      end : result_monitor
   end : result_monitor_thread

   initial begin
      clk = 0;
      forever begin
         #10;
         clk = ~clk;
      end
   end


   // --- the protocol, in the BFM ---
   // Everything that knows HOW the DUT is talked to lives here, in one place:
   // the rest of the testbench asks for an operation and never touches a wire.
   // That is the idea of the interfaces-and-BFM section, and it holds to the end of the course.

   task reset_alu();
      reset_n = 1'b0;
      @(negedge clk);
      @(negedge clk);
      reset_n = 1'b1;
      start   = 1'b0;
   endtask : reset_alu

   // NEW with the sequences: the fourth argument. The protocol did not change; the only
   // thing added is reading result on the edge where done is already up.
   bit bug_operandos;
   initial bug_operandos = $test$plusargs("BUG");

   task send_op(input byte iA, input byte iB, input operation_t iop,
                output shortint unsigned oresult);
      oresult = 0;
      if (iop == rst_op) begin
         @(posedge clk);
         reset_n = 1'b0;
         start   = 1'b0;
         @(posedge clk);
         #1;
         reset_n = 1'b1;
      end else begin
         @(negedge clk);
         op_set = iop;
         A = iA;
         B = iB;
         start = 1'b1;
         if (iop == no_op) begin
            @(posedge clk);
            #1;
            start = 1'b0;
         end else begin
            // +BUG=1: changes B halfway through the multiplication. The
            // multiplier already latched A and B on the first edge, so the
            // RESULT DOES NOT CHANGE: the scoreboard stays green. The only
            // thing that sees it is the assertion. That is the whole section.
            if (bug_operandos && iop == mul_op) begin
               @(negedge clk);
               @(negedge clk);
               B = ~iB;
            end
            do @(negedge clk); while (done == 0);
            oresult   = result;
            start = 1'b0;
         end
      end  // else: !if(iop == rst_op)
   endtask : send_op


   // ==========================================================================
   //  The protocol, checked where it happens
   // ==========================================================================
   //
   // The properties live HERE, with the signals, and not in the testbench: they
   // plug themselves in, nobody connects them, and the passive agent of the Agents
   // section gets them for free. All they need in order to run is --assert.

   // TWO CLOCKS, and it is not an implementation detail: the BFM drives on
   // negedge and the DUT registers on posedge. An assertion samples in the
   // preponed region of the edge it is given, so a signal written ON the negedge
   // is not seen on that negedge: it is seen on the next one. With everything on
   // posedge, two consecutive no_op -- start goes down at t=111 and back up at
   // t=120, between two posedges -- read as ONE transaction with the operands
   // changing: 145 false positives every 1000 operations. With everything on
   // negedge, the false positives move to the done properties.
   //
   //   stimulus (start, A, B, op_set)  -> negedge, where the BFM writes
   //   response (done, result)         -> posedge, where the DUT registers

   default disable iff (!reset_n);

   // --- The stimulus ---

   // The rule from slide 1 of day 1, executable at last: while start is up, the
   // operands and the operation are not touched.
   property p_operandos_estables;
      @(negedge clk) start |=> $stable(A) && $stable(B) && $stable(op_set);
   endproperty : p_operandos_estables

   a_operandos_estables :
   assert property (p_operandos_estables)
   else
      `uvm_error("SVA", $sformatf(
                 "%m: operand changed with start up: A=%0d B=%0d op=%s", A, B, op2enum().name()))

   // --- The DUT's answer ---

   // The variable latency from the VTALU spec section, in one line: one cycle for the
   // one-cycle ops, four edges for the multiplication.
   property p_done_llega;
      @(posedge clk) start && (op_set != no_op) |-> ##[1:5] done;
   endproperty : p_done_llega

   a_done_llega :
   assert property (p_done_llega)
   else `uvm_error("SVA", $sformatf("%m: start con op=%s y done no llego en 5 ciclos", op2enum().name()))

   // The fine print: no_op is the only operation that does not answer.
   property p_no_op_sin_done;
      @(posedge clk) start && (op_set == no_op) |=> !done;
   endproperty : p_no_op_sin_done

   a_no_op_sin_done :
   assert property (p_no_op_sin_done)
   else `uvm_error("SVA", $sformatf("%m: done subio para una no_op"))

   // --- Every assertion comes with its cover property ---
   //
   // An assertion whose antecedent never happens PASSES, and checks nothing.
   // The cover is the antidote. And it also debunks mental models: the
   // "three-cycle" multiplication takes FOUR edges (done3 -> done2 ->
   // done1 -> done_mult), so c_mult_3ciclos stays at 0 forever.
   // --- VTALU rev2: the output the scoreboard only glances at ---

   // ovf belongs to sub and to nobody else. An assertion, because it is a rule of
   // the spec and not arithmetic: the scoreboard checks WHAT it computes, this
   // checks that it does not invent a flag where none belongs.
   property p_ovf_solo_en_sub;
      @(posedge clk) done && (op_set != sub_op) |-> !ovf;
   endproperty : p_ovf_solo_en_sub

   a_ovf_solo_en_sub :
   assert property (p_ovf_solo_en_sub)
   else `uvm_error("SVA", $sformatf("%m: ovf arriba con op=%s, que no puede desbordar", op2enum().name()))

   // And the cover that goes with it: without this, a regression where the random
   // never subtracted too much leaves the assertion green having checked nothing.
   c_ovf : cover property (@(posedge clk) done && ovf);
   c_sub_sin_borrow : cover property (@(posedge clk) done && (op_set == sub_op) && !ovf);

   c_mult_3ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##3 done);
   c_mult_4ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##4 done);
   c_un_ciclo : cover property (@(posedge clk) $rose(start) && (op_set inside {add_op, sub_op, and_op, xor_op}) ##1 done);

endinterface : vtalu_bfm

interface vtalu_bfm;
   import uvm_pkg::*;
   import vtalu_pkg::*;
   `include "uvm_macros.svh"

   byte unsigned          A;
   byte unsigned          B;
   bit                    clk;
   bit                    reset_n;
   bit                    start;
   wire                   done;
   wire            [15:0] result;
   wire                   ovf;
   operation_t            op_set;

   command_monitor        command_monitor_h;

   function operation_t op2enum();
      case (op_set)
         3'b000:  return no_op;
         3'b001:  return add_op;
         3'b010:  return sub_op;
         3'b011:  return and_op;
         3'b100:  return xor_op;
         3'b101:  return mul_op;
         default: $fatal(1, "Illegal operation on op bus");
      endcase  // case (op_set)
   endfunction : op2enum

   always @(posedge clk) begin : op_monitor
      static bit in_command = 0;
      // The null guard rst_monitor already had, now here too. With two BFMs in
      // the top, one can be left without a monitor while the testbench is being
      // built -- or forever, if someone forgets to instantiate the passive
      // agent. Without the guard that is a simulator crash instead of a
      // testbench that sees nothing.
      if (command_monitor_h != null) begin : con_monitor
         if (start) begin : start_high
            if (!in_command) begin : new_command
               command_monitor_h.write_to_monitor(A, B, op2enum());
               in_command = (op2enum() != no_op);
            end : new_command
         end : start_high
         else  // start low
            in_command = 0;
      end : con_monitor
   end : op_monitor

   always @(negedge reset_n) begin : rst_monitor
      if (command_monitor_h != null)  //guard against VCS time 0 negedge
         command_monitor_h.write_to_monitor(A, B, rst_op);
   end : rst_monitor

   result_monitor result_monitor_h;

   initial begin : result_monitor_thread
      forever begin : result_monitor
         @(posedge clk);
         // Same guard as op_monitor and rst_monitor: with two BFMs in the top,
         // one can be left without a monitor. Without this, forgetting the
         // passive agent is a simulator "Null pointer dereferenced" instead of
         // the checker's message -- which is exactly where exercise d6 starts.
         if (done && result_monitor_h != null) result_monitor_h.write_to_monitor(result, ovf);
      end : result_monitor
   end : result_monitor_thread

   initial begin
      clk = 0;
      forever begin
         #10;
         clk = ~clk;
      end
   end


   // --- the protocol, in the BFM ---
   // Everything that knows HOW the DUT is talked to lives here, in one place:
   // the rest of the testbench asks for an operation and never touches a wire.
   // That is the idea of the interfaces-and-BFM section, and it holds to the end of the course.

   task reset_alu();
      reset_n = 1'b0;
      @(negedge clk);
      @(negedge clk);
      reset_n = 1'b1;
      start   = 1'b0;
   endtask : reset_alu

   // NEW with the sequences: the fourth argument. The protocol did not change; the only
   // thing added is reading result on the edge where done is already up.
   bit bug_operandos;
   initial bug_operandos = $test$plusargs("BUG");

   task send_op(input byte iA, input byte iB, input operation_t iop,
                output shortint unsigned oresult);
      oresult = 0;
      if (iop == rst_op) begin
         @(posedge clk);
         reset_n = 1'b0;
         start   = 1'b0;
         @(posedge clk);
         #1;
         reset_n = 1'b1;
      end else begin
         @(negedge clk);
         op_set = iop;
         A = iA;
         B = iB;
         start = 1'b1;
         if (iop == no_op) begin
            @(posedge clk);
            #1;
            start = 1'b0;
         end else begin
            // +BUG=1: changes B halfway through the multiplication. The
            // multiplier already latched A and B on the first edge, so the
            // RESULT DOES NOT CHANGE: the scoreboard stays green. The only
            // thing that sees it is the assertion. That is the whole section.
            if (bug_operandos && iop == mul_op) begin
               @(negedge clk);
               @(negedge clk);
               B = ~iB;
            end
            do @(negedge clk); while (done == 0);
            oresult   = result;
            start = 1'b0;
         end
      end  // else: !if(iop == rst_op)
   endtask : send_op


   // ==========================================================================
   //  The protocol, checked where it happens
   // ==========================================================================
   //
   // The properties live HERE, with the signals, and not in the testbench: they
   // plug themselves in, nobody connects them, and the passive agent of the Agents
   // section gets them for free. All they need in order to run is --assert.

   // TWO CLOCKS, and it is not an implementation detail: the BFM drives on
   // negedge and the DUT registers on posedge. An assertion samples in the
   // preponed region of the edge it is given, so a signal written ON the negedge
   // is not seen on that negedge: it is seen on the next one. With everything on
   // posedge, two consecutive no_op -- start goes down at t=111 and back up at
   // t=120, between two posedges -- read as ONE transaction with the operands
   // changing: 145 false positives every 1000 operations. With everything on
   // negedge, the false positives move to the done properties.
   //
   //   stimulus (start, A, B, op_set)  -> negedge, where the BFM writes
   //   response (done, result)         -> posedge, where the DUT registers

   default disable iff (!reset_n);

   // --- The stimulus ---

   // The rule from slide 1 of day 1, executable at last: while start is up, the
   // operands and the operation are not touched.
   property p_operandos_estables;
      @(negedge clk) start |=> $stable(A) && $stable(B) && $stable(op_set);
   endproperty : p_operandos_estables

   a_operandos_estables :
   assert property (p_operandos_estables)
   else
      `uvm_error("SVA", $sformatf(
                 "%m: operand changed with start up: A=%0d B=%0d op=%s", A, B, op2enum().name()))

   // --- The DUT's answer ---

   // The variable latency from the VTALU spec section, in one line: one cycle for the
   // one-cycle ops, four edges for the multiplication.
   property p_done_llega;
      @(posedge clk) start && (op_set != no_op) |-> ##[1:5] done;
   endproperty : p_done_llega

   a_done_llega :
   assert property (p_done_llega)
   else `uvm_error("SVA", $sformatf("%m: start con op=%s y done no llego en 5 ciclos", op2enum().name()))

   // The fine print: no_op is the only operation that does not answer.
   property p_no_op_sin_done;
      @(posedge clk) start && (op_set == no_op) |=> !done;
   endproperty : p_no_op_sin_done

   a_no_op_sin_done :
   assert property (p_no_op_sin_done)
   else `uvm_error("SVA", $sformatf("%m: done subio para una no_op"))

   // --- Every assertion comes with its cover property ---
   //
   // An assertion whose antecedent never happens PASSES, and checks nothing.
   // The cover is the antidote. And it also debunks mental models: the
   // "three-cycle" multiplication takes FOUR edges (done3 -> done2 ->
   // done1 -> done_mult), so c_mult_3ciclos stays at 0 forever.
   // --- VTALU rev2: the output the scoreboard only glances at ---

   // ovf belongs to sub and to nobody else. An assertion, because it is a rule of
   // the spec and not arithmetic: the scoreboard checks WHAT it computes, this
   // checks that it does not invent a flag where none belongs.
   property p_ovf_solo_en_sub;
      @(posedge clk) done && (op_set != sub_op) |-> !ovf;
   endproperty : p_ovf_solo_en_sub

   a_ovf_solo_en_sub :
   assert property (p_ovf_solo_en_sub)
   else `uvm_error("SVA", $sformatf("%m: ovf arriba con op=%s, que no puede desbordar", op2enum().name()))

   // And the cover that goes with it: without this, a regression where the random
   // never subtracted too much leaves the assertion green having checked nothing.
   c_ovf : cover property (@(posedge clk) done && ovf);
   c_sub_sin_borrow : cover property (@(posedge clk) done && (op_set == sub_op) && !ovf);

   c_mult_3ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##3 done);
   c_mult_4ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##4 done);
   c_un_ciclo : cover property (@(posedge clk) $rose(start) && (op_set inside {add_op, sub_op, and_op, xor_op}) ##1 done);

endinterface : vtalu_bfm

interface vtalu_bfm;
   import uvm_pkg::*;
   import vtalu_pkg::*;
   `include "uvm_macros.svh"

   byte unsigned          A;
   byte unsigned          B;
   bit                    clk;
   bit                    reset_n;
   bit                    start;
   wire                   done;
   wire            [15:0] result;
   wire                   ovf;
   operation_t            op_set;

   command_monitor        command_monitor_h;

   function operation_t op2enum();
      case (op_set)
         3'b000:  return no_op;
         3'b001:  return add_op;
         3'b010:  return sub_op;
         3'b011:  return and_op;
         3'b100:  return xor_op;
         3'b101:  return mul_op;
         default: $fatal(1, "Illegal operation on op bus");
      endcase  // case (op_set)
   endfunction : op2enum

   always @(posedge clk) begin : op_monitor
      static bit in_command = 0;
      // The null guard rst_monitor already had, now here too. With two BFMs in
      // the top, one can be left without a monitor while the testbench is being
      // built -- or forever, if someone forgets to instantiate the passive
      // agent. Without the guard that is a simulator crash instead of a
      // testbench that sees nothing.
      if (command_monitor_h != null) begin : con_monitor
         if (start) begin : start_high
            if (!in_command) begin : new_command
               command_monitor_h.write_to_monitor(A, B, op2enum());
               in_command = (op2enum() != no_op);
            end : new_command
         end : start_high
         else  // start low
            in_command = 0;
      end : con_monitor
   end : op_monitor

   always @(negedge reset_n) begin : rst_monitor
      if (command_monitor_h != null)  //guard against VCS time 0 negedge
         command_monitor_h.write_to_monitor(A, B, rst_op);
   end : rst_monitor

   result_monitor result_monitor_h;

   initial begin : result_monitor_thread
      forever begin : result_monitor
         @(posedge clk);
         // Same guard as op_monitor and rst_monitor: with two BFMs in the top,
         // one can be left without a monitor. Without this, forgetting the
         // passive agent is a simulator "Null pointer dereferenced" instead of
         // the checker's message -- which is exactly where exercise d6 starts.
         if (done && result_monitor_h != null) result_monitor_h.write_to_monitor(result, ovf);
      end : result_monitor
   end : result_monitor_thread

   initial begin
      clk = 0;
      forever begin
         #10;
         clk = ~clk;
      end
   end


   // --- the protocol, in the BFM ---
   // Everything that knows HOW the DUT is talked to lives here, in one place:
   // the rest of the testbench asks for an operation and never touches a wire.
   // That is the idea of the interfaces-and-BFM section, and it holds to the end of the course.

   task reset_alu();
      reset_n = 1'b0;
      @(negedge clk);
      @(negedge clk);
      reset_n = 1'b1;
      start   = 1'b0;
   endtask : reset_alu

   // NEW with the sequences: the fourth argument. The protocol did not change; the only
   // thing added is reading result on the edge where done is already up.
   bit bug_operandos;
   initial bug_operandos = $test$plusargs("BUG");

   task send_op(input byte iA, input byte iB, input operation_t iop,
                output shortint unsigned oresult);
      oresult = 0;
      if (iop == rst_op) begin
         @(posedge clk);
         reset_n = 1'b0;
         start   = 1'b0;
         @(posedge clk);
         #1;
         reset_n = 1'b1;
      end else begin
         @(negedge clk);
         op_set = iop;
         A = iA;
         B = iB;
         start = 1'b1;
         if (iop == no_op) begin
            @(posedge clk);
            #1;
            start = 1'b0;
         end else begin
            // +BUG=1: changes B halfway through the multiplication. The
            // multiplier already latched A and B on the first edge, so the
            // RESULT DOES NOT CHANGE: the scoreboard stays green. The only
            // thing that sees it is the assertion. That is the whole section.
            if (bug_operandos && iop == mul_op) begin
               @(negedge clk);
               @(negedge clk);
               B = ~iB;
            end
            do @(negedge clk); while (done == 0);
            oresult   = result;
            start = 1'b0;
         end
      end  // else: !if(iop == rst_op)
   endtask : send_op


   // ==========================================================================
   //  The protocol, checked where it happens
   // ==========================================================================
   //
   // The properties live HERE, with the signals, and not in the testbench: they
   // plug themselves in, nobody connects them, and the passive agent of the Agents
   // section gets them for free. All they need in order to run is --assert.

   // TWO CLOCKS, and it is not an implementation detail: the BFM drives on
   // negedge and the DUT registers on posedge. An assertion samples in the
   // preponed region of the edge it is given, so a signal written ON the negedge
   // is not seen on that negedge: it is seen on the next one. With everything on
   // posedge, two consecutive no_op -- start goes down at t=111 and back up at
   // t=120, between two posedges -- read as ONE transaction with the operands
   // changing: 145 false positives every 1000 operations. With everything on
   // negedge, the false positives move to the done properties.
   //
   //   stimulus (start, A, B, op_set)  -> negedge, where the BFM writes
   //   response (done, result)         -> posedge, where the DUT registers

   default disable iff (!reset_n);

   // --- The stimulus ---

   // The rule from slide 1 of day 1, executable at last: while start is up, the
   // operands and the operation are not touched.
   property p_operandos_estables;
      @(negedge clk) start |=> $stable(A) && $stable(B) && $stable(op_set);
   endproperty : p_operandos_estables

   a_operandos_estables :
   assert property (p_operandos_estables)
   else
      `uvm_error("SVA", $sformatf(
                 "%m: operand changed with start up: A=%0d B=%0d op=%s", A, B, op2enum().name()))

   // --- The DUT's answer ---

   // The variable latency from the VTALU spec section, in one line: one cycle for the
   // one-cycle ops, four edges for the multiplication.
   property p_done_llega;
      @(posedge clk) start && (op_set != no_op) |-> ##[1:5] done;
   endproperty : p_done_llega

   a_done_llega :
   assert property (p_done_llega)
   else `uvm_error("SVA", $sformatf("%m: start con op=%s y done no llego en 5 ciclos", op2enum().name()))

   // The fine print: no_op is the only operation that does not answer.
   property p_no_op_sin_done;
      @(posedge clk) start && (op_set == no_op) |=> !done;
   endproperty : p_no_op_sin_done

   a_no_op_sin_done :
   assert property (p_no_op_sin_done)
   else `uvm_error("SVA", $sformatf("%m: done subio para una no_op"))

   // --- Every assertion comes with its cover property ---
   //
   // An assertion whose antecedent never happens PASSES, and checks nothing.
   // The cover is the antidote. And it also debunks mental models: the
   // "three-cycle" multiplication takes FOUR edges (done3 -> done2 ->
   // done1 -> done_mult), so c_mult_3ciclos stays at 0 forever.
   // --- VTALU rev2: the output the scoreboard only glances at ---

   // ovf belongs to sub and to nobody else. An assertion, because it is a rule of
   // the spec and not arithmetic: the scoreboard checks WHAT it computes, this
   // checks that it does not invent a flag where none belongs.
   property p_ovf_solo_en_sub;
      @(posedge clk) done && (op_set != sub_op) |-> !ovf;
   endproperty : p_ovf_solo_en_sub

   a_ovf_solo_en_sub :
   assert property (p_ovf_solo_en_sub)
   else `uvm_error("SVA", $sformatf("%m: ovf arriba con op=%s, que no puede desbordar", op2enum().name()))

   // And the cover that goes with it: without this, a regression where the random
   // never subtracted too much leaves the assertion green having checked nothing.
   c_ovf : cover property (@(posedge clk) done && ovf);
   c_sub_sin_borrow : cover property (@(posedge clk) done && (op_set == sub_op) && !ovf);

   c_mult_3ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##3 done);
   c_mult_4ciclos : cover property (@(posedge clk) $rose(start) && (op_set == mul_op) ##4 done);
   c_un_ciclo : cover property (@(posedge clk) $rose(start) && (op_set inside {add_op, sub_op, and_op, xor_op}) ##1 done);

endinterface : vtalu_bfm

// The capstone DUT: an APB3 slave with four registers.
//
// The spec is in spec.md, and it is the only thing to read in order to verify it.
// This file is NOT touched: if your testbench needs to change the RTL to pass,
// the one that is wrong is the testbench.
//
// The only liberty taken is bug_en, which would not exist in a real DUT:
// with +BUG=1 the accumulator stops looking at CTRL.EN. It is there so you can
// check that your scoreboard checks something -- a scoreboard that never saw an
// error is not tested.
module apb_regs (
    input  logic        PCLK,
    input  logic        PRESETn,
    input  logic        PSEL,
    input  logic        PENABLE,
    input  logic        PWRITE,
    input  logic [ 7:0] PADDR,
    input  logic [31:0] PWDATA,
    input  logic        bug_en,
    output logic [31:0] PRDATA,
    output logic        PREADY,
    output logic        PSLVERR
);

   logic        en;       // CTRL[0]
   logic        ovf;      // STATUS[1], pegajoso
   logic [31:0] scratch;  // SCRATCH
   logic [31:0] acc;      // ACC

   // The map fits in 16 bytes: four 32-bit registers. PADDR[1:0] is
   // ignored; from 0x10 up there is nobody and the answer is PSLVERR.
   wire mapped = (PADDR < 8'h10);
   wire access = PSEL && PENABLE;

   // The handshake: the write does not wait, the read inserts ONE wait state.
   // rd_wait re-arms as soon as PENABLE drops, that is between one transfer and
   // the next, with no need to count cycles.
   logic rd_wait;
   always_ff @(posedge PCLK or negedge PRESETn) begin
      if (!PRESETn) rd_wait <= 1'b1;
      else if (!PENABLE) rd_wait <= 1'b1;
      else if (access && !PWRITE) rd_wait <= 1'b0;
   end

   assign PREADY  = !PSEL ? 1'b1 : (PWRITE ? 1'b1 : !rd_wait);
   assign PSLVERR = access && !mapped;

   // The cycle where the transfer actually happens: it is the only edge that
   // matters to the monitor, and the only one where the DUT changes state.
   wire xfer = access && PREADY;

   always_comb begin
      PRDATA = 32'h0;
      if (mapped)
         case (PADDR[3:2])
            2'd0: PRDATA = {31'h0, en};        // CTRL: CLR es autoclear, lee 0
            2'd1: PRDATA = scratch;
            2'd2: PRDATA = acc;
            default: PRDATA = {30'h0, ovf, en};  // STATUS
         endcase
   end

   logic [32:0] suma;
   assign suma = {1'b0, acc} + {1'b0, PWDATA};

   always_ff @(posedge PCLK or negedge PRESETn) begin
      if (!PRESETn) begin
         en      <= 1'b0;
         ovf     <= 1'b0;
         scratch <= 32'h0;
         acc     <= 32'h0;
      end else if (xfer && PWRITE && mapped) begin
         case (PADDR[3:2])
            2'd0: begin
               en <= PWDATA[0];
               if (PWDATA[1]) begin  // CLR
                  acc <= 32'h0;
                  ovf <= 1'b0;
               end
            end
            2'd1: begin
               scratch <= PWDATA;
               // The accumulator only runs with EN=1. It is the only line
               // +BUG=1 breaks.
               if (en || bug_en) begin
                  acc <= suma[31:0];
                  if (suma[32]) ovf <= 1'b1;  // sticky until the next CLR
               end
            end
            default: ;  // ACC and STATUS are read-only: the write is ignored
         endcase
      end
   end

endmodule : apb_regs