diego

1. Proof equivalence of algebraic and geometric definition of dot product
- 1.1. Observation
  - 1.1.1. Proof

1. Proof equivalence of algebraic and geometric definition of dot product

This is a quick proof on the equivalent definitions for the dot product. Just for me to test on how integrate org roam with latex tikz and sage plugins, I generate this HTML page with the Emacs function org-html-export-as-html(with minor edits),

1.1. Observation

Algebraic and geometric definitions of dot product are equivalent this is: $x\cdot y = (x_1,x_2) \cdot (y_1,y_2) = x_1y_1 + x_2y_2 = \Vert x\Vert \Vert y\Vert \cos{\theta}$ where $\theta$ is the angle between x and y

1.1.1. Proof

We will proove it for the 2 dimention case, it can be easily extended to n dimention by embedding the 2 vectors in a plane… Lets consider x and y as in the definition, notice that the dot product is invariant over chage of orthonormal bases, this because given a 2×2 matrix M we have that $Mx \cdot My = (m_{11}x_{1}+m_{12}x_{2}, m_{21}x_{1} + m_{22}x_{2}) \cdot (m_{11}y_{1}+m_{12}y_{2}, m_{21}y_{1}+m_{22}y_{2}) =$ $m_{11}^{2} x_{1} y_{1} + m_{21}^{2} x_{1} y_{1} + m_{11} m_{12} x_{2} y_{1} + m_{21} m_{22} x_{2} y_{1} + m_{11} m_{12} x_{1} y_{2} + m_{21} m_{22} x_{1} y_{2} + m_{12}^{2} x_{2} y_{2} + m_{22}^{2} x_{2} y_{2}$ Notice that it can be refactored as $x_1y_1(m_{11}^2 + m_{21}^{2}) + (x_1y_2 + x_2y_{1})(m_{11}m_{12}+m_{21}m_{22}) + x_2y_2(m_{22}^2 + m_{12}^{2})$ and as M is an orthogonal matrix then $m_{11}m_{12} + m_{21}m_{22} = 0$ as that matrix has as columns orthogonal vectors and this expression is its dot product also notice the $m_{11}^2 + m_{21}^2 = \Vert m_{1}\Vert ^{2}$ and $m_{22}^2 + m_{12}^2 = \Vert m_{2}\Vert^{2}$ where $[m_{1} | m_{2}] := m$ this is are the orthnormal vectors of the base, and as they are unitary then both previous expresions are equal to one so finally $Mx \cdot My = x_1y_1 + x_2y_2 = x \cdot y$

So to proof $x_1y_1 + x_2y_2 = \Vert x\Vert \Vert y\Vert \cos{\theta}$ we will change the base of x and y from the standard base i, j to a new base $u := \hat x$ and $v := \hat x ^{\perp}$ which are the unitary vector in the x direction and the perpendicular vector (so that we have a right coordinate) to the unitary x vector respectively

Following the diagram of the two bases described in the las parragraph

\begin{tikzpicture}
  \draw[<->] (-1,0)--(1,0) node[right]{$i$};
  \draw[<->] (0,-1)--(0,1) node[above]{$j$};
  \draw[<->,red] (45:-1)--(45:1) node[above]{$u := \hat x$};
  \draw[<->,red] (135:-1)--(135:1) node[above]{$v := \hat x ^\perp$};
\end{tikzpicture}

To simplifly calculaitions notice that $v = (-x_{2}, x_{1})$ that way we can express the matrix of base change from (u,v) to (i,y) is the matrix m in then code below. Also recall that $\left| x \right| \left| y \right| \cos \theta$ can be seen geometrically as $\left| x \right| \text{Proj}_{x}y$ this is the norm of x times the projection of y over x Now if we change to the base (u,v) conveniently the projection of y over x will be just be the component in the $\hat x$ direction (first coordinate).

var('x1 x2 y1 y2');
x = vector([x1,x2]);
y = vector([y1,y2]);
xhat = x/norm(x)
m = matrix([ [xhat[0],-xhat[1]],[xhat[1],xhat[0]] ])
print(f'm = ', end='');
mylatex(factor(m))
print(f'X := m^-1*x = ', end="");
X = (m.inverse()*x).apply_map(factor)
mylatex( X )
print(f'Y := m^-1*y = ', end="");
Y = (m.inverse()*y).apply_map(factor)
mylatex( Y )

m = $\left(\begin{array}{rr} \frac{x_{1}}{\sqrt{x_{1}^{2} + x_{2}^{2}}} & -\frac{x_{2}}{\sqrt{x_{1}^{2} + x_{2}^{2}}} \\ \frac{x_{2}}{\sqrt{x_{1}^{2} + x_{2}^{2}}} & \frac{x_{1}}{\sqrt{x_{1}^{2} + x_{2}^{2}}} \end{array}\right)$
X := m^-1*x = $\left(\sqrt{x_{1}^{2} + x_{2}^{2}},\,0\right)$
Y := m^-1*y = $\left(\frac{x_{1} y_{1} + x_{2} y_{2}}{\sqrt{x_{1}^{2} + x_{2}^{2}}},\,-\frac{x_{2} y_{1} - x_{1} y_{2}}{\sqrt{x_{1}^{2} + x_{2}^{2}}}\right)$

And according to our last discussion then $\text{Proj}_{X}Y = \frac{x_{1} y_{1} + x_{2} y_{2}}{\sqrt{x_{1}^{2} + x_{2}^{2}}}$ and finally we have that $x \cdot y = X \cdot Y = \left| X \right| \text{Proj}_XY = \sqrt{x_1^2 + x_2^2}\ \frac{x_{1} y_{1} + x_{2} y_{2}}{\sqrt{x_{1}^{2} + x_{2}^{2}}} = x_{1} y_{1} + x_{2} y_{2}$ As stated

1. Example of a naive testbench in verilog

Following a dummy example of a basic test bench designed on SV, this example is extracted from the grate UVM primer book by Ray Salemi, this design is naive in the sense that it has a rigid architecture, it lacks extensibility and scalability, for really basic designs it should be fine (also if you want to rapidly test a small part of a larger design), but for large projects with multiple teams working on the same IP, this test bench architecture won’t work.

module test(PAddr, PWrite, PSel, PWData, PEnable, Rst, clk);
   // Port declarations omitted...

   initial begin
      // Drive reset

      Rst <= 0;
      #100 Rst <=Re1%;

      // Drive the control bus

      @ (posedge clk)
        PAddr <= 16’'h50;
      PWData <= 32'h50;
      PWrite <= 1'b1;
      PsSel <= 1'bl;

      // Toggle PEnable
      @ (posedge clk)
        PEnable <= 1'bl;
      @ (posedge clk)
        PEnable <= 1'b0;



      // Check the result

      if (top.mem.memory[16’h50] == 32’'h50)
        $display("Success");
      else
        $display("Error, wrong value in memory") ;
      $finish;
   end
endmodule

Author Archives: diego

Proof equivalence of algebraic and geometric definition of dot product

Table of Contents

1. Proof equivalence of algebraic and geometric definition of dot product

1.1. Observation

1.1.1. Proof

Naive Verilog Test Bench

1. Example of a naive testbench in verilog

Proof assistants