Merge pull request #1525 from danilovesky/verilog-import-inout

Improve STG verification and Verilog import

ci/flow-mpsat-g/test.result.ref

@@ -1 +1 @@
-24 out of 28 benchmarks passed the test
+22 out of 26 benchmarks passed the test

settings.gradle

@@ -22,7 +22,7 @@ gradle.ext.javaTargetVersion = JavaVersion.VERSION_11
 gradle.ext.javaReleaseVersion = 11  /* Must be integer, e.g. 11 for JDK11*/
 
 // Checkstyle code linter (https://checkstyle.sourceforge.io/)
-gradle.ext.checkstyleVersion = '10.12.2'
+gradle.ext.checkstyleVersion = '10.12.3'
 // PMD code analyser (https://pmd.github.io/)
 gradle.ext.pmdVersion = '6.55.0'
 // Jacoco code coverage (https://www.eclemma.org/jacoco/)

workcraft/CircuitPlugin/javacc/org/workcraft/plugins/circuit/jj/verilog/VerilogParser.jj

@@ -211,7 +211,7 @@ List<VerilogPort> parsePorts():
 }
 {
     (
-        LOOKAHEAD("(" (<INPUT> | <OUTPUT>))
+        LOOKAHEAD("(" (<INPUT> | <OUTPUT> | <INOUT>))
         ports = parseCompactPorts()
     |
         ports = parseExtendedPorts()
@@ -331,10 +331,15 @@ VerilogPort.Type parsePortType():
             return VerilogPort.Type.OUTPUT;
         }
     |
-        <WIRE>
+        <INOUT>
         {
-            return VerilogPort.Type.INTERNAL;
+            return VerilogPort.Type.INOUT;
         }
+    |
+        <WIRE>
+        {
+    return VerilogPort.Type.WIRE;
+}
 }
 
 VerilogPort.Range parseRange():

workcraft/CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitSettings.java

@@ -89,6 +89,7 @@ public class CircuitSettings extends AbstractModelSettings {
     private static final String keyVerilogAssignDelay = prefix + ".verilogAssignDelay";
     private static final String keyBusSuffix = prefix + ".busSuffix";
     private static final String keyDissolveSingletonBus = prefix + ".dissolveSingletonBus";
+    private static final String keyAcceptInoutPort = prefix + ".acceptInoutPort";
     private static final String keyModuleFilePattern = prefix + ".moduleFilePattern";
     // Reset
     private static final String keyResetActiveHighPort = prefix + ".resetActiveHighPort";
@@ -140,6 +141,7 @@ public class CircuitSettings extends AbstractModelSettings {
     private static final String defaultVerilogAssignDelay = "";
     private static final String defaultBusSuffix = "__" + BUS_INDEX_PLACEHOLDER;
     private static final boolean defaultDissolveSingletonBus = true;
+    private static final boolean defaultAcceptInoutPort = true;
     private static final String defaultModuleFilePattern = MODULE_NAME_PLACEHOLDER + FileFilters.DOCUMENT_EXTENSION;
     // Reset
     private static final String defaultResetActiveHighPort = "rst";
@@ -191,6 +193,7 @@ public class CircuitSettings extends AbstractModelSettings {
     private static String verilogAssignDelay = defaultVerilogAssignDelay;
     private static String busSuffix = defaultBusSuffix;
     private static boolean dissolveSingletonBus = defaultDissolveSingletonBus;
+    private static boolean acceptInoutPort = defaultAcceptInoutPort;
     private static String moduleFilePattern = defaultModuleFilePattern;
     // Reset
     private static String resetActiveHighPort = defaultResetActiveHighPort;
@@ -352,6 +355,11 @@ public class CircuitSettings extends AbstractModelSettings {
                 CircuitSettings::setDissolveSingletonBus,
                 CircuitSettings::getDissolveSingletonBus));
 
+        properties.add(new PropertyDeclaration<>(Boolean.class,
+                PropertyHelper.BULLET_PREFIX + "Accept inout ports and ignore their connections",
+                CircuitSettings::setAcceptInoutPort,
+                CircuitSettings::getAcceptInoutPort));
+
         properties.add(new PropertyDeclaration<>(String.class,
                 PropertyHelper.BULLET_PREFIX + "File pattern for import of hierarchical Verilog modules ("
                         + MODULE_NAME_PLACEHOLDER + " denotes module name)",
@@ -518,6 +526,7 @@ public void load(Config config) {
         setVerilogAssignDelay(config.getString(keyVerilogAssignDelay, defaultVerilogAssignDelay));
         setBusSuffix(config.getString(keyBusSuffix, defaultBusSuffix));
         setDissolveSingletonBus(config.getBoolean(keyDissolveSingletonBus, defaultDissolveSingletonBus));
+        setAcceptInoutPort(config.getBoolean(keyAcceptInoutPort, defaultAcceptInoutPort));
         setModuleFilePattern(config.getString(keyModuleFilePattern, defaultModuleFilePattern));
         // Reset
         setResetActiveHighPort(config.getString(keyResetActiveHighPort, defaultResetActiveHighPort));
@@ -569,6 +578,7 @@ public void save(Config config) {
         config.set(keyVerilogAssignDelay, getVerilogAssignDelay());
         config.set(keyBusSuffix, getBusSuffix());
         config.setBoolean(keyDissolveSingletonBus, getDissolveSingletonBus());
+        config.setBoolean(keyAcceptInoutPort, getAcceptInoutPort());
         config.set(keyModuleFilePattern, getModuleFilePattern());
         // Reset
         config.set(keyResetActiveHighPort, getResetActiveHighPort());
@@ -783,6 +793,14 @@ public static void setDissolveSingletonBus(boolean value) {
         dissolveSingletonBus = value;
     }
 
+    public static boolean getAcceptInoutPort() {
+        return acceptInoutPort;
+    }
+
+    public static void setAcceptInoutPort(boolean value) {
+        acceptInoutPort = value;
+    }
+
     public static String getModuleFilePattern() {
         return moduleFilePattern;
     }