Browse Source

Use SVA defaults for clock & reset; minor RTL optimizations for bettrer readability

verific
T. Meissner 6 years ago
parent
commit
ac767bb9d3
3 changed files with 37 additions and 26 deletions
  1. +13
    -11
      alu/alu.vhd
  2. +13
    -8
      alu/alu_t.sv
  3. +11
    -7
      counter/counter_t.sv

+ 13
- 11
alu/alu.vhd View File

@ -24,10 +24,12 @@ end entity alu;
architecture rtl of alu is
constant c_add : std_logic_vector(1 downto 0) := "00";
constant c_sub : std_logic_vector(1 downto 0) := "01";
constant c_and : std_logic_vector(1 downto 0) := "10";
constant c_or : std_logic_vector(1 downto 0) := "11";
subtype t_opc is std_logic_vector(Opc_i'length-1 downto 0);
constant c_add : t_opc := "00";
constant c_sub : t_opc := "01";
constant c_and : t_opc := "10";
constant c_or : t_opc := "11";
begin
@ -40,14 +42,14 @@ begin
elsif (rising_edge(Clk_i)) then
case Opc_i is
when c_add => (OverFlow_o, Dout_o) <=
std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) +
resize(unsigned(DinB_i), Dout_o'length+1));
std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) +
resize(unsigned(DinB_i), Dout_o'length+1));
when c_sub => (OverFlow_o, Dout_o) <=
std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) -
resize(unsigned(DinB_i), Dout_o'length+1));
when c_and => Dout_o <= DinA_i and DinB_i;
when c_or => Dout_o <= DinA_i or DinB_i;
when others => null;
std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) -
resize(unsigned(DinB_i), Dout_o'length+1));
when c_and => Dout_o <= DinA_i and DinB_i;
when c_or => Dout_o <= DinA_i or DinB_i;
when others => null;
end case;
end if;
end process;


+ 13
- 8
alu/alu_t.sv View File

@ -41,24 +41,29 @@ module alu_t (
always @(posedge Clk_i)
init_state = 0;
default clocking
@(posedge Clk_i);
endclocking
default disable iff (!Reset_n_i);
bit unsigned [`WIDTH:0] dina, dinb;
assign dina = DinA_i;
assign dinb = DinB_i;
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_ADD && (dina + dinb) > 2**`WIDTH-1 |=> OverFlow_o);
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_SUB && (dina - dinb) > 2**`WIDTH-1 |=> OverFlow_o);
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i)));
assert property (Opc_i == `OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
assert property (Opc_i == `OPC_ADD && (dina + dinb) > 2**`WIDTH-1 |=> OverFlow_o);
assert property (Opc_i == `OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
assert property (Opc_i == `OPC_SUB && (dina - dinb) > 2**`WIDTH-1 |=> OverFlow_o);
assert property (Opc_i == `OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
assert property (Opc_i == `OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i)));
property cover_opc (opc);
@(posedge Clk_i)
disable iff (!Reset_n_i) Opc_i == opc;
Opc_i == opc;
endproperty
cover property (cover_opc(`OPC_ADD));


+ 11
- 7
counter/counter_t.sv View File

@ -38,19 +38,23 @@ module counter_t (
// Use global clock to constrain the DUT clock
always @($global_clock) begin
assume(Clk_i != $past(Clk_i));
assume (Clk_i != $past(Clk_i));
end
default clocking
@(posedge Clk_i);
endclocking
default disable iff (!Reset_n_i);
// Immediate assertions
always @(*)
if (!Reset_n_i) assert (Data_o == `INITVAL);
// Fails with unbounded prove using SMTBMC, maybe
// the assumptions/assertions have to be more strict.
// With abc pdr this can be successfully proved.
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o < `ENDVAL |=> Data_o == $past(Data_o) + 1);
assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o == `ENDVAL |=> $stable(Data_o));
assert property (@(posedge Clk_i) Data_o >= `INITVAL && Data_o <= `ENDVAL);
// Concurrent assertions
assert property (Data_o < `ENDVAL |=> Data_o == $past(Data_o) + 1);
assert property (Data_o == `ENDVAL |=> $stable(Data_o));
assert property (Data_o >= `INITVAL && Data_o <= `ENDVAL);
endmodule


Loading…
Cancel
Save