<feed xmlns='http://www.w3.org/2005/Atom'>
<title>montreal/verif/formal/simple_alu, branch feature/shifter</title>
<subtitle>RV32E core for TinyTapeout, codename "Montréal". Mirror of https://github.com/ubc-asic/montreal.git.
</subtitle>
<id>https://git.warricklo.net/montreal/atom?h=feature%2Fshifter</id>
<link rel='self' href='https://git.warricklo.net/montreal/atom?h=feature%2Fshifter'/>
<link rel='alternate' type='text/html' href='https://git.warricklo.net/montreal/'/>
<updated>2026-05-19T08:31:06+00:00</updated>
<entry>
<title>Pass linter</title>
<updated>2026-05-19T08:31:06+00:00</updated>
<author>
<name>Chat</name>
<email>63841542+chatrajaman3@users.noreply.github.com</email>
</author>
<published>2026-05-19T08:31:06+00:00</published>
<link rel='alternate' type='text/html' href='https://git.warricklo.net/montreal/commit/?id=429dd4fa609a5b8c71f8cd6ae6f8d74fd59f2280'/>
<id>urn:sha1:429dd4fa609a5b8c71f8cd6ae6f8d74fd59f2280</id>
<content type='text'>
  - simple_alu.sv: rename ports with suffixes (clk_i, rst_ni, a_i, b_i,
    sel_i, y_o, overflow_o); add default case to sel case statement;
    add y_next and overflow_next combinational signals; simplify
    always_ff to only register y_next and overflow_next
  - simple_alu_fv.sv: rename ports to match RTL (clk_i, rst_ni, a_i, b_i,
    sel_i, y_i, overflow_i); remove trailing spaces
  - simple_alu_top_fv.sv: rename ports; replace .* with explicit
    connections to match updated port names
  - simple_alu_bind.sv: add missing posix newline at EOF
</content>
</entry>
<entry>
<title>Add simple_alu RTL and formal verification</title>
<updated>2026-05-15T02:58:51+00:00</updated>
<author>
<name>Chat</name>
<email>63841542+ChillZero@users.noreply.github.com</email>
</author>
<published>2026-05-15T02:58:51+00:00</published>
<link rel='alternate' type='text/html' href='https://git.warricklo.net/montreal/commit/?id=1fcb70209582fd05c03919b31502deb2b7af472a'/>
<id>urn:sha1:1fcb70209582fd05c03919b31502deb2b7af472a</id>
<content type='text'>
  - simple_alu.sv: 32-bit ALU with add/sub, 33-bit extended overflow
    detection, and active-low synchronous reset
  - simple_alu_bind.sv: attaches checker to simple_alu without modifying RTL
  - simple_alu_top_fv.sv: replace bind (unsupported in open-source Yosys)
    with explicit wrapper that instantiates DUT and checker side-by-side
  - simple_alu_fv.sv: bind-based checker module observing DUT signals
  - simple_alu.sby: SymbiYosys config running BMC and cover tasks
  - README.md: verification plan tracking implemented and planned properties
  - .gitignore: exclude SymbiYosys output directories
</content>
</entry>
</feed>
