Method of checking equivalence between a first design comprising a shift register logic SRL chain and a second design

Abstract

A method of checking equivalence between a first design comprising a shift register logic SRL chain and a second design comprising a memory block. The method comprises identifying an inductive invariant to replace the SRL chain or the memory block, and replacing the SRL chain and the memory block by a set of constraints, wherein the set of constraints state that the SRL chain and the memory block are equivalent for the checking of equivalence between the first design and the second design.

Claims

1. A computer implemented method of checking equivalence between a first design comprising a shift register logic SRL chain and a second design comprising a memory block comprising a read-address and a write-address, the method comprising: verifying a plurality of conditions corresponding to a transformation of the SRL chain into the memory block, wherein the plurality of conditions comprise the following conditions: C1) the initial states for the SRL chain and the memory block are equivalent, C2) the first design implements a shift register, C3) the revised memory block is written at the location pointed to by a write address and read from the location pointed to by a read address, C4) the read and write addresses in the revised memory block maintain an offset n, and C5) the write address is implemented by a counter; checking that the plurality of conditions hold, in order to prove that the SRL chain in the first design is formally equivalent to the memory block in the second design, replacing the SRL chain and the memory block by a set of constraints, wherein the replacing comprising removing the SRL chain and the memory block circuit and the set of constraints comprises the assertion dg=dr that the input data of SRL chain in the first design and the input data of the memory block in the second design are equivalent and the assumption outg=outr that the output data of SRL chain in the first design and the output data of the memory block in the second design are equivalent; and applying equivalence checking between the first design and the second design, wherein internal implementation details of the SRL chain in the first design and of the memory block in the second design are ignored during the equivalence checking.

2. The method of claim 1, comprising checking the validity of the replacement step, the method comprises verifying of a set of theorems using said plurality of conditions to prove that the SRL chain in the first design is formally equivalent to the memory circuitry in the second design, whereby if the plurality of conditions hold, the validity of said replacement step follows from said set of theorems.

3. The method according to claim 1, wherein the method comprises maintaining an offset between the read-address and the write-address, whereby the offset corresponds to the length of the SRL chain.

4. The method of claim 1, wherein a counting scheme in the revised with an effective offset between the read address and the write address is maintained.

5. The method of claim 1, wherein an enable signal is provided.

6. The method of claim 1, wherein an asynchronous clear is provided, so that registers of the SRL chain can be directly reset using the asynchronous clear signal.

7. The method of claim 4 wherein a synchronous reset is provided, so that the registers of the SRL chain can be synchronously reset using the synchronous reset signal with respect to the clock signal.

8. The method of claim 1, wherein the input stage of the memory block is buffered with one or more stages of input registers.

9. The method of claim 8, wherein an effective offset between the read address and write address of the memory block is the difference between the length of the SRL chain (n) and the number of the one or more stages of input registers (p), to account for p stages of input registers.

10. The method of claim 1, wherein the enable signal is registered to form a delayed signal (enreg) which is further applied as the enable signal of the memory block storage elements.

11. The method of claim 1, where the output of the memory is buffered with one or more stages of the output registers in the revised side.

12. The method of claim 11, wherein the number of such output registers after the core memory block is deduced using state-reachability analysis.

13. The method of claim 1, wherein the revised memory result in a parallel or cascaded memory configuration.

14. The method of claim 1, wherein the width of the SRL chain is more than one.

15. A non-transitory computer-readable storage medium having stored therein software instructions that, when executed by a processor, cause the processor to perform a method of checking equivalence between a first design comprising a shift register logic SRL chain and a second design comprising a memory block comprising a read-address and a write-address, the method comprising: verifying a plurality of conditions corresponding to a transformation of the SRL chain into the memory block, wherein the plurality of conditions comprises the following conditions: C1) the initial states for the SRL chain and the memory block are equivalent, C2) the first design implements a shift register, C3) the revised memory block is written at the location pointed to by a write address and read from the location pointed to by a read address, C4) the read and write addresses in the revised memory block maintain an offset n, and C5) the write address is implemented by a counter; checking that the plurality of conditions hold, in order to prove that the SRL chain in the first design is formally equivalent to the memory block in the second design, replacing the SRL chain and the memory block by a set of constraints, wherein the replacing comprising removing the SRL chain and the memory block circuit and the set of constraints comprises the assertion dg=dr that the input data of SRL chain in the first design and the input data of the memory block in the second design are equivalent and the assumption outg=outr that the output data of SRL chain in the first design and the output data of the memory block in the second design are equivalent; and applying equivalence checking between the first design and the second design, wherein internal implementation details of the SRL chain in the first design and of the memory block in the second design are ignored during the equivalence checking.

Description

BRIEF DESCRIPTION OF THE DRAWINGS

(1) For a more complete understanding of the present invention and the advantages thereof, reference is now made to the following description and the accompanying drawings, in which:

(2) FIGS. 1A-1B illustrate a principle of a transformation between a shift register chain SRL chain into an equivalent memory circuitry.

(3) FIG. 2 illustration of a transformation between a shift register chain SRL chain into an equivalent memory circuitry.

(4) FIG. 3 a flowchart of an equivalence checking between a shift register chain SRL chain into an equivalent memory circuitry.

(5) FIGS. 4A-4C illustrate a principle of an equivalence checking between a shift register chain SRL chain into an equivalent memory circuitry in an aspect of the present disclosure.

(6) FIG. 5 a principle of a transformation between a shift register chain SRL chain into an equivalent memory circuitry in an aspect of the present disclosure.

(7) FIG. 6 a principle of a transformation between a shift register chain SRL chain into an equivalent memory circuitry in an aspect of the present disclosure.

(8) FIG. 7 a principle of a transformation between a shift register chain SRL chain into an equivalent memory circuitry in an aspect of the present disclosure.

(9) FIG. 8 a principle of a transformation between a shift register chain SRL chain into an equivalent memory circuitry in an aspect of the present disclosure.

(10) FIG. 9 a principle of a transformation between a shift register chain SRL chain into an equivalent memory circuitry in an aspect of the present disclosure.

(11) FIG. 10 is a system architecture diagram of a system for equivalence checking between a first design comprising a shift register logic SRL chain and a second design comprising a memory block in accordance with a preferred embodiment of the present invention.

DETAILED DESCRIPTION OF PREFERRED EMBODIMENTS

(12) In the following, and as already shown in FIG. 1, the individual elements of the SRL chain are denoted as s(0) to s(n−1), where n is the length of the SRL chain. The depth of the RAM, which is a non-restrictive example of using a block memory, on the revised design is m. A superscript notation is used to denote the next state. For instance, s′(i) is the next state of the register element of the SRL at position i. Subscripts are used to differentiate between the golden and the revised designs. For instance, d.sub.g is the data input signal at the golden design. The corresponding data input in the revised design is dr.

(13) The individual elements of the memory are referred to using lowercase ram. For instance, ram(k) is the kth location of the memory. RAM(i) is the memory element corresponding to the ith location in the SRL chain.

(14) The present invention proposes a method of checking of equivalence between a first design 1 comprising an SRL chain 10 and a second design 2 comprising a memory block 20.

(15) A general architecture for a system for equivalence checking between a shift register chain SRL chain into an equivalent memory circuit in accordance with a preferred embodiment of the present invention is shown in FIG. 10. The system includes a computing device 3000, which may be a computer or server having one or more processors, a memory and a non-transitory storage medium such as a hard drive or solid state drive. The computing device 3000 has a proof module 3100, a verification module 3200, and equivalence checking module 3400. The computing device may have other modules or applications.

(16) A general equivalence checking is depicted in FIG. 4A, together with the flowchart of FIG. 3.

(17) In the following, the first design 1 is called “golden design”, and the second design 2 is referred to as “revised design”.

(18) As shown in FIG. 4C, in the first stage, a plurality of conditions C1 to C5 in the golden design 1 and in the revised designs 2 are proved. These conditions establish that there exists a proper SRL chain 10 in the golden design 1 and properly composed memory 20 in the revised design 2. This step will be described later in the disclosure and can be performed by the proof module.

(19) Once these necessary conditions C1 to C5 are proved, one or more constraints 50 are formed at the output out.sub.g of the golden SRL chain 10 and at the output outr the revised memory block 20 and an assertion 60 is added at the respective input d.sub.g, dr. This is shown on FIG. 4C and can be performed by the verification module. The constraint(s) 50 state(s) that the respective outputs of the SRL and the memory block implementation are equivalent.

(20) The equivalence checking problem further proceeds with these constraints and assertion and can be performed by the equivalence checking module. This means that the internal circuitry of the SRL or the memory block is not taken into consideration further and the complete equivalence checking problem can be decomposed into the individual stages described before. These theorems provide sufficient criteria to guarantee that the shift register logic and its implementation using a memory block are equivalent. Therefore, in subsequent steps, the internal implementation details of both the SRL chain in the golden design and the corresponding memory circuitry in the revised design can be ignored. This simplifies the remaining equivalence checking problem considerably, enabling scalable verification for industrial sized designs.

(21) Hence, after establishment of the necessary conditions C1 to C5 in the golden and revised designs, the equivalence checking problem sums up to proving the constraint 50 that out.sub.r=out.sub.g, i.e. that the sink of the SRL and its implementation on the revised design are always delivering the same data. This corresponds to a decision that an inductive invariant has been identified.

(22) The different stages of FIGS. 4B and 4C are described in the following sections.

(23) The first stage shown on FIG. 4B consists in verifying a plurality of conditions corresponding to the transformation of the SRL chain 10 into the memory block 20. For the sake of convenience, the conditions are written with the acronym RAM for the memory block. It is noted that the memory block can be a RAM, SRAM, DRAM, Magnetic RAM, Block RAM etc. as the core element

(24) A first condition C.1 requires that the initial states for the golden and the revised are equivalent, as follows:
(a) ∀.sub.i=0.sup.n-1(s(i)=0)
(b) ∀.sub.k=0.sup.m-1(ram(k)=0)  Condition C.1

(25) According to a second condition C2, the golden design implements a shift register.

(26) $\begin{array}{cc}\mathrm{Condition}C\mathrm{.2}& \\ {\forall }_{i=0}^{n-1}{s}^{\prime }\left(i\right)=\{\begin{array}{cc}{d}_g& \mathrm{if}i=0\\ s\left(i-1\right)& \mathrm{otherwise}\end{array}& \left(a\right)\\ {\mathrm{out}}_g=s\left(n-1\right)& \left(b\right)\end{array}$
A third condition C.3 states that the revised design memory is written at the location pointed to by W.sub.addr and read from the location pointed to by Radar

(27) $\begin{array}{cc}\mathrm{Condition}C\mathrm{.3}& \\ {\forall }_{k=0}^{m-1}{\mathrm{ram}}^{\prime }\left(k\right)=\{\begin{array}{cc}{d}_r& \mathrm{if}k=W_{\mathrm{addr}}\\ \mathrm{ram}\left(k\right)& \mathrm{otherwise}\end{array}& \left(a\right)\\ {\mathrm{out}}_r=\mathrm{ram}\left(R_{\mathrm{addr}}\right)& \left(b\right)\end{array}$
According to a fourth condition C4, the read and write addresses in the revised design maintain an offset n, the SRL chain length.
W.sub.addr=(R.sub.addr+n)%m  Condition C.4

(28) Finally, a fifth condition C.5 states that a write address W.sub.addr is implemented by a counter
W′.sub.addr=(W.sub.addr++1)%m  Condition C.5

(29) Once the plurality of conditions C1 to C5 has been introduced, a set of theorems for the transformation from the SRL chain 10 to the memory block 20 can be proved in order to prove the equivalence between the golden design 1 and the revised design 2, i.e. the invariant provided in the below equation:
∀.sub.i=0.sup.n-1(s(i)==RAM(i))  Equation (1)
This correspond to the stage shown on FIG. 4C and the stage is explained below.

(30) The first step is to derive a relationship between RAM(i) and ram(k). Recall that RAM(i) is the memory element corresponding to s(i), the ith SRL element, as explained with reference to FIGS. 1A-1B. Once again consider the individual steps in the example provided in FIG. 2. Here, n=4 and m=5 (number of storage elements in the memory). As the shift progresses in time w.r.t. the clock cycles, the W.sub.addr increments, whereas the position of the registers in the SRL chain remains the same.

(31) For the example in FIG. 2 Step 4, W.sub.addr points to the 2nd storage cell and the following relations are derived
RAM(0)=ram((W.sub.addr−0−1)%5)=ram(1)
RAM(1)=ram((W.sub.addr−1−1)%5)=ram(0)
RAM(2)=ram((W.sub.addr−2<1)%5)=ram(4)
RAM(3)=ram((W.sub.addr−3−1)%5)=ram(3)

(32) Similarly, in FIG. 2 Step 5, W.sub.addr=3 and RAM(0)=ram(W.sub.addr−0−1)=ram(2), and so on.

(33) Summarizing the SRL shift pattern and the RAM storage locations, the relation can be generalized as follows:
RAM(i)=ram((W.sub.addr−i−1)%m)  Equation (2)

(34) It should be noted that the variable n does not appear in Equation 2. Instead, the offset n is proved separately for the relationship between W.sub.addr and R.sub.addr in condition C.4.

(35) Next, the set of theorems, namely theorem 1, theorem 2 and theorem 3, in the context of the equivalence verification is provided.

(36) $\begin{array}{cc}\mathrm{Theorem}1.& \\ {\forall }_{i=0}^{m-1}{\mathrm{Ram}}^{\prime }\left(k\right)=\{\begin{array}{cc}{d}_r,& \mathrm{if}i=0,\\ \mathrm{RAM}\left(i-1\right)& \mathrm{otherwise}\end{array}& \end{array}$

(37) Proof

(38) RAM(i)=ram((W.sub.addr−i−1) % m)) from Equation (2)

(39) RAM′(i)=ram′((W′.sub.addr−i−1) % m))

(40) RAM′(i)=ram′((W.sub.addr−i) % m)) from Condition C.5

(41) i=0: RAM′(0)=ram′((W.sub.addr) % m)) RAM′(0)=d.sub.r from Condition C.3

(42) i>0: RAM′(i)=ram′((W.sub.addr−i) % m)) RAM′(i)=ram((W.sub.addr−i))% m from Condition C.3 RAM′(i)=ram((W.sub.addr−(i−1)−1) % m)) RAM′(i)=RAM(i−1) using Equation (2)

(43) Theorem 2,

(44) ∀.sub.i=0.sup.n-1s(i)==RAM(i)

(45) Proof (induction)

(46) Step 1: initial state equivalence from Condition

(47) Step 2: s′(i)==RAM′(i)

(48) i=0: dg==dr assertion for input equivalence

(49) i>0: s(i−1)==RAM(i−1) using Theorem 1 and C.2 assertion for nut equivalence

(50) By virtue of the induction, the second theorem 2 proves that the SRL chain 10 in the golden design 1 is equivalent to the memory circuitry or memory block 20 in the revised design 2, if the conditions C.1 to C.5 are satisfied and the assertion 60 at the respective input sides holds.

(51) Theorem 2 proves that the SRL chain 10 in the golden design is formally equivalent to the memory circuitry 20 in the revised design, leading to theorem 3:

(52) Theorem 3.

(53) out.sub.r=out.sub.g

(54) Proof

(55) out.sub.r=ram(R.sub.addr)

(56) out.sub.r=ram(((R.sub.addr+n) % m)−n) % m

(57) out.sub.r=ram((W.sub.addr−n) % m) using Condition C.4

(58) out.sub.r=RAM(n−1) using Equation (2)

(59) out.sub.r=s(n−1) using Theorem 2

(60) out.sub.r=out.sub.g using Condition C.2

(61) In other words, after proving the plurality of conditions C.1 to C.5, the following constraint 50 and assertion 60 are added to the complete equivalence checking problem: constrain out.sub.g==out.sub.r assert d.sub.g==d.sub.r
This means that for the subsequent steps of verification, the output signals of the SRL chain and of the memory block are assumed to be functionally equivalent when the inputs of the SRL chain and the memory block are driven by the same data. Hence, the internal circuitry of the SRL chain and of the memory block can be ignored.

(62) In an embodiment for the transformation from an SRL chain to memory block and the verification techniques provided, the counting circuitry in the revised design is implemented using any of the counting schemes such as a binary counter, Gray counter, Johnson counter, ring counter, one-hot/one-cold encoded counter etc. For proving that the memory implementation is equivalent to the SRL in the golden design, the encoding or working of the counter is irrelevant. Important is that the effective offset between the read-address and the write-address is n (Condition 4).

(63) In a second embodiment shown on FIG. 5, an enable signal is provided and the related modifications to the SRL chain 210 and the memory block circuitry 220 are shown in FIG. 5.

(64) In order to check equivalence of the SRL chain 210 and the memory block 220 in the presence of enable signals, the plurality of conditions and the set of theorems can be modified to take into account said enable signal. Note that only those conditions that differ from the conditions of the first embodiment are listed in the following.

(65) The golden design 210 implements a shift register.

(66) $\begin{array}{cc}{\forall }_{i=0}^{n-1}{s}^{\prime }\left(i\right)=\{\begin{array}{cc}s\left(i\right),& \mathrm{if}{\mathrm{en}}_g=0\\ d_g,& \mathrm{if}i=0.Math.{\mathrm{en}}_g=1\\ s\left(i-1\right),& i>0.Math.{\mathrm{en}}_g=1\end{array}& \left(a\right)\\ {\mathrm{out}}_g=s\left(n-1\right)& \left(b\right)\end{array}$

(67) The revised design memory 220 is written at the location pointed by W.sub.addr and read from the location R.sub.addr

(68) $\begin{array}{cc}{\forall }_{k=0}^{m-1}{\mathrm{ram}}^{\prime }\left(k\right)=\{\begin{array}{cc}{d}_r& \mathrm{if}k=W_{\mathrm{addr}}.Math.{\mathrm{en}}_r=1\\ \mathrm{ram}\left(k\right)& \mathrm{otherwise}\end{array}& \left(a\right)\\ {\mathrm{out}}_r=\mathrm{ram}\left(R_{\mathrm{addr}}\right)& \left(b\right)\end{array}$

(69) The write address W.sub.addr is implemented by a counter.

(70) $\begin{array}{cc}{W}_{\mathrm{addr}}^{\prime }=\{\begin{array}{cc}\left(W_{\mathrm{addr}}+1\right)\%m& \mathrm{if}{\mathrm{en}}_r==1\\ W_{\mathrm{addr}}& \mathrm{otherwise}\end{array}& \left(a\right)\end{array}$

(71) The modified theorems incorporating the enable signal are as follows. It should be noted that both statement and proof of Theorem 3 is unaffected by the addition of the enable signal and as such omitted in the following.

(72) $\begin{array}{cc}\mathrm{Theorem}1.& \\ {\forall }_{i=0}^{m-1}{\mathrm{RAM}}^{\prime }\left(i\right)=\left\{\begin{array}{cc}\mathrm{RAM}\left(i\right),& \mathrm{if}\mathrm{en}=0\\ d_r,& \mathrm{if}i=0.Math.\mathrm{en}=1\\ \mathrm{RAM}\left(i-1\right),& \mathrm{if}i>0.Math.\mathrm{en}=1\end{array},\mathrm{Proof}\mathrm{RAM}\left(i\right)=\mathrm{ram}\left(\left(W_{\mathrm{addr}}-i-1\right)\%m\right)\right){\mathrm{RAM}}^{\prime }\left(i\right)={\mathrm{ram}}^{\prime }\left(\left(W_{\mathrm{addr}}^{\prime }-i-1\right)\%m\right))\mathrm{en}=0\text{:}\mathrm{using}\mathrm{Conditions}C\mathrm{.5}\mathrm{and}C\mathrm{.3}{\mathrm{RAM}}^{\prime }\left(i\right)=\mathrm{RAM}\left(i\right)\mathrm{en}=1\text{:}\mathrm{Same}\mathrm{as}\mathrm{in}\mathrm{proof}\mathrm{of}\mathrm{Theorem}1\mathrm{in}\mathrm{the}\mathrm{basic}\mathrm{framework}.& \mathrm{from}\mathrm{Equation}\left(2\right)\end{array}$

(73) Theorem 2.

(74) ∀.sub.i=0.sup.n-1s(i)==RAM(i)

(75) Proof (induction)

(76) Base Case: initial state equivalence from Condition C.1

(77) Inductive Step

(78) en=0:

(79) ∀.sub.i=0.sup.n-1(s′(i)==s(i)){circumflex over ( )}∀.sub.k=0.sup.m-1(ram′(k)==ram(k))

(80) Same as in proof of Theorem 2 in the first embodiment

(81) In yet a third embodiment an asynchronous clear (aclr) is provided. This results in additionally the register elements being cleared when an aclr signal is provided. Once the SRL registers are cleared it takes n steps for the next input to be shifted to the output. All the stored data before the aclr signal is cleared. The synthesis tool can choose to implement this in a variety of techniques; for e.g., clear the respective memory elements or delay the aclr signal for n-cycles and gate (Boolean AND) the output of the memory with this delayed aclr signal (aclr-out). For equivalence checking, it needs to be sufficient only to verify that the memory-output is cleared for n-cycles and has valid data at the end of n cycles, after aclr signal is asserted. This results in the condition C3 being gated with an additional aclr-out signal which is an n-cycle delayed version of aclr. Note that the polarity of aclr signal (active low or active high) need to be taken care in the memory output gating signal aclr-out also.

(82) The condition C.3, which provides that the revised design memory is written at the location pointed by W.sub.addr and read from the location Radar, in the presence of asynchronous clear is given below

(83) $\begin{array}{cc}c\mathrm{ondition}C3& \\ {\forall }_{k=0}^{m-1}{\mathrm{ram}}^{\prime }\left(k\right)=\{\begin{array}{cc}{d}_r& \mathrm{if}k=W_{\mathrm{addr}}\\ \mathrm{ram}\left(k\right)& \mathrm{otherwise}\end{array}& \left(a\right)\\ {\mathrm{out}}_r=\mathrm{ram}\left(R_{\mathrm{addr}}\right).Math.\mathrm{adr\_out}& \left(b\right)\end{array}$

(84) In yet a fourth embodiment a synchronous reset (rst) is provided. This embodiment is the same as the previous embodiment. The condition C3 need to be gated with an additional rst-out signal which is an n-cycle delayed version of the original rst signal.

(85) In yet a fifth embodiment, the synthesis tool can also choose to buffer the input stage in the revised memory 420. In this type of SRL2MEMORY transformation, the input of the revised memory, dr, is sampled with one or more registers. The number of such register stages before the memory block is p. In this case, the first p stages are checked using standard equivalence checking techniques and the next (n-p) stages are verified using the verification techniques in first embodiment with a modification of the effective length of the SRL from n to (n-p).

(86) In yet a sixth embodiment, the synthesis tool can also choose to delay the enable signal in the revised memory of the second embodiment. This type of SRL2MEMORY transformation needs to be balanced with an additional input stage register. The enable signal after buffering is called enreg. Here it is only sufficient to verify the revised design storage locations are written and read incorporating the enreg signal (Condition C3) and the counter mechanism also takes enreg into consideration (Condition C5)

(87) C.3 The revised design storage locations are properly written and read:

(88) $\begin{array}{cc}{\mathrm{pdi}}^{\prime }=d_r& \left(a\right)\\ {\forall }_{k=0}^{m-1}{\mathrm{ram}}^{\prime }\left(k\right)=\{\begin{array}{cc}\mathrm{pdi},& \mathrm{if}k=W_{\mathrm{addr}}.Math.\mathrm{enreg}=1\\ \mathrm{ram}\left(k\right)& \mathrm{otherwise}\end{array}& \left(b\right)\\ {\mathrm{out}}_r=\mathrm{ram}\left(R_{\mathrm{addr}}\right)& \left(c\right)\end{array}$

(89) C.5 Revised design has a proper write address mechanism, W.sub.addr, that functions as a counter.

(90) 0$\begin{array}{cc}{W}_{\mathrm{addr}}^{\prime }=\{\begin{array}{cc}\left(W_{\mathrm{addr}}+1\right)\%m& \mathrm{if}\mathrm{enreg}==1\\ W_{\mathrm{addr}}& \mathrm{otherwise}\end{array}& \left(a\right)\end{array}$

(91) In yet a seventh embodiment, one or more registers at the output of the memory can be inserted. The corresponding synthesis transformation from an SRL chain 510 to a memory block 520 is shown in FIG. 9. The output of the core memory block 520 is the signal mem_out. This signal is sampled through one or more stages of output register before the final outr, is emitted. The number of output stage registers is specific to the synthesis tool and the targeted device technology. For equivalence checking, we can consider the register driven by mem_out signal as a last element in the memory block instead of a separate stage. i.e., ram(m−1)=mem_out. Using this notation, the initial conditions to be proved and the associated theorems are the same as in the first embodiment with reference to FIGS. 1A-1B. The theorems and the methodology provided with reference to FIG. 1A-1B can be applied directly to the synthesis with output registers. The number of such output stages if needed is deduced using state reachability analysis.

(92) In yet another embodiment, the SRL2MEMORY transformation is applied to SRL chains where width is more than 1. In this case, the individual chains get mapped to the successive bits of the same word of the memory in the revised design. This can result in parallel or cascaded RAM configurations, when the word length does not match the SRL chain width. The formal verification theory of the present disclosure is applied directly without any modification in such situations also. In this case, each SRL chain is taken separately and verified one at a time.

(93) Finally, it should be noted that the memory topology can vary, for example the memory elements may be arranged in a cascaded fashion in the revised block as a result of synthesis irrespective of the width of the SRL chain. This does not change the verification method explained in the present disclosure.

(94) The foregoing description of the preferred embodiment of the invention has been presented for purposes of illustration and description. It is not intended to be exhaustive or to limit the invention to the precise form disclosed, and modifications and variations are possible in light of the above teachings or may be acquired from practice of the invention. The embodiment was chosen and described in order to explain the principles of the invention and its practical application to enable one skilled in the art to utilize the invention in various embodiments as are suited to the particular use contemplated. It is intended that the scope of the invention be defined by the claims appended hereto and their equivalents. The entirety of each of the aforementioned documents is incorporated by reference herein.