Enhance Synthesis Exit Checks (The-OpenROAD-Project#1698)

~ In `yosys`, call `check -assert` at the correct stage. This requires expanding `yosys` built-in command `synth` to its original sub-commands found in https://github.com/YosysHQ/yosys/blob/master/techlibs/common/synth.cc and inject `check -assert` in the middle of the expanded command. Experimentally, this was the only way to properly capture used wires that do not have a driver. Additional synthesis checkers guarded with `QUIT_ON_SYNTH_CHECKS`: \+ Add `check_latches` \+ Add `check_out_of_bound` \+ Add `check_resizing_cell_port` ~ Fix a "resizing cell port" error in `APU` design ~ Fix a "used but has no driver" error in `tests/912`
MrShaTr · Mar 28, 2023 · 90c6371 · 90c6371
1 parent d708849
commit 90c6371
Show file tree

Hide file tree

Showing 7 changed files with 91 additions and 12 deletions.
diff --git a/designs/APU/src/APU.v b/designs/APU/src/APU.v
@@ -675,8 +675,8 @@ assign odd_or_even = InternalClock;
 
 
 // Generate each channel
-SquareChan   Sq1(clk, ce, reset, 0, ADDR[1:0], DIN, ApuMW0, ClkL, ClkE, Enabled[0], LenCtr_In, Sq1Sample, Sq1NonZero);
-SquareChan   Sq2(clk, ce, reset, 1, ADDR[1:0], DIN, ApuMW1, ClkL, ClkE, Enabled[1], LenCtr_In, Sq2Sample, Sq2NonZero);
+SquareChan   Sq1(clk, ce, reset, 1'b0, ADDR[1:0], DIN, ApuMW0, ClkL, ClkE, Enabled[0], LenCtr_In, Sq1Sample, Sq1NonZero);
+SquareChan   Sq2(clk, ce, reset, 1'b1, ADDR[1:0], DIN, ApuMW1, ClkL, ClkE, Enabled[1], LenCtr_In, Sq2Sample, Sq2NonZero);
 TriangleChan Tri(clk, ce, reset, ADDR[1:0], DIN, ApuMW2, ClkL, ClkE, Enabled[2], LenCtr_In, TriSample, TriNonZero);
 NoiseChan    Noi(clk, ce, reset, ADDR[1:0], DIN, ApuMW3, ClkL, ClkE, Enabled[3], LenCtr_In, NoiSample, NoiNonZero);
 DmcChan      Dmc(clk, ce, reset, odd_or_even, ADDR[2:0], DIN, ApuMW4, DmcSample, DmaReq, DmaAck, DmaAddr, DmaData, DmcIrq, IsDmcActive);

diff --git a/designs/usb_cdc_core/src/usb_cdc_core.v b/designs/usb_cdc_core/src/usb_cdc_core.v
@@ -1037,6 +1037,7 @@ assign ep3_tx_data_strb_w  = 1'b0;
 assign ep3_tx_data_w       = 8'b0;
 assign ep3_tx_data_last_w  = 1'b0;
 assign ep3_tx_stall_w      = 1'b0;
+assign ep2_tx_stall_w      = 1'b0;
 
 assign ep2_rx_space_w      = 1'b0;
 assign ep3_rx_space_w      = 1'b0;

diff --git a/docs/source/reference/configuration.md b/docs/source/reference/configuration.md
@@ -325,7 +325,7 @@ These variables worked initially, but they were too sky130 specific and will be
 
 |Variable|Description|
 |-|-|
-| `QUIT_ON_SYNTH_CHECKS` | Use yosys `check -assert` at the end of synthesis. This checks for combinational loops, conflicting drivers and wires with no drivers. 1 = Enabled, 0 = Disabled <br> (Default: `1`)|
+| `QUIT_ON_SYNTH_CHECKS` | Quit if any of the following conditions are met: (1) `check -assert` in yosys. This checks for combinational loops, conflicting drivers and wires with no drivers. (2) Using a signal that doesn't match a module port size in the RTL. For instance, given such a module `module example(x); input x; endmodule` it gets instantiated like that `example y(2'b11);` (3) Found Latches in the design. (4) Out of bound(range) errors in the RTL. e.g. `wire [10:0] x; assign x[13] = 1'b1`. 1 = Enabled, 0 = Disabled <br> (Default: `1`)|
 | `QUIT_ON_UNMAPPED_CELLS` | Checks if there are unmapped cells after synthesis and aborts if any was found. 1 = Enabled, 0 = Disabled <br> (Default: `1`)|
 | `QUIT_ON_ASSIGN_STATEMENTS` | Checks for assign statement in the generated gate level netlist and aborts of any was found.1 = Enabled, 0 = Disabled <br> (Default: `0`)|
 | `QUIT_ON_TR_DRC` | Checks for DRC violations after routing and exits the flow if any was found. 1 = Enabled, 0 = Disabled <br> (Default: `1`)|

diff --git a/scripts/tcl_commands/checkers.tcl b/scripts/tcl_commands/checkers.tcl
@@ -12,7 +12,44 @@
 # See the License for the specific language governing permissions and
 # limitations under the License.
 
+proc check_latches {log} {
+    set match {\$LATCH}
+    set checker [exec bash -c "grep '$match' \
+        $log || true"]
+
+    if { $checker ne "" } {
+        puts_err "Synthesis failed. There are latches during synthesis."
+        throw_error
+    }
+}
 
+proc check_out_of_bound {log} {
+    set match {out of bounds on signal}
+    set checker [exec bash -c "grep '$match' \
+        $log || true"]
+
+    if { $checker ne "" } {
+        puts_err "Synthesis failed. Range select out of bounds on some signals. Search for '$match' in $log"
+        throw_error
+    }
+}
+
+proc check_resizing_cell_port {log} {
+    set match {Resizing cell port}
+    set checker [exec bash -c "grep '$match' \
+        $log || true"]
+
+    if { $checker ne "" } {
+        puts_err "Synthesis failed. Signal not matching port size. Search for '$match' in $log"
+        throw_error
+    }
+}
+
+proc run_synthesis_checkers {log} {
+    check_latches $log
+    check_out_of_bound $log
+    check_resizing_cell_port $log
+}
 
 proc check_assign_statements {args} {
     set checker [count_matches assign $::env(synthesis_results).v]

diff --git a/scripts/tcl_commands/synthesis.tcl b/scripts/tcl_commands/synthesis.tcl
@@ -119,6 +119,9 @@ proc run_synthesis {args} {
         set_netlist $::env(synthesis_results)/$::env(DESIGN_NAME).v
     } else {
         run_yosys -indexed_log $log
+        if { $::env(QUIT_ON_SYNTH_CHECKS) } {
+            run_synthesis_checkers $log
+        }
     }
     TIMER::timer_stop
     exec echo "[TIMER::get_runtime]" | python3 $::env(SCRIPTS_DIR)/write_runtime.py "synthesis - yosys"

diff --git a/scripts/yosys/synth.tcl b/scripts/yosys/synth.tcl
@@ -252,11 +252,52 @@ if { $adder_type == "RCA"} {
     }
 }
 
-if { $::env(SYNTH_NO_FLAT) } {
-    synth -top $vtop
+# taken from https://github.com/YosysHQ/yosys/blob/master/techlibs/common/synth.cc
+# <synth> split to run check -assert in the middle
+hierarchy -check -auto-top
+proc_clean
+proc_rmdead
+proc_prune
+proc_init
+proc_arst
+proc_rom
+proc_mux
+proc_dlatch
+proc_dff
+proc_memwr
+proc_clean
+opt_expr
+if { $::env(SYNTH_NO_FLAT) != 1 } {
+    flatten
+}
+opt_expr
+opt_clean
+if { $::env(QUIT_ON_SYNTH_CHECKS) == 1 } {
+    check -assert $::env(DESIGN_NAME)
 } else {
-    synth -top $vtop -flatten
+    check $::env(DESIGN_NAME)
 }
+opt -nodffe -nosdff
+fsm
+opt
+wreduce
+peepopt
+opt_clean
+alumacc
+share
+opt
+memory -nomap
+opt_clean
+opt -fast -full
+memory_map
+opt -full
+techmap
+opt -fast
+abc -fast
+opt -fast
+hierarchy -check
+stat
+check
 
 if { $::env(SYNTH_EXTRA_MAPPING_FILE) ne "" } {
     if { [file exists $::env(SYNTH_EXTRA_MAPPING_FILE)] } {
@@ -361,10 +402,6 @@ proc run_strategy {output script strategy_name {postfix_with_strategy 0}} {
     }
 
     write_verilog -noattr -noexpr -nohex -nodec -defparam $output
-    if { $::env(QUIT_ON_SYNTH_CHECKS) == 1 } {
-        read_liberty -ignore_miss_func $::env(LIB_SYNTH)
-        check -assert $::env(DESIGN_NAME)
-    }
     design -reset
 }
 design -save checkpoint

diff --git a/tests/912/src/def_test.v b/tests/912/src/def_test.v
@@ -19,8 +19,9 @@ module def_test (
     output tied_to_zero,
     output manufacturing_grid_missaligned_pin
     );
- // We tie this to one, so if def's pin is tied to zero, it will LVS error
-assign tied_to_zero = 1;
+    // We tie this to one, so if def's pin is tied to zero, it will LVS error
+    assign tied_to_zero = 1;
+    assign manufacturing_grid_missaligned_pin = 1;
 
     assign out = !in;