Skip to content

Commit

Permalink
ctrl: Update formal to fix on new yosys
Browse files Browse the repository at this point in the history
This was failing on newer versions of yosys.  The assert is
not true when we are testing the control unit alone as any
input can come in, we update to only check this for CPU level tests.

Also we remove the spr_access_valid assert which is just checking the
properties of an assign.
  • Loading branch information
stffrdhrn committed May 16, 2022
1 parent 2863278 commit 1a8c19b
Showing 1 changed file with 2 additions and 5 deletions.
7 changes: 2 additions & 5 deletions rtl/verilog/mor1kx_ctrl_cappuccino.v
Original file line number Diff line number Diff line change
Expand Up @@ -1624,14 +1624,11 @@ endgenerate
if (f_past_valid && !$past(rst) && $rose(ctrl_bubble_o))
assert ($past(execute_bubble_i));

`ifndef CTRL
//SPR shouldn't give more than one acknowledgement
always @*
assert ($onehot0(spr_access_ack));

//SPR acknowledgement makes spr access valid
always @*
if ($onehot(spr_access_ack))
assert (spr_access_valid);
`endif

//Insn mfspr should always read from spr and
//insn mtspr should always write to spr.
Expand Down

0 comments on commit 1a8c19b

Please sign in to comment.