Trying to verify Verilog/VHDL designs with formal methods and tools
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

57 lines
1.7 KiB

4 years ago
4 years ago
  1. module alu_t (
  2. input Reset_n_i,
  3. input Clk_i,
  4. input [1:0] Opc_i,
  5. input [31:0] DinA_i,
  6. input [31:0] DinB_i,
  7. output [31:0] Dout_o,
  8. output OverFlow_o
  9. );
  10. alu alu_i (
  11. .Reset_n_i(Reset_n_i),
  12. .Clk_i(Clk_i),
  13. .Opc_i(Opc_i),
  14. .DinA_i(DinA_i),
  15. .DinB_i(DinB_i),
  16. .Dout_o(Dout_o),
  17. .OverFlow_o(OverFlow_o)
  18. );
  19. const logic [1:0] OPC_ADD = 0;
  20. const logic [1:0] OPC_SUB = 1;
  21. const logic [1:0] OPC_AND = 2;
  22. const logic [1:0] OPC_OR = 3;
  23. initial begin
  24. assume (!Reset_n_i);
  25. end
  26. bit unsigned [32:0] dina, dinb;
  27. assign dina = DinA_i;
  28. assign dinb = DinB_i;
  29. assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
  30. assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_ADD && (dina + dinb) > 2**32-1 |=> OverFlow_o);
  31. assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
  32. assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_SUB && (dina - dinb) > 2**32-1 |=> OverFlow_o);
  33. assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
  34. assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i)));
  35. assert property (@(posedge Clk_i or negedge Clk_i) !Reset_n_i |-> Dout_o == 0);
  36. property cover_opc (opc);
  37. @(posedge Clk_i)
  38. disable iff (!Reset_n_i) Opc_i == opc;
  39. endproperty
  40. cover property (cover_opc(OPC_ADD));
  41. cover property (cover_opc(OPC_SUB));
  42. cover property (cover_opc(OPC_AND));
  43. cover property (cover_opc(OPC_OR));
  44. endmodule