RTL Subsetting: Extracting a Smaller RTL that Preserves a Subset of Functionality

Abstract.

Improving the scalability of formal verification and simulation of Register-Transfer-Level hardware design including hardware accelerators and processors is becoming an increasingly heated topic. Although various techniques such as abstraction, decomposition etc. have been applied to improve the scalibility, they are all aimed at general-purpose RTLs, i.e. they assume that the RTL’s functionality all needs to be verified or simulated and thus try to simply these tasks for the whole RTL. However, a neglected scenario is that only a subset of a RTL’s functionality (e.g. an instruction subset) will be used, which is common for accelerators with multiple functional modules. This means verification and simulation may be conducted only for a subset of the whole RTL, which becomes easier due to the reduced RTL size. This paper presents a brand-new technique to get a RTL subset that preserves a subset of functionalities of the whole RTL. More specifically, given an instruction subset that specifies the functionality subset, this technique enables us to find a RTL subset that suffices this instruction subset. In the paper, RTL subsetting is conducted on the module instance level of the RTL through an algorithm that determines which instances should be removed and finally outputs a RTL subset. Experiments on different sized accelerators and processors demonstrate that our technique has a satisfying performance even on large RTLs with over 50,000 registers.

1. 1

Algorithm 0 Removability Check 0

1:Subset Assumptions

A

, RTL

R

, Module Instance

inst

result

;

3:for Every output

o_{i}

inst

4: for Every possible value

v_{j}

o_{i}

R^{\prime}\leftarrow

Replacing

o_{i}

in R with

v_{j}

equal_{j}\leftarrow EqualCheck(R,R^{\prime},A)

7: end for

removable_{i}=\bigcup\limits_{j}equal_{j}

9:end for

10:

removable=\bigcap\limits_{i}removable_{i}

11:return

removable

2. 1

Algorithm 1 Removability Check 1

1:Subset Assumptions

A

, RTL

R

, module instance

inst

, Time Limit

time

removable

;

\triangleright

true

false

timeout

unobs\_check\leftarrow\{\}

4:for Every output

o_{i}

inst

unctrl\leftarrow unctrl\_single\_check(A,R,o_{i},time)

6: if

unctrl!=true

then

unobs\_check=\{\}

7: else

8: end if

9:end for

10:

removable=\bigcap\limits_{i}removable_{i}

11:return

removable

⬇

1input clk;

2output [3:0] o;

3reg [3:0] x, y, z.

5always @(posedge clk)

6x <= y + z;

8assign o = x;

⬇

1input clk;

2output [3:0] o;

3reg [3:0] x, y, z.

5always @(posedge clk) begin

6x <= y;

7z <= -y

8end

10assign o = x+z;

⬇

1input clk;

2reg [63:0] reg_a, reg_b; //two operands

3reg [127:0] o; //product

4reg [5:0] counter; //shift counts

5reg finish;

7initial begin

8 o = 0;

9 finish = 0;

10 counter = 0;

11end

13always @(posedge clk) begin

14 if (reg_a == 0 || reg_b == 0) begin

15 finish <= 1;

16 end

17 else begin //shift and add

18 if (reg_b[0] == 1)

19 o <= o + reg_a << counter;

20 reg_b <= reg_b >> 1;

21 counter <= counter + 1;

22 end

23end

\nextpage

⬇

1input clk;

2reg finish;

4reg [127:0] o, o_next, d_leftover, n;

5initial begin

6 o_next = c; // c is the ciphertext

7 o = 1;

8 finish = 0;

9 d_leftover = d; // d is the decryption key

10 n = N; // N is the modulus

11end

13always @(posedge clk) begin

14 if(d_leftover[0] == 1) begin

15 o <= (o * o_next) % n;

16 end

18 o_next <= (o_next*o_next) % n;

19 d_leftover <= (d_leftover >> 1);

20end

22assign finish = (d_leftover == 0);