Formal

[Harshitha172000]

Formal Verification of Mor1kx using yosys formal tools. Assertions added to the source files can be tested using SBY files (Path: bench/formal).

[stffrdhrn]

https://chris.beams.io/posts/git-commit/#why-not-how

[stffrdhrn]

Can you add this to our github actions CI? I think we can start merging the changes after a few things are fixed.

1. The tests all pass, I am getting a failure on lsu
2. Some of the review comments are addressed
3. Sorry its a bit late, but I think you need to clean up your git commit comments, read the article I posted.
   • https://chris.beams.io/posts/git-commit/
   • Your commit descriptions are not up to our standards i.e. a recent commit formal test branch that doesnt explain what the change is.
   • You will need to rebase and reword your git commits
   • I recommend squash and fixup to reduce your commits rather than just adding new commits. i.e. after a code review you can just fixup/amend a commit rather than adding a commit that says "FIx as per PR comments"
   • Add a commit body explaining why the changes are needed

[Harshitha172000]

LSU passes the formal test now.

I think assertions to cpu_cappuccino are not enough, and there is no point in asserting the same properties which are added in the submodules. How should I proceed further with this top module testing?

Also, what should I add to git actions ci?

[stffrdhrn]

LSU passes the formal test now.

I think assertions to cpu_cappuccino are not enough, and there is no point in asserting the same properties which are added in the submodules. How should I proceed further with this top module testing?

Look at riscv-formal run it understand how it works. We can think about doing something similar.

Also, what should I add to git actions ci?

Look at the file .github/workflows/ci.yml please add a step to install yosys symbiyosis and run the make -C bench/formal tests.

Next time when you comment. Its better to respond to the comments where I made them, I cannot recall some of the context of these questions. Others in the future will have a really hard time to see the context.

[Harshitha172000]

Edited PR with the following changes:

1. Removed reset assertions on internal state variables.
2. Moved assertions from the CPU module to respective submodules.
3. Reduced internal state assertions up to some extent.

Submodules still have spr assertions. I will clean it up once I add the spr interface.

[Harshitha172000]

You have added fspr_master and fspr_slave to this commit. On the call I asked you to keep this on a separate branch i.e. formal-spr like you did with formal-ci. That way we can review this separately.

Can you remove this from the commit and do the work on a separate branch/PR?

I have removed my last commit and moved the spr interface to formal-spr PR.

[Harshitha172000]

I have added unknown tests in ALU and PCU too. Shall I remove those tests?

[stffrdhrn]

I have added unknown tests in ALU and PCU too. Shall I remove those tests?

I think so, I would like them to be removed everywhere for now.

[Harshitha172000]

Changes done:

1. Fixed issues with Store Buffer.
2. Added assertions to tick timer.
3. Removed unknown test from the register file, pcu, pic, and alu.

[Harshitha172000]

Added checks for the serial features like multiplier, divider, and shifter. Let me know if the approach used is correct. We need to update the SBY file when the feature type is changed. Shall I add tasks for all features? This may create too many execute_alu directories after the test.

[stffrdhrn]

Added checks for the serial features like multiplier, divider, and shifter. Let me know if the approach used is correct. We need to update the SBY file when the feature type is changed. Shall I add tasks for all features? This may create too many execute_alu directories after the test.

I think adding the tasks is good if it all passes. The extra directories is not an issue, how much more time will it take?

[Harshitha172000]

I think adding the tasks is good if it all passes. The extra directories is not an issue, how much more time will it take?

All tests pass and I have added four tasks. Tags just specify parameters that are set. I tried using tags in pycode to set parameters but yosys shows an error while decoding string parameters, so not using pycode. The entire alu test may take one or two minutes.

[Harshitha172000]

Modified check for Three-stage multiplier. Previously, input assumption fails during the top module test. So, verification was limited to ALU.

Before

`ifdef ALU
   //Three stage Multiplier takes 3clks to output the result
   always @(posedge clk) begin
      if (FEATURE_MULTIPLIER == "THREESTAGE" &&
          $past(op_mul_i,3) && f_past_valid &&
          !$past(rst) && !$past(rst,2) && !$past(rst,3))
         //Assume multiplication opcode is valid for three clock cycles
         assume ($past(op_mul_i) && $past(op_mul_i,2));
   end
   //MULTIPLICATION: THREE STAGE
   always @(posedge clk) begin
      if (!$past(op_mul_i,4) && $past(op_mul_i,3) &&
          f_past_valid && FEATURE_MULTIPLIER == "THREESTAGE"
          && !$past(rst) && !$past(rst,2) && !$past(rst,3) &&
          mul_valid && $past(decode_valid_i,4) && !$past(rst,4)) begin
         //Stall three clock cycles
         assert ($past(alu_stall) && $past(alu_stall,2) && $past(alu_stall,3));
         //After completion, no stall
         assert (!alu_stall);
         assert (alu_valid_o);
      end
   end
`endif

After investigation, I noticed that pipeline_flush_i affects input assumption due to which test fails in CPU.

Modified code

   //MULTIPLICATION: THREE STAGE
   reg f_op_mul;
   initial f_op_mul = 0;

   always @(posedge clk) begin
      if (FEATURE_MULTIPLIER == "THREESTAGE"
          && f_past_valid && !$past(rst)) begin
          if ($rose(op_mul_i) && !mul_valid && !pipeline_flush_i)
             f_op_mul <= 1;
          if (($rose(f_op_mul) || (!$past(f_op_mul,2) && $past(f_op_mul))) 
              && ((!$past(pipeline_flush_i) && !pipeline_flush_i) ||
              !pipeline_flush_i))
             `ASSUME ($stable(op_mul_i));
          if ((!$past(f_op_mul,2) && $past(f_op_mul) && !$past(rst,2)
              && op_mul_i) || !pipeline_flush_i || !op_mul_i)
             f_op_mul <= 0;
      end
   end

   always @(posedge clk)
      if (FEATURE_MULTIPLIER == "THREESTAGE" && !$past(op_mul_i,4)
          && $past(op_mul_i,3) && mul_valid && $past(decode_valid_i,4) &&
          f_past_valid &&  !$past(rst) && !$past(rst,2) && !$past(rst,3) &&
          !$past(rst,4) && !(op_div_i | op_mul_i | fpu_op_is_arith |
          fpu_op_is_cmp | op_shift_i | op_ffl1_i) && $fell(f_op_mul)) begin
         //Stall three clock cycles
         assert ($past(alu_stall) && $past(alu_stall,2) && $past(alu_stall,3));
         //After execution, no stall
         assert (!alu_stall);
         assert (alu_valid_o);
      end

The additional condition has been added to avoid ALU stall after completing execution. These opcode's arrival in the 4th clock cycle may result in alu_stall and may delay valid signal.